Selene/AStat
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

Init commit

Browse source
This commit is contained in:
Granahir2 2024-05-29 11:47:47 +02:00
parent 1d3fb5eb85
commit e6ecc3e9b0
60 changed files with 6656 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
.gitignore vendored Normal file
View file

@ -0,0 +1,8 @@
*.html
analyzer
results/
_build/
*.dot
*.pdf
*.svg
*.tar.gz

31
Makefile Normal file
View file

@ -0,0 +1,31 @@
# Cours "Semantics and applications to verification"
#
# Marc Chevalier 2018
# Josselin Giet 2021
# Ecole normale supérieure, Paris, France / CNRS / INRIA
.PHONY: all clean cleantest doc compress
all:
@rm -f analyzer.exe
@dune build analyzer.exe
@ln -sf _build/default/analyzer.exe analyzer
clean: cleantest
@rm -rf _build/ analyzer *~ */*~
@rm -rf *.dot *.pdf *.svg */*.dot */*.pdf */*.svg *.tar.gz
cleantest:
@rm -rf results
# Use `make test TEST_OPT="--flags"` to run tests with extra flags.
TEST_OPT::=""
test: cleantest all
@scripts/test.sh . ${TEST_OPT}
doc: all
@dune build @doc-private
compress: clean
@tar -czvf ../project-semantics.tar.gz --exclude=".git*" ../project-semantics
@mv ../project-semantics.tar.gz .

37
analyzer.ml Normal file
View file

@ -0,0 +1,37 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Simple driver: parses the file given as argument and prints it back.
You should modify this file to call your functions instead!
*)
open Iterator
open Cfg
(* parse filename *)
let doit filename = begin
let prog = File_parser.parse_file filename in
let cfg = Tree_to_cfg.prog prog in
if !Options.verbose then
Format.printf "%a" Cfg_printer.print_cfg cfg;
Cfg_printer.output_dot !Options.cfg_out cfg;
let fa = ConstIterator.iterate cfg in
let fb = SignIterator.iterate cfg in
Format.printf "@[<v 0>Failed asserts :@ %a@]" pp_asserts (ArcSet.inter fa fb) end
(* parses arguments to get filename *)
let main () =
let _ = Options.init () in
doit !Options.file
let _ = main ();

40
domains/constant.ml Normal file
View file

@ -0,0 +1,40 @@
open Naked
open Abstract_syntax_tree
module Constants : NAKED_VALUE_DOMAIN = struct
type t = Z.t
let const z = z
let rand z w = raise NeedTop (* We know rand is never called on singletons *)
let minus z = Z.neg z
let binary a b op = match op with
| AST_PLUS -> Z.add a b
| AST_MINUS -> Z.sub a b
| AST_MULTIPLY -> Z.mul a b
| AST_DIVIDE -> (try(Z.div a b)with Division_by_zero -> raise Absurd)
| AST_MODULO -> Z.rem a b
let is_only_zero z = Z.equal (Z.zero) z
let multiples_of z = if Z.equal Z.zero z then Z.zero else raise NeedTop
let divisors_of z = if Z.equal Z.zero z then Z.zero else raise NeedTop
let remainders z = if Z.equal Z.zero z then Z.zero else raise NeedTop
let convex_sym z = if Z.equal Z.zero z then Z.zero else raise NeedTop
let compatible z op = match op with
| AST_EQUAL -> z
| _ -> raise NeedTop
let compare z w op = match op with
| AST_EQUAL -> if Z.equal z w then z,w else raise Absurd
| AST_NOT_EQUAL -> if Z.equal z w then raise Absurd else z,w
| AST_LESS -> if Z.lt z w then z,w else raise Absurd
| AST_LESS_EQUAL -> if Z.leq z w then z,w else raise Absurd
| AST_GREATER -> if Z.gt z w then z,w else raise Absurd
| AST_GREATER_EQUAL -> if Z.geq z w then z,w else raise Absurd
let bwd_binary x y op r = if Z.equal (binary x y op) r then x,y else raise Absurd
let join x y = if Z.equal x y then x else raise NeedTop
let meet x y = if Z.equal x y then x else raise Absurd
let widen x y = if Z.equal x y then x else raise NeedTop
let narrow x y = if Z.equal x y then x else raise Absurd
let subset x y = Z.equal x y
let print out x = Z.pp_print out x
end

66
domains/domain.ml Normal file
View file

@ -0,0 +1,66 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
open! Cfg
(* Signature for the variables *)
module type VARS = sig
val support: var list
end
(*
Signature of abstract domains representing sets of envrionments
(for instance: a map from variable to their bounds).
*)
module type DOMAIN =
sig
(* type of abstract elements *)
(* an element of type t abstracts a set of mappings from variables
to integers
*)
type t
(* initial environment, with all variables initialized to 0 *)
val init: t
(* empty set of environments *)
val bottom: t
(* assign an integer expression to a variable *)
val assign: t -> var -> int_expr -> t
(* filter environments to keep only those satisfying the boolean expression *)
val guard: t -> bool_expr -> t
(* abstract join *)
val join: t -> t -> t
(* abstract meet *)
val meet: t -> t -> t
(* widening *)
val widen: t -> t -> t
(* narrowing *)
val narrow: t -> t -> t
(* whether an abstract element is included in another one *)
val subset: t -> t -> bool
(* whether the abstract element represents the empty set *)
val is_bottom: t -> bool
(* prints *)
val print: Format.formatter -> t -> unit
end

5
domains/dune Normal file
View file

@ -0,0 +1,5 @@
(library
(name domains)
(wrapped false)
(libraries libs zarith frontend)
(flags -w +a-4-6-7-9-27-29-32..42-44-45-48-50-60 ))

168
domains/naked.ml Normal file
View file

@ -0,0 +1,168 @@
open Abstract_syntax_tree
open Value_domain
exception NeedTop
exception Absurd
module type NAKED_VALUE_DOMAIN =
sig
type t
val const: Z.t -> t
val rand: Z.t -> Z.t -> t
val minus: t -> t
val binary: t -> t -> int_binary_op -> t
val is_only_zero: t -> bool
val multiples_of: t -> t
val divisors_of: t -> t
val remainders: t -> t
val convex_sym: t -> t
val compatible: t -> compare_op -> t (* returns the arguments possibly on the right of a comp w t*)
val compare: t -> t -> compare_op -> (t*t)
val bwd_binary: t -> t -> int_binary_op -> t -> (t*t)
val join: t -> t -> t
val meet: t -> t -> t
val widen: t -> t -> t
val narrow: t -> t -> t
val subset: t -> t -> bool
val print: Format.formatter -> t -> unit
end
module AddTopBot (N : NAKED_VALUE_DOMAIN) : VALUE_DOMAIN =
struct
type t = Bot | Top | V of N.t
let top = Top
let bottom = Bot
let is_bottom a = match a with
| Bot -> true
| _ -> false
let is_top a = match a with
| Top -> true
| _ -> false
let const c = try V (N.const c) with NeedTop -> Top
let rand a b = try (if Z.equal a b then
V (N.const a)
else (if Z.leq a b then V (N.rand a b) else Bot)) with NeedTop -> Top
let unary a op = try (match op with
| AST_UNARY_PLUS -> a
| AST_UNARY_MINUS -> (match a with
| Top -> Top
| Bot -> Bot
| V t -> V (N.minus t)) ) with NeedTop -> Top
let binary a b op = try( if (is_bottom a || is_bottom b) then (Bot)
else match op with
| AST_PLUS -> if (is_top a || is_top b) then Top else
let V a', V b' = a, b in V (N.binary a' b' AST_PLUS)
| AST_MINUS -> if (is_top a || is_top b) then Top else
let V a', V b' = a, b in V (N.binary a' b' AST_MINUS)
| AST_MULTIPLY -> (match a, b with
| Top, Top -> Top
| Top, V x | V x, Top -> V (N.multiples_of x)
| V x, V y -> V(N.binary x y AST_MULTIPLY))
| AST_DIVIDE -> (match a, b with
| Top, Top -> Top
| Top, V x -> if N.is_only_zero x then Bot else Top
| V x, Top -> V(N.divisors_of x)
| V x, V y -> if N.is_only_zero y then Bot else V(N.binary x y AST_DIVIDE))
| AST_MODULO -> (match a, b with
| Top, Top -> Top
| Top, V x -> if N.is_only_zero x then Bot else V(N.convex_sym x) (* convex symetric hull *)
| V x, Top -> V(N.remainders x)
| V x, V y -> if N.is_only_zero y then Bot else V(N.binary x y AST_MODULO)) ) with NeedTop -> Top
let compare a b op = match a, b with
| Bot, _ | _, Bot -> Bot, Bot
| Top, Top -> Top, Top (* We are non-relational ! *)
| V x, Top -> V x, (try(V (N.compatible x op))with NeedTop->Top)(*We can't learn anything comparing to Top*)
| Top, V x -> (try(V (N.compatible x (reverse op)))with NeedTop->Top), V x
| V x, V y -> try( let a', b' = (N.compare x y op) in V a', V b' )with Absurd -> Bot,Bot
let bwd_unary x op r =
match r with
| Top -> Top
| Bot -> Bot
| V r' -> (match x with
| Top -> (match op with
| AST_UNARY_PLUS -> r
| AST_UNARY_MINUS -> V(N.minus r'))
| Bot -> Bot
| V x' -> (match op with
| AST_UNARY_PLUS -> (try(V (N.meet x' r') )with Absurd -> Bot)
| AST_UNARY_MINUS -> try( V(N.meet x' (N.minus r')))with Absurd->Bot))
let bwd_binary x y op r =
match r with
| Top -> x, y
| Bot -> (match op with
| AST_DIVIDE | AST_MODULO -> x, (try (V (N.const Z.zero) )with NeedTop->Top)
| _ -> x, y (* This can only happen if one of x or y was already Bot *)
)
| V r' -> (match x, y with
| Bot, _| _, Bot -> x,y
| Top, Top -> x, y (*TODO: add some trivialities like a / b = 0 implies a == 0 *)
| V a, Top -> (match op with
| AST_PLUS -> (V a, V (N.binary r' a AST_MINUS))
| AST_MINUS -> (V a, V (N.binary a r' AST_MINUS))
(*
If a can't be null, the values described by b are exactly the values taken by r'/a
(there aren't any rounding issues because r' = ab IMPLIES b = r'/a.)
If a and r' can be null, we can't deduce anything.
If a can be null but r' can't, then b can take any value r'/a can (when a != 0)
*)
| AST_MULTIPLY -> let an, rn = N.subset (N.const Z.zero) a, N.subset (N.const Z.zero) r' in
(match an, rn with
| false, _ -> (V a, V (N.binary r' a AST_DIVIDE))
| true, false -> if N.is_only_zero a then (V a, Bot) else V a, V (N.binary r' a AST_DIVIDE)
| true, true -> (V a, Top))
| AST_DIVIDE | AST_MODULO -> x,y) (* divide has rounding issues, modulo makes my head hurt *)
| Top, V a -> (match op with
| AST_PLUS -> (V (N.binary r' a AST_MINUS), V a)
| AST_MINUS -> (V (N.binary r' a AST_PLUS), V a)
| AST_MULTIPLY -> let an, rn = N.subset (N.const Z.zero) a, N.subset (N.const Z.zero) r' in
(match an, rn with
| false, _ -> (V a, V (N.binary r' a AST_DIVIDE))
| true, false -> if N.is_only_zero a then (V a, Bot) else V a, V (N.binary r' a AST_DIVIDE)
| true, true -> (V a, Top))
| AST_DIVIDE | AST_MODULO -> x,y)
| V a, V b -> try( let a',b' = (N.bwd_binary a b op r') in V a', V b' )with Absurd->(Bot,Bot) )
let join a b = try (match a, b with
| Top, x | x, Top -> Top
| Bot, x | x, Bot -> x
| V a', V b' -> V(N.join a' b') )with NeedTop -> Top
let meet a b = match a, b with
| Bot, x | x, Bot -> Bot
| Top, x | x, Top -> x
| V a', V b' -> try( V(N.meet a' b') )with Absurd -> Bot
let widen a b = try( match a, b with
| Bot, x | x, Bot -> x
| Top, x | x, Top -> Top
| V a', V b' -> V(N.widen a' b') )with NeedTop->Top
let narrow a b = match a, b with
| Bot, x | x, Bot -> Bot
| Top, x | x, Top -> x
| V a', V b' -> try( V(N.narrow a' b') )with Absurd -> Bot
let subset a b = match a, b with
| Bot, b -> true
| b, Bot -> false
| b, Top -> true
| Top, b -> false
| V a', V b' -> (N.subset a' b')
let print out a =
match a with
| Top -> Format.fprintf out "T"
| Bot -> Format.fprintf out "B"
| V a' -> N.print out a'
end

87
domains/sign.ml Normal file
View file

@ -0,0 +1,87 @@
open Naked
open Abstract_syntax_tree
module Signs : NAKED_VALUE_DOMAIN = struct
type t = N | Z | P (*Negative/Zero/Positive (signs include 0)*)
let const z = if (Z.equal Z.zero z) then Z else
(if Z.lt z Z.zero then N else P)
let rand a b = if Z.leq b Z.zero then N
else (if Z.geq a Z.zero then P else raise NeedTop) (*We know a < b*)
let minus a = match a with
| N -> P | Z -> Z | P -> N
let rec binary a b op = match op with
| AST_PLUS -> (match a, b with
| P, P | P, Z | Z, P -> P
| Z, Z -> Z
| _ -> N)
| AST_MINUS -> binary a (minus b) AST_PLUS
| AST_MULTIPLY -> (match a, b with
| P, P | N, N -> P
| Z, _ | _, Z -> Z
| _ -> N)
| AST_DIVIDE -> (match a, b with
| _, Z -> raise Absurd
| _ -> binary a b AST_MULTIPLY)
| AST_MODULO -> a
let is_only_zero a = match a with
| Z -> true | _ -> false
let multiples_of a = match a with
| Z -> Z | _ -> raise NeedTop
let divisors_of a = match a with
| Z -> Z | _ -> raise NeedTop
let remainders a = a
let convex_sym a = match a with
| Z -> Z | _ -> raise NeedTop
let compatible a op = match op with
| AST_EQUAL -> a
| AST_NOT_EQUAL -> raise NeedTop
| AST_LESS | AST_LESS_EQUAL -> if a == P || a == Z then P else raise NeedTop
| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then N else raise NeedTop
let compare a b op = match op with
| AST_EQUAL -> if a <> b then Z, Z else a, b
| AST_NOT_EQUAL -> if a == b && a == Z then raise Absurd else a, b
| AST_LESS | AST_LESS_EQUAL -> if b == N || b == Z then
(match a with | P -> Z | Z -> Z | N -> N), b
else a, b (*if b is P then we learn nothing*)
| AST_GREATER | AST_GREATER_EQUAL -> if a == N || a == Z then
a, (match b with | P -> Z | Z -> Z | N -> N)
else a,b
let meet x y = match x,y with
|P, N | N, P -> raise Absurd
|Z, _ | _, Z -> Z
|N, N | P, P -> x
let rec bwd_binary a b op r = match op with
| AST_PLUS -> (match r with
| P -> (if a <> P && b <> P then Z,Z else a,b)
| N -> (if a <> N && b <> N then Z,Z else a,b)
| Z -> if a == b then Z,Z else a,b)
| AST_MINUS -> let a', nb' = bwd_binary a (minus b) AST_PLUS r in (a', minus nb')
| AST_MULTIPLY -> (match r with
| Z -> a,b (*all products must be zero, so one is Z, but we don't know which...*)
| P -> (match a, b with
| P, P | N, N -> a,b
| Z, _ | _, Z -> a,b
| N, P | P, N -> a,b) (*all products are 0, so at least one is Z, but...*)
| N -> let a', nb' = bwd_binary a (minus b) AST_MULTIPLY (minus r) in (a', minus nb'))
| AST_DIVIDE -> if b == Z then raise Absurd else (*Here zeros don't bother us!*)
(match r with
| Z -> Z,b
| P -> b,b
| N -> b, minus b)
| AST_MODULO -> if b == Z then raise Absurd else
(meet a r,b)
let join x y = match x,y with
| P, N | N, P -> raise NeedTop
| Z, a | a, Z -> a
| N, N | P, P -> x
let widen x y = join x y
let narrow x y = meet x y
let subset x y = x == y || (x == Z)
let print out x = match x with
| Z -> Format.fprintf out "0"
| N -> Format.fprintf out "<=0"
| P -> Format.fprintf out ">=0"
end

207
domains/value_domain.ml Normal file
View file

@ -0,0 +1,207 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Signature of abstract domains representing sets of integers
(for instance: constants or intervals).
*)
open Abstract_syntax_tree
module type VALUE_DOMAIN =
sig
(* type of abstract elements *)
(* an element of type t abstracts a set of integers *)
type t
(* unrestricted value: [-oo,+oo] *)
val top: t
(* bottom value: empty set *)
val bottom: t
(* constant: {c} *)
val const: Z.t -> t
(* interval: [a,b] *)
val rand: Z.t -> Z.t -> t
(* unary operation *)
val unary: t -> int_unary_op -> t
(* binary operation *)
val binary: t -> t -> int_binary_op -> t
(* comparison *)
(* [compare x y op] returns (x',y') where
- x' abstracts the set of v in x such that v op v' is true for some v' in y
- y' abstracts the set of v' in y such that v op v' is true for some v in x
i.e., we filter the abstract values x and y knowing that the test is true
a safe, but not precise implementation, would be:
compare x y op = (x,y)
*)
val compare: t -> t -> compare_op -> (t * t)
(* backards unary operation *)
(* [bwd_unary x op r] return x':
- x' abstracts the set of v in x such as op v is in r
i.e., we fiter the abstract values x knowing the result r of applying
the operation on x
*)
val bwd_unary: t -> int_unary_op -> t -> t
(* backward binary operation *)
(* [bwd_binary x y op r] returns (x',y') where
- x' abstracts the set of v in x such that v op v' is in r for some v' in y
- y' abstracts the set of v' in y such that v op v' is in r for some v in x
i.e., we filter the abstract values x and y knowing that, after
applying the operation op, the result is in r
*)
val bwd_binary: t -> t -> int_binary_op -> t -> (t * t)
(* set-theoretic operations *)
val join: t -> t -> t
val meet: t -> t -> t
(* widening *)
val widen: t -> t -> t
(* narrowing *)
val narrow: t -> t -> t
(* subset inclusion of concretizations *)
val subset: t -> t -> bool
(* check the emptiness of the concretization *)
val is_bottom: t -> bool
(* print abstract element *)
val print: Format.formatter -> t -> unit
end
open Cfg
open Domain
module NonRelational (V : VALUE_DOMAIN) : DOMAIN = struct
module VMap = VarMap
type t = Bot | E of V.t VMap.t
let init = E VMap.empty (* Nonpresent variables are 0 *)
let bottom = Bot
let print out env = match env with
| Bot -> Format.fprintf out "@[<h 0>Bot@]"
| E map -> begin Format.fprintf out "@[<h 0>{";
VMap.iter (fun varid val1 -> Format.fprintf out "%a : %a @ " Cfg_printer.print_var varid V.print val1) map;
Format.fprintf out "}@]"; end
let rec compute e expr = match expr with
| CFG_int_unary (uop, aux) -> V.unary (compute e aux) uop
| CFG_int_binary (bop, aux1, aux2) -> V.binary (compute e aux1) (compute e aux2) bop
| CFG_int_var v -> (try ( VMap.find v e )with Not_found -> V.const Z.zero)
| CFG_int_const c -> V.const c
| CFG_int_rand (c1, c2) -> V.rand c1 c2
let assign env v expr = match env with
| Bot -> Bot
| E envmap -> E (VMap.add v (compute envmap expr) envmap)
let join env1 env2 = match (env1, env2) with
| Bot, x | x, Bot -> x
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.join x (V.const Z.zero))
| Some x, Some y -> Some (V.join x y)) map1 map2)
let meet env1 env2 = match(env1, env2) with
| Bot, x | x, Bot -> Bot
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.meet x (V.const Z.zero))
| Some x, Some y -> Some (V.meet x y)) map1 map2)
type hc4_tree = HC4_int_unary of int_unary_op * hc4_tree * V.t
| HC4_int_binary of int_binary_op * hc4_tree * hc4_tree * V.t
| HC4_int_var of var * V.t
| HC4_int_const of Z.t * V.t
| HC4_int_rand of Z.t*Z.t * V.t
let get_abst hc4 = (match hc4 with
| HC4_int_unary (_,_,v) -> v
| HC4_int_binary (_,_,_,v) -> v
| HC4_int_var (_,v) -> v
| HC4_int_const (_,v) -> v
| HC4_int_rand (_,_,v) -> v)
let rec build_HC4 iexp mapenv = match iexp with
| CFG_int_unary (uop, iexp') -> let sub = build_HC4 iexp' mapenv in HC4_int_unary (uop, sub, (V.unary (get_abst sub) uop))
| CFG_int_binary (bop, iexp1, iexp2) -> let sub1, sub2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
HC4_int_binary (bop,sub1,sub2,(V.binary (get_abst sub1) (get_abst sub2) bop))
| CFG_int_var v -> let abst = (try( VMap.find v mapenv )with Not_found -> V.const Z.zero) in HC4_int_var (v, abst)
| CFG_int_const z -> let abst = V.const z in HC4_int_const (z, abst)
| CFG_int_rand (a, b) -> let abst = V.rand a b in HC4_int_rand (a,b,abst)
let rec revise_HC4 tree mapenv newval = match tree with
| HC4_int_unary (uop, sub, abst) -> revise_HC4 sub mapenv (V.bwd_unary (get_abst sub) uop (V.meet abst newval))
| HC4_int_binary (bop, sub1, sub2, abst) -> let refined1, refined2 = V.bwd_binary (get_abst sub1) (get_abst sub2) bop (V.meet abst newval) in
meet (revise_HC4 sub1 mapenv refined1) (revise_HC4 sub2 mapenv refined2)
| HC4_int_var (v, abst) -> E (VMap.add v (V.meet abst newval) mapenv)
| HC4_int_const (z,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
| HC4_int_rand (a,b,abst) -> if( V.is_bottom (V.meet abst newval) ) then Bot else E mapenv
let rec guard_noneg env boolexp = match boolexp with
| CFG_bool_unary (_, _) -> failwith "We were supposed to remove negations !!"
| CFG_bool_binary (AST_AND, exp1, exp2) -> meet (guard_noneg env exp1) (guard_noneg env exp2)
| CFG_bool_binary (AST_OR, exp1, exp2) -> join (guard_noneg env exp1) (guard_noneg env exp2)
| CFG_bool_const (b) -> if b then env else Bot
| CFG_bool_rand -> env
| CFG_compare (cop, iexp1, iexp2) -> match env with
| Bot -> Bot
| E mapenv -> let hc4_1, hc4_2 = build_HC4 iexp1 mapenv, build_HC4 iexp2 mapenv in
let newval1, newval2 = V.compare (get_abst hc4_1) (get_abst hc4_2) cop in (
meet (revise_HC4 hc4_1 mapenv newval1) (revise_HC4 hc4_2 mapenv newval2) )
let guard env boolexp = guard_noneg env (rm_negations boolexp)
let widen env1 env2 = match (env1, env2) with
| Bot, x | x, Bot -> x
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.widen x (V.const Z.zero))
| Some x, Some y -> Some (V.widen x y)) map1 map2)
let narrow env1 env2 = match(env1, env2) with
| Bot, x | x, Bot -> Bot
| E map1, E map2 ->
E (VMap.merge (fun v val1 val2 -> match val1, val2 with
| None, None -> None
| None, Some x | Some x, None -> Some (V.narrow x (V.const Z.zero))
| Some x, Some y -> Some (V.narrow x y)) map1 map2)
let subset env1 env2 = match env1, env2 with
| Bot, _ -> true
| _, Bot -> false
| E map1, E map2 -> let b1 = VMap.for_all (fun varid val1 -> match VMap.find_opt varid map2 with
| None -> V.subset val1 (V.const Z.zero)
| Some val2 -> V.subset val1 val2) map1 in
let b2 = VMap.for_all (fun varid val2 -> match VMap.find_opt varid map1 with
| None -> V.subset (V.const Z.zero) val2
| Some val1 -> V.subset val1 val2) map2 in
b1 && b2
let is_bottom env = match env with
| Bot -> true
| E map -> VMap.exists (fun varid val1 -> V.is_bottom val1) map
end

4
dune Normal file
View file

@ -0,0 +1,4 @@
(executable
(name analyzer)
(libraries libs frontend zarith iterator domains)
(flags (:standard -warn-error -A)))

2
dune-project Normal file
View file

@ -0,0 +1,2 @@
(lang dune 2.7)
(using menhir 2.1)

11
examples/bool/assert_false.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(false); //@KO
}

12
examples/bool/assert_false_false.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(false); //@KO
assert(false); //This assertion should not fail
}

11
examples/bool/assert_not_false.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(!false);
}

11
examples/bool/assert_not_rand.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(!brand); //@KO
}

11
examples/bool/assert_not_true.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(!true); //@KO
}

11
examples/bool/assert_rand.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(brand); //@KO
}

12
examples/bool/assert_rand_false.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(brand); //@KO
assert(false); //@KO
}

11
examples/bool/assert_true.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
assert(true);
}

13
examples/constant/constant_add.c Normal file
View file

@ -0,0 +1,13 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
int y = 12;
void main(){
int i = 10;
int j = -2;
int x = i + j;
assert(x == 8);
}

11
examples/constant/constant_cmp.c Normal file
View file

@ -0,0 +1,11 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(1, 3);
assert(i == 1 || i == 3); //@KO
}

13
examples/constant/constant_cmp_add.c Normal file
View file

@ -0,0 +1,13 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
int j = rand(1, 2);
if( i + j == 1)
assert(j == 1);
}

14
examples/constant/constant_cmp_mul.c Normal file
View file

@ -0,0 +1,14 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
int j = rand(0, 2);
int x = 0;
if( i * j == x )
assert(j == 0); //@KO
}

12
examples/constant/constant_cmp_simple.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
int j = 42;
assert(i == j); //@KO
}

13
examples/constant/constant_div.c Normal file
View file

@ -0,0 +1,13 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 9;
int j = -2;
int x = i / j; // We follow towards zero convention
assert(x == -4);
}

13
examples/constant/constant_div_zero.c Normal file
View file

@ -0,0 +1,13 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 9;
int j = 0;
int x = i / j; // Dividing by zero does not raise an error;
assert(1 == 2); // test the abstract value is bottom
}

13
examples/constant/constant_mul_zero.c Normal file
View file

@ -0,0 +1,13 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
int j = rand(1, 2);
int x = i * j;
assert(x == 0);
}

13
examples/constant/constant_rem.c Normal file
View file

@ -0,0 +1,13 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 9;
int j = -2;
int x = i % j; // a % b = a - b*(a/b)
assert(x == 1);
}

12
examples/constant_loop/constant_loop_1.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
for(i = 0; i != 10; i++);
assert(i == 10);
}

12
examples/constant_loop/constant_loop_2.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
while(true) i++;
assert(1 == 2);
}

12
examples/constant_loop/constant_loop_3.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 1;
while(rand(0, 1)==0) i++;
assert(i == 0); //@KO
}

16
examples/interval/interval_add.c Normal file
View file

@ -0,0 +1,16 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(0, 3);
int j = rand(-10, 20);
int x = i + j;
assert(x >= -10);
assert(x <= 23);
assert(x != -10); //@KO
assert(x != 23); //@KO
}

17
examples/interval/interval_cmp_eq.c Normal file
View file

@ -0,0 +1,17 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(0, 42);
int j = rand(-10, 20);
if (i == j){
assert(i <= 20);
assert(j >= 0);
assert(i != 20); //@KO
assert(j != 0); //@KO
}
}

17
examples/interval/interval_cmp_gt_add.c Normal file
View file

@ -0,0 +1,17 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(1, 23);
int j = rand(5, 42);
if( i + j > 60){
assert(i >= 19);
assert(j >= 38);
assert(i != 19); //@KO
assert(j != 38); //@KO
}
}

12
examples/interval/interval_cmp_leq.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(0, 23);
if (i <= 10) assert( i <= 12);
if (i < 0) assert(1 == 0);
}

17
examples/interval/interval_cmp_leq2.c Normal file
View file

@ -0,0 +1,17 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(1, 23);
int j = rand(5, 42);
if( i >= j){
assert(i >= 5);
assert(j <= 23);
assert(i != 5); //@KO
assert(j != 23); //@KO
}
}

14
examples/interval/interval_cmp_simple.c Normal file
View file

@ -0,0 +1,14 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(-2, 42);
assert(i <= 42);
assert(i >= -2);
assert(i != 42); //@KO
assert(i != -2); //@KO
}

20
examples/interval/interval_goto.c Normal file
View file

@ -0,0 +1,20 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
if(brand){ goto L1; }
L0: // performing a widening here loose all information
goto LF;
L1:
if(brand) { i += 1; } else { i -= 1; } // i in [-1; 1]
goto L0;
LF:
assert(i <= 1);
assert(i >= -1);
}

16
examples/interval/interval_mul.c Normal file
View file

@ -0,0 +1,16 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = rand(0, 3);
int j = rand(-10, 20);
int x = i * j;
assert(x >= -30);
assert(x <= 60);
assert(x != -30); //@KO
assert(x != 60); //@KO
}

12
examples/interval_loop/interval_loop.c Normal file
View file

@ -0,0 +1,12 @@
/*
* Cours "Sémantique et Application à la Vérification de programmes"
*
* Josselin Giet 2021
* Ecole normale supérieure, Paris, France / CNRS / INRIA
*/
void main(){
int i = 0;
for(i = 0; i < 10; i++);
assert(i >= 10);
}

225
frontend/abstract_syntax_tree.ml Normal file
View file

@ -0,0 +1,225 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Definition of the abstract syntax trees output by the parser.
*)
(* position in the source file, we use ocamllex's default type *)
type position = Lexing.position
let position_unknown = Lexing.dummy_pos
(* extents are pairs of positions *)
type extent = position * position (* start/end *)
let extent_unknown = (position_unknown, position_unknown)
(* Many parts of the syntax are tagged with an extent indicating which
part of the parser-file corresponds to the sub-tree.
This is very useful for interesting error reporting!
*)
type 'a ext = 'a * extent
(* variable identifiers are string *)
type id = string
(* types of variables: only int for now *)
type typ =
(* mathematical integers, in Z *)
| AST_TYP_INT
(* unary expression operators *)
type int_unary_op =
| AST_UNARY_PLUS (* +e *)
| AST_UNARY_MINUS (* -e *)
type bool_unary_op =
| AST_NOT (* !e logical negation *)
(* binary expression operators *)
type int_binary_op =
| AST_PLUS (* e + e *)
| AST_MINUS (* e - e *)
| AST_MULTIPLY (* e * e *)
| AST_DIVIDE (* e / e *)
| AST_MODULO (* e % e *)
type compare_op =
| AST_EQUAL (* e == e *)
| AST_NOT_EQUAL (* e != e *)
| AST_LESS (* e < e *)
| AST_LESS_EQUAL (* e <= e *)
| AST_GREATER (* e > e *)
| AST_GREATER_EQUAL (* e >= e *)
let reverse c = match c with
| AST_LESS -> AST_GREATER
| AST_GREATER -> AST_LESS
| AST_LESS_EQUAL -> AST_GREATER_EQUAL
| AST_GREATER_EQUAL -> AST_LESS_EQUAL
| x -> x
let negate c = match c with
| AST_LESS -> AST_GREATER_EQUAL
| AST_GREATER -> AST_LESS_EQUAL
| AST_LESS_EQUAL -> AST_GREATER
| AST_GREATER_EQUAL -> AST_LESS
| AST_EQUAL -> AST_NOT_EQUAL
| AST_NOT_EQUAL -> AST_EQUAL
type bool_binary_op =
| AST_AND (* e && e *)
| AST_OR (* e || e *)
(* expressions *)
type int_expr =
(* unary operation *)
| AST_int_unary of int_unary_op * (int_expr ext)
(* binary operation *)
| AST_int_binary of int_binary_op * (int_expr ext) * (int_expr ext)
(* variable use *)
| AST_int_identifier of id ext
(* constants (integers are still in their string representation) *)
| AST_int_const of string ext
(* non-deterministic choice between two integers *)
| AST_int_rand of (string ext) (* lower bound *) *
(string ext) (* upper bound *)
(* calls a function with arguments and return value *)
| AST_expr_call of (id ext) (* function name *) *
(int_expr ext list) (* arguments *)
type bool_expr =
(* unary operation *)
| AST_bool_unary of bool_unary_op * (bool_expr ext)
(* binary operation *)
| AST_bool_binary of bool_binary_op * (bool_expr ext) * (bool_expr ext)
| AST_compare of compare_op * (int_expr ext) * (int_expr ext)
(* constants *)
| AST_bool_const of bool
(* non-deterministic choice *)
| AST_bool_rand
(* statements *)
type stat =
(* block of statements { ... } *)
| AST_block of stat ext list
(* assignment lvalue = expr *)
| AST_assign of (id ext) * (int_expr ext)
(* assignment lvalue op= expr *)
| AST_assign_op of (id ext) * int_binary_op * (int_expr ext)
(* increment lvalue += cst *)
| AST_increment of (id ext) * int
(* if-then-else; the else branch is optional *)
| AST_if of (bool_expr ext) (* condition *) *
(stat ext) (* then branch *) *
(stat ext option) (* optional else *)
(* while loop *)
| AST_while of (bool_expr ext) (* condition *) *
(stat ext) (* body *)
(* for loop *)
| AST_for of (stat ext list) (* init *) *
(bool_expr ext option) (* condition *) *
(stat ext list) (* increment *) *
(stat ext) (* body *)
(* assertion: fail if the boolean expression does not hold *)
| AST_assert of bool_expr ext
(* declaration of a local variable, live until the end of the current block *)
| AST_local_decl of var_decl ext
(* calls a function with arguments (no return value) *)
| AST_stat_call of (id ext) (* function name *) *
(int_expr ext list) (* arguments *)
(* exits form the function, with optional return value *)
| AST_return of int_expr ext option
(* exits from the innermost while loop *)
| AST_break of unit ext
(* empty instruction: do nothing *)
| AST_SKIP
(* go to a label in the function *)
| AST_goto of id ext
(* destination of a goto *)
| AST_label of id ext
(* declare some variables with a common type *)
and var_decl = (typ ext) (* type *) * (var_init list) (* variable list *)
(* each declared variable has an optional initializer *)
and var_init = (id ext) (* declared variable *) *
(int_expr ext option) (* initializer *)
(* function declaration
(no return type, all functions return void)
*)
type fun_decl =
{ (* function name *)
fun_name: id ext;
(* formal arguments, with type *)
fun_args: ((typ ext) * (id ext)) list;
(* type of the returned value, if any *)
fun_typ: typ option ext;
(* function body *)
fun_body: stat ext list;
(* function location *)
fun_ext: extent;
}
(* top-level statements *)
type toplevel =
(* global variable declaration *)
| AST_global_decl of var_decl ext
(* function declaration *)
| AST_fun_decl of fun_decl ext
(* a program is a list of top-level statements *)
type prog = toplevel list ext

152
frontend/add_assert_div.ml Normal file
View file

@ -0,0 +1,152 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
open Abstract_syntax_tree
let rec aux_int acc e =
match fst e with
| AST_int_identifier _
| AST_int_const _
| AST_int_rand (_, _) -> acc
| AST_int_unary (_, e) -> aux_int acc e
| AST_int_binary (AST_DIVIDE, e1, e2)
| AST_int_binary (AST_MODULO, e1, e2) ->
let acc = aux_int acc e1 in
let acc = aux_int acc e2 in
e2::acc
| AST_int_binary (_ , e1, e2) ->
let acc = aux_int acc e1 in
let acc = aux_int acc e2 in
acc
| AST_expr_call (_, args) ->
List.fold_left aux_int acc (List.rev args)
let rec aux_bool acc b =
match fst b with
| AST_bool_const _
| AST_bool_rand -> acc
| AST_bool_unary (_, b) -> aux_bool acc b
| AST_bool_binary (_, b1, b2) ->
let acc = aux_bool acc b1 in
let acc = aux_bool acc b2 in
acc
| AST_compare (_, e1, e2) ->
let acc = aux_int acc e1 in
let acc = aux_int acc e2 in
acc
(** [find_div_int expr] returns the list of integer expressions found as
divisors in the integer expression [expr].
the first elements of the list are the lower in the AST *)
let find_div_int (e: int_expr ext) : int_expr ext list =
aux_int [] e |> List.rev
(** [find_div_bool b_expr] returns the list of integer expressions found as
divisors in the boolean expression [b_expr].
the first elements of the list are the lower in the AST *)
let find_div_bool (b: bool_expr ext) : int_expr ext list =
aux_bool [] b |> List.rev
(** [create_assertions e] retuns a statment assrting that [e != 0].
All locations informations are found in [e]. *)
let create_assertions (e: int_expr ext) : stat ext =
let ext = snd e in
let zero = AST_int_const ("0", ext), ext in
let be = AST_compare (AST_NOT_EQUAL, e, zero), ext in
let s = AST_assert be in
s, ext
(** [add_assertions_stat s] returns (a bloc of) statements containing [s] and
all necessary assertions. *)
let rec add_assertions_stat (s: stat ext): stat ext list =
let ext = snd s in
match fst s with
| AST_label _
| AST_break _
| AST_SKIP
| AST_increment (_, _)
| AST_return None
| AST_goto _ -> [s]
| AST_local_decl ((typ, vari), ext_decl) ->
let aux (vari: var_init): stat ext list =
match snd vari with
| None -> [AST_local_decl ((typ, [vari]), ext_decl), ext]
| Some (e, ext_e) ->
let exprs = find_div_int (e, ext_e) in
let stats = List.map create_assertions exprs in
stats@[AST_local_decl ((typ, [vari]), ext_decl), ext_decl] in
let stats = List.map aux vari |> List.flatten in
stats
| AST_block b ->
let stats = List.map add_assertions_stat b |> List.flatten in
[AST_block stats, ext]
| AST_assign (_, expr) ->
let exprs = find_div_int expr in
let stats = List.map create_assertions exprs in
stats@[s]
| AST_assign_op (_, _, expr) ->
let exprs = find_div_int expr in
let stats = List.map create_assertions exprs in
stats@[s]
| AST_if (b_expr, s1, s2) ->
let exprs = find_div_bool b_expr in
let s =
let s1 = AST_block (add_assertions_stat s1), snd s1 in
let s2 = Option.map (fun s -> AST_block (add_assertions_stat s), snd s) s2 in
AST_if (b_expr, s1, s2), ext in
let stats = List.map create_assertions exprs in
stats@[s]
| AST_while (b_expr, s1) ->
let exprs = find_div_bool b_expr in
let stats = List.map create_assertions exprs in
let s =
let s1 = add_assertions_stat s1 in
let s1 = AST_block (s1@stats), ext in
AST_while (b_expr, s1), ext in
stats@[s]
| AST_for (stats_init, Some b_expr, stats_inc, body) ->
let exprs = find_div_bool b_expr in
let stats = List.map create_assertions exprs in
let stats_init = List.map add_assertions_stat stats_init |> List.flatten in
let stats_init = stats_init@stats in
let body = AST_block (add_assertions_stat body), snd body in
let stats_inc = List.map add_assertions_stat stats_inc |> List.flatten in
let stats_inc = stats_inc@stats in
let s = AST_for (stats_init, Some b_expr, stats_inc, body), ext in
[s]
| AST_for (stats_init, None, stats_inc, body) ->
let stats_init = List.map add_assertions_stat stats_init |> List.flatten in
let body = AST_block (add_assertions_stat body), snd body in
let stats_inc = List.map add_assertions_stat stats_inc |> List.flatten in
let s = AST_for (stats_init, None, stats_inc, body), ext in
[s]
| AST_assert (b_expr) ->
let exprs = find_div_bool b_expr in
let stats = List.map create_assertions exprs in
stats@[s]
| AST_stat_call (_, args) ->
let exprs = List.map find_div_int args |> List.flatten in
let stats = List.map create_assertions exprs in
stats@[s]
| AST_return (Some expr) ->
let exprs = find_div_int expr in
let stats = List.map create_assertions exprs in
stats@[s]
(** [add_assertions p] returns the program [p] with all division guarded with
non-null assertions. *)
let add_assertions (p: prog) : prog =
let aux (fdecl: fun_decl): fun_decl =
let fun_body = List.map add_assertions_stat fdecl.fun_body |> List.flatten in
{ fdecl with fun_body } in
let aux: toplevel -> toplevel = function
| AST_global_decl _ as x -> x
| AST_fun_decl (fdecl, ext) ->
AST_fun_decl (aux fdecl, ext) in
let decls, ext = p in
List.map aux decls, ext

261
frontend/cfg.ml Normal file
View file

@ -0,0 +1,261 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Control-flow graphs (CFG).
The CFG representation is much simpler than the tree representation:
- complex expressions are compiled into a sequence of simpler ones;
- variables are desambiguated;
- the binding of formal and actual arguments is explicit (as assignments);
- the control structures are translated into jumps between nodes.
*)
open Abstract_syntax_tree
(* Variables *)
(* ********* *)
(* Each global variable, local variable and function parameter is associated a
var structure.
We use unique identifiers (integers) to distinguish between variables declared
at different point with the same name.
*)
type var =
{ var_id: int; (* unique variable identifier *)
var_name: id; (* original name, in the program *)
var_type: typ; (* variable type *)
var_pos: extent; (* position of the variable declaration *)
}
(* Expressions *)
(* *********** *)
(*
Expressions in the CFG are call-free. Calls are extracted during the
translation form AST to CFG and put in separate instructions
(possibly introducing temporary variables).
To simplify, we remove some all location information (ext) in expressions.
Variable scoping is resolved in the translation: variables in CFG
expressions are var structures instead of plain strings.
*)
type int_expr =
(* unary operation *)
| CFG_int_unary of int_unary_op * int_expr
(* binary operation *)
| CFG_int_binary of int_binary_op * int_expr * int_expr
(* variable use *)
| CFG_int_var of var
(* constants *)
| CFG_int_const of Z.t
(* non-deterministic choice between two integers *)
| CFG_int_rand of Z.t (* lower bound *) * Z.t (* upper bound *)
type bool_expr =
(* unary operation *)
| CFG_bool_unary of bool_unary_op * bool_expr
(* binary operation *)
| CFG_bool_binary of bool_binary_op * bool_expr * bool_expr
| CFG_compare of compare_op * int_expr * int_expr
(* constants *)
| CFG_bool_const of bool
(* non-deterministic choice *)
| CFG_bool_rand
let rec rm_negations (boolexp : bool_expr) = match boolexp with
| CFG_bool_unary (AST_NOT, CFG_bool_unary (AST_NOT, be1)) -> be1
| CFG_bool_unary (AST_NOT, CFG_bool_binary (AST_AND, be1, be2)) ->
CFG_bool_binary (AST_OR, rm_negations (CFG_bool_unary (AST_NOT, be1)),
rm_negations (CFG_bool_unary (AST_NOT, be2)))
| CFG_bool_unary (AST_NOT, CFG_bool_binary (AST_OR, be1, be2)) ->
CFG_bool_binary (AST_AND, rm_negations (CFG_bool_unary (AST_NOT, be1)),
rm_negations (CFG_bool_unary (AST_NOT, be2)))
| CFG_bool_unary (AST_NOT, CFG_compare (cop, iexpr1, iexpr2)) ->
CFG_compare (negate cop, iexpr1, iexpr2)
| CFG_bool_unary (AST_NOT, CFG_bool_const (true)) -> CFG_bool_const (false)
| CFG_bool_unary (AST_NOT, CFG_bool_const (false)) -> CFG_bool_const (true)
| CFG_bool_unary (AST_NOT, CFG_bool_rand) -> CFG_bool_rand
| x -> x
(* Instructions *)
(* ************ *)
(*
Each arc between two CFG node is labelled with an instruction to
execute to go from the source node to the destination node.
CFG instructions are thus very simple.
*)
type inst =
(* go to the destination node doing nothing *)
(* the string argument is just for printing, it give some
information on the original instruction that caused the skip
*)
| CFG_skip of string
(* assignment *)
| CFG_assign of var * int_expr
(* guard: test that must be satisfied to make a transition *)
| CFG_guard of bool_expr
(* assertion: it is an error if the test is not satisfied *)
| CFG_assert of bool_expr ext
(* function call *)
| CFG_call of func
(* Functions *)
(* ********* *)
(*
Functions have a single entry node and a single exit node.
The execution always starts at the entry node, and the function always
returns through the return node.
A return instruction inside the function is compiled as a jump to the
exit node.
Any returned value is stored into a special variable before jumping to
the exit node.
*)
and func =
{ func_id: int; (* unique function identifier *)
func_name: string; (* function name *)
func_pos: extent; (* function position in the source *)
func_entry: node; (* entry node *)
func_exit: node; (* exit node *)
func_args: var list; (* list of formal arguments *)
func_ret: var option; (* variable used to store the return value *)
mutable func_calls: arc list; (* list of calls to the function *)
}
(* Graphs *)
(* ****** *)
(*
Each CFG node is denoted by a unique (integer) identifier.
A CFG node corresponds roughly to a position in the program, but complex
statements and expressions can be split among many nodes.
*)
and node =
{ node_id: int; (* unique identifier *)
node_pos: position; (* position in the source *)
mutable node_out: arc list; (* arcs with this node as source *)
mutable node_in: arc list; (* arcs with this node as destination *)
}
and arc =
{ arc_id: int; (* unique identifier *)
arc_src: node; (* source node *)
arc_dst: node; (* destination node *)
arc_inst: inst; (* instruction *)
}
(* Sets, maps and hashtables *)
(* ************************* *)
(* module parameter for Hashtbl, Set and Map functors *)
module Node =
struct
type t = node
let compare v1 v2 = compare v1.node_id v2.node_id
let equal v1 v2 = v1.node_id = v2.node_id
let hash v = v.node_id
end
module Arc =
struct
type t = arc
let compare v1 v2 = compare v1.arc_id v2.arc_id
let equal v1 v2 = v1.arc_id = v2.arc_id
let hash v = v.arc_id
end
module Var =
struct
type t = var
let compare v1 v2 = compare v1.var_id v2.var_id
let equal v1 v2 = v1.var_id = v2.var_id
let hash v = v.var_id
end
module Func =
struct
type t = func
let compare v1 v2 = compare v1.func_id v2.func_id
let equal v1 v2 = v1.func_id = v2.func_id
let hash v = v.func_id
end
module NodeSet = Set.Make(Node)
module NodeMap = Mapext.Make(Node)
module NodeHash = Hashtbl.Make(Node)
module ArcSet = Set.Make(Arc)
module ArcMap = Mapext.Make(Arc)
module ArcHash = Hashtbl.Make(Arc)
module VarSet = Set.Make(Var)
module VarMap = Mapext.Make(Var)
module VarHash = Hashtbl.Make(Var)
module FuncSet = Set.Make(Func)
module FuncMap = Mapext.Make(Func)
module FuncHash = Hashtbl.Make(Func)
(* Program CFG *)
(* *********** *)
type cfg =
{ cfg_vars: var list; (* list of all the variables *)
cfg_funcs: func list; (* list of all the functions *)
cfg_nodes: node list; (* list of all the nodes in the program *)
cfg_arcs: arc list; (* list of all the arcs in the program *)
cfg_init_entry: node; (* first node of code initializing global variables *)
cfg_init_exit: node; (* last node of initialization code *)
}

283
frontend/cfg_printer.ml Normal file
View file

@ -0,0 +1,283 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Pretty-printer for control-flow graphs.
*)
open Lexing
open Abstract_syntax_tree
open Cfg
(* locations *)
(* ********* *)
let pp_pos fmt p =
let file = p.pos_fname in
let line = p.pos_lnum in
Format.fprintf fmt "File \"%s\", line %d" file line
let string_of_position p =
Format.sprintf "%s:%i:%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
let string_of_extent (p,q) =
if p.pos_fname = q.pos_fname then
if p.pos_lnum = q.pos_lnum then
if p.pos_cnum = q.pos_cnum then
Format.sprintf "%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
else
Format.sprintf "%s:%i.%i-%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) (q.pos_cnum - q.pos_bol)
else
Format.sprintf "%s:%i.%i-%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_lnum (q.pos_cnum - q.pos_bol)
else
Format.sprintf "%s:%i.%i-%s:%i.%i" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) q.pos_fname q.pos_lnum (q.pos_cnum - q.pos_bol)
(* operators *)
(* ********* *)
let string_of_int_unary_op = function
| AST_UNARY_PLUS -> "+"
| AST_UNARY_MINUS -> "-"
let string_of_bool_unary_op = function
| AST_NOT -> "!"
let string_of_int_binary_op = function
| AST_MULTIPLY -> "*"
| AST_DIVIDE -> "/"
| AST_MODULO -> "%"
| AST_PLUS -> "+"
| AST_MINUS -> "-"
let string_of_compare_op = function
| AST_EQUAL -> "=="
| AST_NOT_EQUAL -> "!="
| AST_LESS -> "<"
| AST_LESS_EQUAL -> "<="
| AST_GREATER -> ">"
| AST_GREATER_EQUAL -> ">="
let string_of_bool_binary_op = function
| AST_AND -> "&&"
| AST_OR -> "||"
let int_expr_precedence = function
| CFG_int_unary (_, _) -> 99
| CFG_int_binary ((AST_MULTIPLY | AST_DIVIDE | AST_MODULO), _, _) -> 6
| CFG_int_binary ((AST_PLUS | AST_MINUS), _, _) -> 5
| _ -> 100
let bool_expr_precedence = function
| CFG_compare (_,_,_) -> 3
| CFG_bool_binary (AST_AND,_,_) -> 2
| CFG_bool_binary (AST_OR,_,_) -> 1
| _ -> 100
(* utility to print lists *)
let print_list f sep fmt l =
let rec aux = function
| [] -> ()
| [a] -> f fmt a
| a::b -> f fmt a; Format.fprintf fmt "%s" sep; aux b
in
aux l
(* utility to print options *)
let print_option f none fmt l =
match l with
| None -> Format.fprintf fmt "%s" none
| Some v -> f fmt v
(* expressions *)
(* *********** *)
let print_var fmt v =
Format.fprintf fmt "%s(%i)" v.var_name v.var_id
let string_of_type t =
match t with
| AST_TYP_INT -> "int"
let rec print_int_expr fmt e =
match e with
| CFG_int_unary (op,e1) ->
Format.fprintf fmt "%s" (string_of_int_unary_op op);
if int_expr_precedence e1 <= int_expr_precedence e
then Format.fprintf fmt " (%a)" print_int_expr e1
else Format.fprintf fmt " %a" print_int_expr e1
| CFG_int_binary (op,e1,e2) ->
if int_expr_precedence e1 < int_expr_precedence e
then Format.fprintf fmt "(%a) " print_int_expr e1
else Format.fprintf fmt "%a " print_int_expr e1;
Format.fprintf fmt "%s" (string_of_int_binary_op op);
if int_expr_precedence e2 <= int_expr_precedence e
then Format.fprintf fmt " (%a)" print_int_expr e2
else Format.fprintf fmt " %a" print_int_expr e2
| CFG_int_const i -> Format.fprintf fmt "%s" (Z.to_string i)
| CFG_int_rand (i1,i2) ->
Format.fprintf fmt "rand(%s,%s)" (Z.to_string i1) (Z.to_string i2)
| CFG_int_var v -> print_var fmt v
and print_bool_expr fmt e =
match e with
| CFG_bool_unary (op,e1) ->
Format.fprintf fmt "%s" (string_of_bool_unary_op op);
if bool_expr_precedence e1 <= bool_expr_precedence e
then Format.fprintf fmt " (%a)" print_bool_expr e1
else Format.fprintf fmt " %a" print_bool_expr e1
| CFG_bool_binary (op,e1,e2) ->
if bool_expr_precedence e1 < bool_expr_precedence e
then Format.fprintf fmt "(%a) " print_bool_expr e1
else Format.fprintf fmt "%a " print_bool_expr e1;
Format.fprintf fmt "%s" (string_of_bool_binary_op op);
if bool_expr_precedence e2 <= bool_expr_precedence e
then Format.fprintf fmt " (%a)" print_bool_expr e2
else Format.fprintf fmt " %a" print_bool_expr e2
| CFG_compare (op,e1,e2) ->
if int_expr_precedence e1 < bool_expr_precedence e
then Format.fprintf fmt "(%a) " print_int_expr e1
else Format.fprintf fmt "%a " print_int_expr e1;
Format.fprintf fmt "%s" (string_of_compare_op op);
if int_expr_precedence e2 <= bool_expr_precedence e
then Format.fprintf fmt " (%a)" print_int_expr e2
else Format.fprintf fmt " %a" print_int_expr e2
| CFG_bool_const i -> Format.fprintf fmt "%B" i
| CFG_bool_rand -> Format.fprintf fmt "brand"
(* instructions *)
(* ************ *)
let print_inst fmt i =
match i with
| CFG_skip msg -> Format.fprintf fmt "%s" msg
| CFG_assign (v,e) -> Format.fprintf fmt "%a = %a" print_var v print_int_expr e
| CFG_guard b -> Format.fprintf fmt "%a ?" print_bool_expr b
| CFG_assert (b, _) -> Format.fprintf fmt "assert %a" print_bool_expr b
| CFG_call f -> Format.fprintf fmt "call %s" f.func_name
(* programs *)
(* ******** *)
(* raw dump of the graph *)
let print_cfg fmt p =
let pp_var fmt v =
Format.fprintf fmt "%s(%i):%s"
v.var_name v.var_id (string_of_type v.var_type)
in
Format.fprintf fmt "List of variables:\n";
List.iter
(fun v ->
Format.fprintf fmt " %a at %s\n"
pp_var v (string_of_extent v.var_pos)
) p.cfg_vars;
Format.fprintf fmt "\n";
Format.fprintf fmt "List of functions:\n";
List.iter
(fun f ->
Format.fprintf fmt " %i: %s(%a) -> %a at %s, entry: %i, exit: %i, calls:"
f.func_id f.func_name
(print_list pp_var ",") f.func_args
(print_option pp_var "void") f.func_ret
(string_of_extent f.func_pos)
f.func_entry.node_id f.func_exit.node_id;
List.iter
(fun a ->
Format.fprintf fmt " %i->%i" a.arc_src.node_id a.arc_dst.node_id
) f.func_calls;
Format.fprintf fmt "\n";
) p.cfg_funcs;
Format.fprintf fmt "\n";
Format.fprintf fmt "List of nodes:\n";
List.iter
(fun n ->
Format.fprintf fmt " %i: at %s, in: "
n.node_id (string_of_position n.node_pos);
List.iter (fun a -> Format.fprintf fmt "%i " a.arc_src.node_id) n.node_in;
Format.fprintf fmt "out:";
List.iter (fun a -> Format.fprintf fmt "%i " a.arc_dst.node_id) n.node_out;
Format.fprintf fmt "\n";
) p.cfg_nodes;
Format.fprintf fmt "\n";
Format.fprintf fmt "List of arcs:\n";
List.iter
(fun a ->
Format.fprintf fmt " %i -> %i: %a\n"
a.arc_src.node_id a.arc_dst.node_id print_inst a.arc_inst
) p.cfg_arcs;
Format.fprintf fmt "\n"
(* dump to a DOT file, viewable with Graphviz *)
let output_dot name p =
let ch = open_out name in
let fmt = Format.formatter_of_out_channel ch in
Format.fprintf fmt "digraph CFG {\n";
(* nodes and instructions *)
List.iter
(fun a ->
Format.fprintf fmt " %i -> %i [label=\"%a\"];\n"
a.arc_src.node_id a.arc_dst.node_id print_inst a.arc_inst
) p.cfg_arcs;
let isguard arc =
match arc.arc_inst with CFG_guard _ -> true | _ -> false in
List.iter
(fun n -> if n.node_out <> [] && List.for_all isguard n.node_out then
Format.fprintf fmt " %i [shape=diamond];" n.node_id)
p.cfg_nodes;
(* function entry and exit *)
List.iter
(fun f ->
Format.fprintf fmt " entry_%s [shape=box,label=\"%s(%a) -> %a\"];\n"
f.func_name f.func_name
(print_list print_var ",") f.func_args
(print_option print_var "void") f.func_ret;
Format.fprintf fmt " exit_%s [shape=box,label=\"exit %s\"];\n"
f.func_name f.func_name;
Format.fprintf fmt " entry_%s -> %i;\n" f.func_name f.func_entry.node_id;
Format.fprintf fmt " %i -> exit_%s;\n" f.func_exit.node_id f.func_name
) p.cfg_funcs;
(* init code entry and exit *)
Format.fprintf fmt " init_entry [shape=box];\n";
Format.fprintf fmt " init_exit [shape=box];\n";
Format.fprintf fmt " init_entry -> %i;\n" p.cfg_init_entry.node_id;
Format.fprintf fmt " %i -> init_exit;\n" p.cfg_init_exit.node_id;
Format.fprintf fmt "}\n";
flush ch;
close_out ch

17
frontend/dune Normal file
View file

@ -0,0 +1,17 @@
(library
(name frontend)
(wrapped false)
(libraries libs zarith menhirLib apron))
; Special target to generate messages for parser
(rule
(targets parser_messages.ml)
(deps parser.messages parser.mly)
(action (with-stdout-to %{targets} (run menhir --compile-errors %{deps}))))
(menhir
(flags --explain --table)
(modules parser))
(ocamllex
(modules lexer))

28
frontend/errors.ml Normal file
View file

@ -0,0 +1,28 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Error handling utility
*)
open Abstract_syntax_tree
type error_kind =
| AssertFalse
let pp_error_kind fmt = function
| AssertFalse -> Format.fprintf fmt "Assertion failure"
type err = error_kind * extent * bool_expr
let pp_err fmt (ek, ext, be) =
Format.fprintf fmt "%a: %a \"%a\""
Cfg_printer.pp_pos (fst ext)
pp_error_kind ek
Cfg_printer.print_bool_expr be

38
frontend/file_parser.ml Normal file
View file

@ -0,0 +1,38 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Opens and parses a file given as argument.
*)
open Abstract_syntax_tree
open Cfg_printer
open Lexing
(* parsing, with nice error messages *)
let parse_file (filename: string) : prog =
let file = open_in filename in
let lexbuf = from_channel file in
lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = filename; pos_lnum = 1};
let module MI = Parser.MenhirInterpreter in
let checkpoint = Parser.Incremental.file lexbuf.lex_curr_p
and supplier = MI.lexer_lexbuf_to_supplier Lexer.token lexbuf
and succeed x = x
and fail checkpoint =
let position = string_of_position lexbuf.lex_start_p in
let error_msg =
match checkpoint with
| MI.HandlingError env -> env |> MI.current_state_number |> Parser_messages.message
| _ -> assert false (* This should not happen. *)
in
Printf.printf "%s: %s" position error_msg;
exit 1
in
MI.loop_handle succeed fail supplier checkpoint

11
frontend/file_parser.mli Normal file
View file

@ -0,0 +1,11 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2014
Marc Chevalier 2018
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
val parse_file: string -> Abstract_syntax_tree.prog
(* Opens and parses a file given as argument. *)

122
frontend/lexer.mll Normal file
View file

@ -0,0 +1,122 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Lexer for a very simple C-like "curly bracket" language.
This version has local variables, function calls, and returns.
*)
{
open Lexing
open Parser
(* keyword table *)
let kwd_table = Hashtbl.create 10
let _ =
List.iter (fun (a,b) -> Hashtbl.add kwd_table a b)
[
(* types *)
"void", TOK_VOID;
"int", TOK_INT;
(* constants *)
"true", TOK_TRUE;
"false", TOK_FALSE;
(* expression operators *)
"rand", TOK_RAND;
"brand", TOK_BRAND;
(* control flow *)
"for", TOK_FOR;
"while", TOK_WHILE;
"return", TOK_RETURN;
"break", TOK_BREAK;
"if", TOK_IF;
"else", TOK_ELSE;
"goto", TOK_GOTO;
(* special statements *)
"assert", TOK_ASSERT;
]
}
(* special character classes *)
let space = [' ' '\t' '\r']+
let newline = "\n" | "\r" | "\r\n"
(* utilities *)
let digit = ['0'-'9']
let digit_ = ['0'-'9' '_']
(* integers *)
let int_dec = digit digit_*
let int_bin = ("0b" | "0B") ['0'-'1'] ['0'-'1' '_']*
let int_oct = ("0o" | "0O") ['0'-'7'] ['0'-'7' '_']*
let int_hex = ("0x" | "0X") ['0'-'9' 'a'-'f' 'A'-'F'] ['0'-'9' 'a'-'f' 'A'-'F' '_']*
let const_int = int_bin | int_oct | int_dec | int_hex
(* tokens *)
rule token = parse
(* identifier (TOK_id) or reserved keyword *)
| ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* as id
{ try Hashtbl.find kwd_table id with Not_found -> TOK_id id }
(* symbols *)
| "(" { TOK_LPAREN }
| ")" { TOK_RPAREN }
| "{" { TOK_LCURLY }
| "}" { TOK_RCURLY }
| "*" { TOK_STAR }
| "+" { TOK_PLUS }
| "-" { TOK_MINUS }
| "!" { TOK_EXCLAIM }
| "/" { TOK_DIVIDE }
| "%" { TOK_PERCENT }
| "<" { TOK_LESS }
| ">" { TOK_GREATER }
| "<=" { TOK_LESS_EQUAL }
| ">=" { TOK_GREATER_EQUAL }
| "==" { TOK_EQUAL_EQUAL }
| "!=" { TOK_NOT_EQUAL }
| "&&" { TOK_AND_AND }
| "||" { TOK_BAR_BAR }
| ";" { TOK_SEMICOLON }
| ":" { TOK_COLON }
| "," { TOK_COMMA }
| "=" { TOK_EQUAL }
| "++" { TOK_PLUS_PLUS }
| "--" { TOK_MINUS_MINUS }
| "+=" { TOK_PLUS_EQUAL }
| "-=" { TOK_MINUS_EQUAL }
| "*=" { TOK_STAR_EQUAL }
| "/=" { TOK_DIVIDE_EQUAL }
| "%=" { TOK_PERCENT_EQUAL }
(* literals *)
| const_int as c { TOK_int c }
(* spaces, comments *)
| "/*" { comment lexbuf; token lexbuf }
| "//" [^ '\n' '\r']* { token lexbuf }
| newline { new_line lexbuf; token lexbuf }
| space { token lexbuf }
(* end of files *)
| eof { TOK_EOF }
(* nested comments (handled recursively) *)
and comment = parse
| "*/" { () }
| [^ '\n' '\r'] { comment lexbuf }
| newline { new_line lexbuf; comment lexbuf }

52
frontend/options.ml Normal file
View file

@ -0,0 +1,52 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Command line parsing utility
*)
module IMap = Map.Make(String)
open Arg
(* Flags *)
let verbose = ref false
(* string arguments *)
let file = ref ""
let cfg_out = ref "cfg.dot"
let domain = ref ""
let args = [
"-v", Set verbose,
" Execute the analyzer in verbose/debug mode";
"--dot-out", Set_string cfg_out,
" Print the cfg in this file (default is cfg.dot)";
"--domain", Set_string domain,
" Select the abstract domain (constants/interval)";
] |> align
let usage = "usage: ./analyzer.exe [options] filename.c"
let init () =
let _ = parse args ( (:=) file) usage in
let _ = if Filename.extension !file <> ".c" then begin
Format.eprintf "file should have extension .c file: \"%s\"\n" !file;
Arg.usage args usage;
exit 1
end
in
let _ = if Filename.extension !cfg_out <> ".dot" then begin
Format.eprintf "CFG output file should have extension .dot (%s)\n" !cfg_out;
Arg.usage args usage;
exit 1
end
in ()

1523
frontend/parser.messages Normal file
View file

File diff suppressed because it is too large Load diff

285
frontend/parser.mly Normal file
View file

@ -0,0 +1,285 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Parser for a very simple C-like "curly bracket" language.
*)
%{
open Abstract_syntax_tree
%}
/* tokens */
/**********/
%token TOK_VOID
%token TOK_INT
%token TOK_TRUE
%token TOK_FALSE
%token TOK_RAND
%token TOK_BRAND
%token TOK_FOR
%token TOK_WHILE
%token TOK_RETURN
%token TOK_BREAK
%token TOK_IF
%token TOK_ELSE
%token TOK_GOTO
%token TOK_ASSERT
%token TOK_LPAREN
%token TOK_RPAREN
%token TOK_LCURLY
%token TOK_RCURLY
%token TOK_STAR
%token TOK_PLUS
%token TOK_MINUS
%token TOK_EXCLAIM
%token TOK_DIVIDE
%token TOK_PERCENT
%token TOK_LESS
%token TOK_GREATER
%token TOK_LESS_EQUAL
%token TOK_GREATER_EQUAL
%token TOK_EQUAL_EQUAL
%token TOK_NOT_EQUAL
%token TOK_AND_AND
%token TOK_BAR_BAR
%token TOK_SEMICOLON
%token TOK_COLON
%token TOK_COMMA
%token TOK_EQUAL
%token TOK_PLUS_PLUS
%token TOK_MINUS_MINUS
%token TOK_PLUS_EQUAL
%token TOK_MINUS_EQUAL
%token TOK_STAR_EQUAL
%token TOK_DIVIDE_EQUAL
%token TOK_PERCENT_EQUAL
%token <string> TOK_id
%token <string> TOK_int
%token TOK_EOF
/* priorities of binary operators (lowest to highest) */
%left TOK_BAR_BAR
%left TOK_AND_AND
%left TOK_EXCLAIM
%left TOK_PLUS TOK_MINUS
%left TOK_STAR TOK_DIVIDE TOK_PERCENT
/* entry-points */
/****************/
%start<Abstract_syntax_tree.toplevel list Abstract_syntax_tree.ext> file
%%
/* toplevel */
/************/
file: t=ext(list(toplevel)) TOK_EOF { t }
toplevel:
| d=ext(var_decl) { AST_global_decl d }
| d=ext(fun_decl) { AST_fun_decl d }
/* expressions */
/***************/
bool_expr:
| TOK_LPAREN e=bool_expr TOK_RPAREN
{ e }
| TOK_TRUE
{ AST_bool_const true }
| TOK_FALSE
{ AST_bool_const false }
| o=bool_unary_op e=ext(bool_expr)
{ AST_bool_unary (o,e) }
| e1=ext(bool_expr) o=bool_binary_op e2=ext(bool_expr)
{ AST_bool_binary (o,e1,e2) }
| e1=ext(int_expr) o=compare_op e2=ext(int_expr)
{ AST_compare (o,e1,e2) }
| TOK_BRAND
{ AST_bool_rand }
int_expr:
| TOK_LPAREN e=int_expr TOK_RPAREN
{ e }
| e=ext(TOK_int)
{ AST_int_const e }
| e=ext(TOK_id)
{ AST_int_identifier e }
| o=int_unary_op e=ext(int_expr)
{ AST_int_unary (o,e) }
| e1=ext(int_expr) o=int_binary_op e2=ext(int_expr)
{ AST_int_binary (o,e1,e2) }
| TOK_RAND TOK_LPAREN e1=ext(sign_int_literal)
TOK_COMMA e2=ext(sign_int_literal) TOK_RPAREN
{ AST_int_rand (e1, e2) }
| e=ext(TOK_id) TOK_LPAREN l=int_expr_list TOK_RPAREN
{ AST_expr_call (e, l) }
int_expr_list:
l=separated_list(TOK_COMMA,ext(int_expr)) { l }
/* integer with optional sign */
sign_int_literal:
| i=TOK_int { i }
| TOK_PLUS i=TOK_int { i }
| TOK_MINUS i=TOK_int { "-"^i }
%inline int_unary_op:
| TOK_PLUS { AST_UNARY_PLUS }
| TOK_MINUS { AST_UNARY_MINUS }
%inline bool_unary_op:
| TOK_EXCLAIM { AST_NOT }
%inline int_binary_op:
| TOK_STAR { AST_MULTIPLY }
| TOK_DIVIDE { AST_DIVIDE }
| TOK_PERCENT { AST_MODULO }
| TOK_PLUS { AST_PLUS }
| TOK_MINUS { AST_MINUS }
%inline assign_op:
| TOK_STAR_EQUAL { AST_MULTIPLY }
| TOK_DIVIDE_EQUAL { AST_DIVIDE }
| TOK_PERCENT_EQUAL { AST_MODULO }
| TOK_PLUS_EQUAL { AST_PLUS }
| TOK_MINUS_EQUAL { AST_MINUS }
%inline compare_op:
| TOK_LESS { AST_LESS }
| TOK_GREATER { AST_GREATER }
| TOK_LESS_EQUAL { AST_LESS_EQUAL }
| TOK_GREATER_EQUAL { AST_GREATER_EQUAL }
| TOK_EQUAL_EQUAL { AST_EQUAL }
| TOK_NOT_EQUAL { AST_NOT_EQUAL }
%inline bool_binary_op:
| TOK_AND_AND { AST_AND }
| TOK_BAR_BAR { AST_OR }
/* declarations */
/****************/
var_decl:
| s=ext(typ) i=separated_list(TOK_COMMA,init_declarator) TOK_SEMICOLON
{ s, i }
init_declarator:
| v=ext(TOK_id) { v, None }
| v=ext(TOK_id) TOK_EQUAL i=ext(int_expr) { v, Some i }
fun_decl:
| t=ext(typ_or_void) i=ext(TOK_id)
TOK_LPAREN p=separated_list(TOK_COMMA,param_decl) TOK_RPAREN
TOK_LCURLY l=list(ext(stat)) TOK_RCURLY
{ { Abstract_syntax_tree.fun_name = i;
Abstract_syntax_tree.fun_typ = t;
Abstract_syntax_tree.fun_args = p;
Abstract_syntax_tree.fun_body = l;
Abstract_syntax_tree.fun_ext = ($startpos, $endpos); }
}
param_decl:
| s=ext(typ) v=ext(TOK_id) { s, v }
typ:
| TOK_INT { AST_TYP_INT }
%inline typ_or_void:
| t=typ { Some t }
| TOK_VOID { None }
/* statements */
/**************/
assign:
| e=ext(TOK_id) TOK_EQUAL f=ext(int_expr)
{ AST_assign (e, f) }
| e=ext(TOK_id) o=assign_op f=ext(int_expr)
{ AST_assign_op (e, o, f) }
| e=ext(TOK_id) TOK_PLUS_PLUS
{ AST_increment (e,1) }
| e=ext(TOK_id) TOK_MINUS_MINUS
{ AST_increment (e,-1); }
assign_list:
l=separated_list(TOK_COMMA,ext(assign)) { l }
common_stat:
| a=assign TOK_SEMICOLON { a }
| d=ext(var_decl) { AST_local_decl d }
| TOK_LCURLY l=list(ext(stat)) TOK_RCURLY { AST_block l }
| e=ext(TOK_id) TOK_COLON { AST_label e }
| TOK_ASSERT TOK_LPAREN e=ext(bool_expr) TOK_RPAREN TOK_SEMICOLON { AST_assert e }
| e=ext(TOK_BREAK) TOK_SEMICOLON { AST_break e }
| e=ext(TOK_id) TOK_LPAREN l=int_expr_list TOK_RPAREN TOK_SEMICOLON { AST_stat_call (e, l) }
| TOK_RETURN e=option(ext(int_expr)) TOK_SEMICOLON { AST_return e }
| TOK_SEMICOLON { AST_SKIP }
| TOK_GOTO e=ext(TOK_id) TOK_SEMICOLON { AST_goto e }
stat_with_else:
| s=common_stat { s }
| TOK_IF TOK_LPAREN e=ext(bool_expr) TOK_RPAREN s=ext(stat_with_else) TOK_ELSE t=ext(stat_with_else) { AST_if (e, s, Some t) }
| TOK_WHILE TOK_LPAREN e=ext(bool_expr) TOK_RPAREN s=ext(stat_with_else) { AST_while (e, s) }
| TOK_FOR TOK_LPAREN a=assign_list TOK_SEMICOLON b=option(ext(bool_expr)) TOK_SEMICOLON c=assign_list TOK_RPAREN s=ext(stat_with_else) { AST_for (a,b,c,s) }
stat:
| s=common_stat { s }
| TOK_IF TOK_LPAREN e=ext(bool_expr) TOK_RPAREN s=ext(stat) { AST_if (e, s, None) }
| TOK_IF TOK_LPAREN e=ext(bool_expr) TOK_RPAREN s=ext(stat_with_else) TOK_ELSE t=ext(stat) { AST_if (e, s, Some t) }
| TOK_WHILE TOK_LPAREN e=ext(bool_expr) TOK_RPAREN s=ext(stat) { AST_while (e, s) }
| TOK_FOR TOK_LPAREN a=assign_list TOK_SEMICOLON b=option(ext(bool_expr)) TOK_SEMICOLON c=assign_list TOK_RPAREN s=ext(stat) { AST_for (a,b,c,s) }
/* utilities */
/*************/
/* adds extent information to rule */
%inline ext(X):
| x=X { x, ($startpos, $endpos) }
%%

640
frontend/tree_to_cfg.ml Normal file
View file

@ -0,0 +1,640 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
Converts an abstract syntax tree to a control-flow-graph.
CFG arcs use a simpler language.
The conversion takes care of splitting complex statements and
expressions, and introducing temporaries if necessary.
*)
open Abstract_syntax_tree
open! Cfg
open Cfg_printer
(* map variable and function names to structures *)
module StringMap = Map.Make(String)
(* constructors *)
(* ************ *)
let node_counter = ref 0
let nodes = ref []
(* create a new node, with a fresh identifier and accumulate into nodes *)
let create_node (pos:position) =
incr node_counter;
let node =
{ node_id = !node_counter;
node_pos = pos;
node_in = [];
node_out = [];
}
in
nodes := node::(!nodes);
node
let arcs = ref []
let arc_counter = ref 0
(* create a new arc and accumulate it into arcs *)
let add_arc (src:node) (dst:node) (inst:inst) =
incr arc_counter;
let arc =
{ arc_id = !arc_counter;
arc_src = src;
arc_dst = dst;
arc_inst = inst;
}
in
src.node_out <- arc::src.node_out;
dst.node_in <- arc::dst.node_in;
(* remember call sites for call instructions *)
(match inst with
| CFG_call f -> f.func_calls <- arc::f.func_calls
| _ -> ()
);
arcs := arc::(!arcs)
let var_counter = ref 0
(* create a variable structure, assigning it a fresh identifier *)
let create_var (name:string) (pos:extent) (typ:typ) =
incr var_counter;
{ var_id = !var_counter;
var_name = name;
var_pos = pos;
var_type = typ;
}
let fun_counter = ref 0
(* create a function structure, assigning it a fresh identifier *)
let create_fun (name:string) (entry:node) (exit:node) (pos:extent) (args:var list) (ret:var option) =
incr fun_counter;
{ func_id = !fun_counter;
func_name = name;
func_pos = pos;
func_entry = entry;
func_exit = exit;
func_args = args;
func_ret = ret;
func_calls = [];
}
(* add a sequence of instructions to the CFG between two nodes *)
let rec add_inst (entry:node) (exit:node) (l:inst ext list) =
match l with
| [] ->
(* entry --[skip]--> exit *)
add_arc entry exit (CFG_skip "skip")
| [(a,_)] ->
(* entry --[a]--> exit *)
add_arc entry exit a
| (first,x)::rest ->
(* add intermediate (next) node *)
let next = create_node (snd x) in
(* entry --[first]--> next *)
add_arc entry next first;
(* next --[rest]--> exit *)
add_inst next exit rest
(* Add a sequence of instructions to the CFG.
The entry of the first instruction is the given node; other
nodes are created.
The exit node of the last instruction is returned.
*)
let rec append_inst (entry:node) (l:inst ext list) : node =
match l with
| [] -> entry
| (first,x)::rest ->
(* add intermediate (next) node *)
let next = create_node (snd x) in
(* entry --[first]--> next *)
add_arc entry next first;
(* next --[rest]--> *)
append_inst next rest
(* Also add a sequence of instruction to the CFG.
The exist of the first instruction is given node.
The entry of the last instruction is returned.
*)
let rec prepend_inst (exit:node) (l:inst ext list) : node =
match l with
| [] -> exit
| (first,x)::rest ->
(* add intermediate (prev) node *)
let prev = create_node (fst x) in
(* prev --[first]--> exit *)
add_arc prev exit first;
(* --[rest]--> prev *)
prepend_inst prev rest
(* translation *)
(* *********** *)
(*
We need to remember a lot of information during translation, such as the
set of variables in the scope, where to jump to after a break or a return,
in which variable to store a returned value, etc.
For gotos, arcs are generated at the end of the translation of each
procedure, to handle more easily backward gotos; hence, we must also
remember label and goto instructions for this later pass.
Everything needed is wrapped in an env.
*)
type env =
{ env_vars: var StringMap.t; (* visible variables in scope, by name *)
env_funcs: func StringMap.t; (* visible functions in scope, by name *)
env_break: node option; (* destination of a break *)
env_exit: node option; (* destination of a return *)
env_return: var option; (* variable storing the returned value *)
env_allvars: VarSet.t; (* set of all variables *)
env_labels: node StringMap.t; (* labels *)
env_gotos: (node * string ext) list; (* gotos *)
}
let add_to_vars (env:env) (v:var) : env =
{ env with
env_vars = StringMap.add v.var_name v env.env_vars;
env_allvars = VarSet.add v env.env_allvars;
}
(*
Expression translation.
Also returns a list of instructions that must be executed before the
expression can be evaluated, such as function calls that have been
extracted from the expression.
*)
let rec int_expr (env:env) (expr:Abstract_syntax_tree.int_expr)
: env * inst ext list * int_expr =
match expr with
| AST_int_unary (o,(e1,_)) ->
let env1, before1, f1 = int_expr env e1 in
env1, before1, CFG_int_unary (o,f1)
| AST_int_binary (o,(e1,_),(e2,_)) ->
let env1, before1, f1 = int_expr env e1 in
let env2, before2, f2 = int_expr env1 e2 in
env2, before1@before2, CFG_int_binary (o,f1,f2)
| AST_int_identifier (id,x) ->
let var =
try StringMap.find id env.env_vars
with Not_found -> failwith (Printf.sprintf "unknown variable %s at %s" id (string_of_extent x))
in
env, [], CFG_int_var var
| AST_int_const (i,x) ->
let v =
try Z.of_string i
with _ -> failwith (Printf.sprintf "invalid integer constant %s at %s" i (string_of_extent x))
in
env, [], CFG_int_const v
| AST_int_rand ((i1,x1),(i2,x2)) ->
let v1 =
try Z.of_string i1
with _ -> failwith (Printf.sprintf "invalid integer constant %s at %s" i1 (string_of_extent x1))
and v2 =
try Z.of_string i2
with _ -> failwith (Printf.sprintf "invalid integer constant %s at %s" i2 (string_of_extent x2))
in
env, [], CFG_int_rand (v1,v2)
| AST_expr_call ((id,x),exprs) ->
let env1, inst, f = call env (id,x) exprs in
(match f.func_ret with
| None -> failwith (Printf.sprintf "function %s has no return value at %s" id (string_of_extent x))
| Some var ->
(* we must create a temporary to hold the returned value
(consider the case where the function is called twice in the expression)
*)
let tmp = create_var ("__ret_"^id) x var.var_type in
let ass = CFG_assign (tmp, CFG_int_var var) in
add_to_vars env1 var, inst@[ass,x], CFG_int_var tmp
)
and bool_expr (env:env) (expr:Abstract_syntax_tree.bool_expr)
: env * inst ext list * bool_expr =
match expr with
| AST_bool_unary (o,(e1,_)) ->
let env1, before1, f1 = bool_expr env e1 in
env1, before1, CFG_bool_unary (o,f1)
| AST_bool_binary (o,(e1,_),(e2,_)) ->
let env1, before1, f1 = bool_expr env e1 in
let env2, before2, f2 = bool_expr env1 e2 in
env2, before1@before2, CFG_bool_binary (o,f1,f2)
| AST_compare (o,(e1,_),(e2,_)) ->
let env1, before1, f1 = int_expr env e1 in
let env2, before2, f2 = int_expr env1 e2 in
env2, before1@before2, CFG_compare (o,f1,f2)
| AST_bool_const f ->
env, [], CFG_bool_const f
| AST_bool_rand ->
env, [], CFG_bool_rand
(* Translate a call. *)
and call (env:env) ((id,x):id ext) (exprs:Abstract_syntax_tree.int_expr ext list)
: env * inst ext list * func =
let f =
try StringMap.find id env.env_funcs
with Not_found -> failwith (Printf.sprintf "unknown function %s at %s" id (string_of_extent x))
in
(* match formal and actual arguments *)
let rec doargs env inst args = match args with
| [],[] -> env, inst
| var::rest1, (expr,x1)::rest2 ->
(* translate argument binding to assignment *)
let env1, before, e1 = int_expr env expr in
doargs env1 (before @ [CFG_assign (var,e1), x1] @ inst) (rest1, rest2)
| _ ->
failwith (Printf.sprintf "wrong number of arguments for function %s at %s" id (string_of_extent x))
in
let env1, inst = doargs env [CFG_call f, x] (f.func_args,exprs) in
env1, inst, f
(* Variable declarations.
Create the variable structure, remember it in the environment,
and translate initialization into assignments.
*)
let decls (env:env) (((t,_),l):var_decl) : env * inst ext list =
List.fold_left
(fun (env,inst) ((id,x),init) ->
let var = create_var id x t in
let env1 = add_to_vars env var in
let expr, ext =
match init with
| None -> AST_int_const ("0", x), x
| Some (expr,x1) -> expr, x1 in
let env2, before, e = int_expr env1 expr in
env2, before @ [CFG_assign (var,e), ext] @ inst
)
(env,[]) l
(*
Translate a statement.
Translation creates a subgraph. The first instruction of the subgraph
is connected to the given entry node, and the last is connected to the
given exit node.
*)
let rec stat (env:env) (entry:node) (exit:node) (s:stat) : env =
match s with
| AST_block l ->
let env1 = stat_list env entry exit l in
(* restore the variable scoping from the begining of the block *)
{ env1 with env_vars = env.env_vars; }
| AST_SKIP ->
add_arc entry exit (CFG_skip "skip");
env
| AST_assign ((id,x),(expr,_)) ->
(* translate expression *)
let env1, before, e1 = int_expr env expr in
(* entry --[before]--> entry1 --[assign] --> exit *)
let entry1 = append_inst entry before in
let var =
try StringMap.find id env1.env_vars
with Not_found -> failwith (Printf.sprintf "unknown variable %s at %s" id (string_of_extent x))
in
add_arc entry1 exit (CFG_assign (var, e1));
env1
| AST_increment ((id,x),v) ->
(* x++ is translated as x = x + 1 *)
let var =
try StringMap.find id env.env_vars
with Not_found -> failwith (Printf.sprintf "unknown variable %s at %s" id (string_of_extent x))
in
add_arc entry exit
(CFG_assign (var, (CFG_int_binary (AST_PLUS, CFG_int_var var, CFG_int_const (Z.of_int v)))));
env
| AST_assign_op ((id,x),op,(expr,_)) ->
(* x += expr is translated as x = x + expr *)
let env1, before, e = int_expr env expr in
let entry1 = append_inst entry before in
let var =
try StringMap.find id env1.env_vars
with Not_found -> failwith (Printf.sprintf "unknown variable %s at %s" id (string_of_extent x))
in
add_arc entry1 exit
(CFG_assign (var, (CFG_int_binary (op, CFG_int_var var, e))));
env1
| AST_assert (expr, ext) ->
(* entry --[before]--> entry1 --[assert] --> exit *)
let env1, before, e = bool_expr env expr in
let entry1 = append_inst entry before in
add_arc entry1 exit (CFG_assert (e, ext));
env1
| AST_break ((),x) ->
(* break: jump outside innermost loop *)
(* entry --[skip]--> env_break *)
(match env.env_break with
| Some node -> add_arc entry node (CFG_skip "skip: break")
| None -> failwith (Printf.sprintf "break outside loop at %s" (string_of_extent x))
);
env
| AST_return None ->
(* return: jump to the function exit *)
(* entry --[skip]--> env_exit *)
(match env.env_exit with
| Some exit -> add_arc entry exit (CFG_skip "skip: return")
| None -> failwith "no exit node for function"
);
env
| AST_return (Some (expr,x)) ->
(* return expr is translated as return = expr
the assignment is connected directly to the function exit
*)
(* entry --[before]--> entry1 --[assign] --> env_exit *)
let env1, before, e = int_expr env expr in
let entry1 = append_inst entry before in
let var =
match env1.env_return with
| Some v -> v
| None -> failwith (Printf.sprintf "function cannot return a value at %s" (string_of_extent x))
in
(match env1.env_exit with
| Some exit -> add_arc entry1 exit (CFG_assign (var, e))
| None -> failwith "no exit node for function"
);
env1
| AST_if ((expr,_),(s1,x1),(Some (s2,x2))) ->
(*
/--[expr]---> node_t --[s1]--\
entry --[before]--> entry1 --| |---> exit
\--[!expr]--> node_f --[s2]--/
*)
let env1, before, e = bool_expr env expr in
(* entry --[before]--> entry1 *)
let entry1 = append_inst entry before in
let node_t, node_f = create_node (fst x1), create_node (fst x2) in
(* entry1 --[expr]--> node_t_t *)
add_arc entry1 node_t (CFG_guard e);
(* entry1 --[!expr] --> node_f *)
add_arc entry1 node_f (CFG_guard (CFG_bool_unary (AST_NOT, e)));
(* node_t --[s1]--> exit *)
let env2 = stat env1 node_t exit s1 in
(* node_f --[s2] --> exit *)
stat env2 node_f exit s2
| AST_if ((expr,_),(s1,x1),None) ->
(*
/--[expr]---> node_t --[s1]--\
entry --[before]--> entry1 --| |---> exit
\--[!expr]--> ---------------/
*)
let env1, before, e = bool_expr env expr in
(* entry --[before]--> entry1 *)
let entry1 = append_inst entry before in
let node_t = create_node (fst x1) in
(* entry1 --[expr]--> node_t *)
add_arc entry1 node_t (CFG_guard e);
(* entry1 --[!expr]--> exit *)
add_arc entry1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e)));
(* node_t --[s1]--> exit *)
stat env1 node_t exit s1
| AST_while ((expr,_),(s1,x1)) ->
(*
similar to "if expr then s1", except that we have
node_t --[s1]--> entry
instead of
node_t --[s1]--> exit
*)
let env1, before, e = bool_expr env expr in
(* entry --[before]--> entry1 *)
let entry1 = append_inst entry before in
let node_t = create_node (fst x1) in
(* entry1 --[expr]--> node_t *)
add_arc entry1 node_t (CFG_guard e);
(* entry1 --[!expr]--> node_f *)
add_arc entry1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e)));
(* node_t --[s1]--> entry *)
let env2 = stat { env1 with env_break = Some exit; } node_t entry s1 in
{ env2 with env_break = env1.env_break; }
| AST_for (init,expr,incr,(s1,x1)) ->
(* init *)
(* entry --[init]--> head *)
let env1, head =
if init = []
then env, entry
else (
let head = create_node (fst x1) in
stat_list env entry head init, head
)
in
(* conditional *)
(*
head --[before]--> head1 ---[expr]---> node_t
\--[!expr]--> exit
*)
let env2, before, e =
match expr with
| None -> env1, [], CFG_bool_const true
| Some (expr,_) -> bool_expr env1 expr
in
let head1 = append_inst head before in
let node_t = create_node (fst x1) in
add_arc head1 node_t (CFG_guard e);
add_arc head1 exit (CFG_guard (CFG_bool_unary (AST_NOT, e)));
(* increment *)
(* tail --[incr]--> head *)
let env3, tail =
if incr = []
then env2, head
else (
let tail = create_node (snd x1) in
stat_list env2 tail head incr, tail
)
in
(* body *)
(* node_t --[s1]--> tail *)
let env4 = stat { env3 with env_break = Some exit; } node_t tail s1 in
{ env4 with env_break = env3.env_break; }
| AST_local_decl (d,_) ->
let env1, inst = decls env d in
add_inst entry exit inst;
env1
| AST_stat_call (idx,exprs) ->
let env1, inst, _ = call env idx exprs in
add_inst entry exit inst;
env1
| AST_label (id,x) ->
(* remember the node of the label *)
if StringMap.mem id env.env_labels then
failwith (Printf.sprintf "duplicate label %s at %s" id (string_of_extent x));
add_arc entry exit (CFG_skip ("skip: label "^id));
{ env with env_labels = StringMap.add id entry env.env_labels; }
| AST_goto (id,x) ->
(* remember the goto; we will generate at the end of the function,
when all the labels are known
*)
{ env with env_gotos = (entry,(id,x))::env.env_gotos; }
(* Translate a sequence of statements. *)
and stat_list (env:env) (entry:node) (exit:node) (l:stat ext list) : env =
match l with
| [] ->
(* entry --[skip]--> exit *)
add_arc entry exit (CFG_skip "skip");
env
| [(s,_)] ->
(* entry --[s]--> exit *)
stat env entry exit s
| (first,x)::rest ->
(* add an intermediate (next) node *)
let next = create_node (snd x) in
(* entry --[first]--> next *)
let env1 = stat env entry next first in
(* next --[rest]--> exit *)
stat_list env1 next exit rest
(* Translate a function *)
let func (env:env) (f:fun_decl) : env =
(* create entry and exit nodes *)
let entry = create_node (fst f.fun_ext) in
let exit = create_node (snd f.fun_ext) in
(* create variable structures for formal arguments and return *)
let args = List.map (fun ((t,_),(id,x)) -> create_var id x t) f.fun_args in
let ret = match f.fun_typ with
| None, _ -> None
| Some t, _ -> Some (create_var ("__return_"^(fst f.fun_name)) f.fun_ext t)
in
(* create function structure *)
let func = create_fun (fst f.fun_name) entry exit f.fun_ext args ret in
(* populate env with formal arguments and return *)
let env1 =
{ env with
env_exit = Some exit;
env_return = ret;
env_funcs = StringMap.add func.func_name func env.env_funcs;
}
in
let env2 = List.fold_left add_to_vars env1 args in
let env3 = match ret with Some v -> add_to_vars env2 v | None -> env2 in
(* translate body *)
let env4 = stat_list env3 entry exit f.fun_body in
(* generate gotos *)
List.iter
(fun (src,(id,x)) ->
let dst =
try StringMap.find id env4.env_labels
with Not_found -> failwith (Printf.sprintf "unknown label %s at %s" id (string_of_extent x))
in
add_arc src dst (CFG_skip ("skip: goto "^id))
) env4.env_gotos;
(* returned environment *)
{ env with
env_funcs = env4.env_funcs;
env_allvars = env4.env_allvars;
}
(* Translate a whole program *)
let prog ((t, x): prog) : cfg =
(* initial environment *)
arcs := [];
nodes := [];
let env_init =
{ env_vars = StringMap.empty;
env_funcs = StringMap.empty;
env_break = None;
env_exit = None;
env_return = None;
env_allvars = VarSet.empty;
env_labels = StringMap.empty;
env_gotos = [];
}
in
(* translate each toplevel instruction *)
let env, revinit =
List.fold_left
(fun (env,revinit) t -> match t with
| AST_fun_decl (f,_) ->
func env f, revinit
| AST_global_decl (d,_) ->
let env1, inst1 = decls env d in
env1, List.rev_append inst1 revinit
)
(env_init,[]) t
in
let init = List.rev revinit in
(* init code *)
let entry = create_node (fst x) in
let exit = create_node (snd x) in
add_inst entry exit init;
(* extract program info *)
let vars = List.rev (VarSet.fold (fun a acc -> a::acc) env.env_allvars []) in
let funcs = List.rev (StringMap.fold (fun _ f acc -> f::acc) env.env_funcs []) in
{ cfg_vars = vars;
cfg_funcs = funcs;
cfg_init_entry = entry;
cfg_init_exit = exit;
cfg_nodes = List.rev !nodes;
cfg_arcs = List.rev !arcs;
}

5
iterator/dune Normal file
View file

@ -0,0 +1,5 @@
(library
(name iterator)
(wrapped false)
(libraries libs zarith menhirLib apron frontend domains))

106
iterator/iterator.ml Normal file
View file

@ -0,0 +1,106 @@
(*
Cours "Sémantique et Application à la Vérification de programmes"
Antoine Miné 2015
Marc Chevalier 2018
Josselin Giet 2021
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
open Cfg
open Domain
let pp_asserts out a =
ArcSet.iter (fun arc -> match arc.arc_inst with
| CFG_assert (b, ext) -> Format.fprintf out "%a@ " Errors.pp_err (AssertFalse, ext, b)
| _ -> failwith "Failed on non-assert") a
module Iterator (D : DOMAIN) = struct
let do_inst state arc asserts =
(* Returns a D.t describing the state we end up in after following the arc. May be bottom*)
match arc.arc_inst with
| CFG_skip _-> state, asserts
| CFG_assign (v, iexpr) -> (D.assign state v iexpr), asserts
| CFG_guard bexpr -> (D.guard state bexpr), asserts
| CFG_assert (bexpr, _) -> (let s = D.guard state (CFG_bool_unary (AST_NOT, bexpr)) in
if D.is_bottom s then (
Format.printf "State %a is disjoint with %a@ " D.print state Cfg_printer.print_bool_expr (rm_negations (CFG_bool_unary (AST_NOT, bexpr)));
state, asserts) else (
Format.printf "Failure of guard on %a@ " D.print s;
(D.guard state bexpr), ArcSet.add arc asserts))
| CFG_call _ -> failwith "Function calls not yet supported"
let node_abst n s = try( NodeMap.find n s )with Not_found -> D.bottom
let pp_nodes out (s,nodelist) =
List.iter (fun node -> (Format.fprintf out "<%i>: %a@ " node.node_id D.print (node_abst node s))) nodelist
let iterate cfg =
let global_state = ref NodeMap.empty in (* non-present nodes are Bot and assumed unreachable *)
let failed_asserts = ref ArcSet.empty in
let dirty_nodes = ref NodeSet.empty in
let update_node n s =
global_state := NodeMap.add n (D.join s (node_abst n !global_state)) !global_state in
let rec do_init_code n =
if (Node.equal n cfg.cfg_init_exit) then () else (
let nextarc = List.find (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in
let nextnode = nextarc.arc_dst in
let s, a = do_inst (node_abst n !global_state) nextarc !failed_asserts in
(Format.printf "@[<h 0>Got node %i state %a@]@ " nextnode.node_id D.print s;
update_node nextnode s; failed_asserts := a; do_init_code nextnode)) in
let rec do_iter n = begin
dirty_nodes := NodeSet.remove n !dirty_nodes;
let curr_abst = node_abst n !global_state in
let l = List.filter (fun x -> Node.equal x.arc_src n) cfg.cfg_arcs in begin
List.iter (fun arc -> let s, a = do_inst curr_abst arc !failed_asserts in
failed_asserts := a;
if D.subset s (node_abst arc.arc_dst !global_state) then ()
else (Format.printf "@[<h 0>Got node %i state %a@]@ " arc.arc_dst.node_id D.print s;
update_node arc.arc_dst s; dirty_nodes := NodeSet.add arc.arc_dst !dirty_nodes)) l;
if NodeSet.is_empty !dirty_nodes then () else
do_iter (NodeSet.choose !dirty_nodes)
end end in
begin
global_state := NodeMap.add (cfg.cfg_init_entry) D.init !global_state;
Format.printf "@[<v 0>";
do_init_code cfg.cfg_init_entry; (* do the init code *)
let x = List.hd cfg.cfg_funcs in (* we are ASSUMING main() is function 0*)
global_state := NodeMap.add (x.func_entry) (node_abst cfg.cfg_init_exit !global_state) !global_state;
do_iter x.func_entry;
Format.printf "@]";
Format.printf "@[<v 0>Node states :@ %a@]" pp_nodes (!global_state,cfg.cfg_nodes);
!failed_asserts;
end
end
open Sign
open Constant
open Naked
open Value_domain
module ConstIterator = Iterator(NonRelational(AddTopBot(Constants)))
module SignIterator = Iterator(NonRelational(AddTopBot(Signs)))
(*
let iterate cfg =
let () = Random.self_init () in
let iter_arc arc: unit =
match arc.arc_inst with
| CFG_assert (b, ext) ->
Format.printf "%a@ " Errors.pp_err (AssertFalse, ext, b)
| _ -> () in
(* let iter_arc arc: unit =
match arc.arc_inst with
| CFG_assert (b, ext) ->
Format.printf "%a@ " Errors.pp_err (AssertFalse, ext, b)
| _ -> () in
let iter_node node: unit =
Format.printf "<%i>: ⊤@ " node.node_id in
List.iter iter_arc cfg.cfg_arcs;
Format.printf "Node Values:@ @[<v 0>";
List.iter iter_node cfg.cfg_nodes;
Format.printf "@]"*)
*)

4
libs/dune Normal file
View file

@ -0,0 +1,4 @@
(library
(name libs)
(wrapped false)
(flags (:standard -warn-error -A)))

913
libs/mapext.ml Normal file
View file

@ -0,0 +1,913 @@
(*
Cours "Semantics and applications to verification"
Antoine Miné 2014
Marc Chevalier 2018
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
This file is derived from the map.ml file from the OCaml distribution.
Changes are marked with the [AM] or [MC] symbol.
Based on rev. 10468 2010-05-25 13:29:43Z
[MC] Updated to follow map.ml as in
Based on rev. 2d6ed01bd89099e93b3a8dd7cad941156f70bce5
Thu Feb 22 14:01:15 2018 +0100
Original copyright follows.
*)
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Library General Public License, with *)
(* the special exception on linking described in file ../LICENSE. *)
(* *)
(***********************************************************************)
module type OrderedType =
sig
type t
val compare: t -> t -> int
end
module type S =
sig
type key
type +'a t
val empty: 'a t
val is_empty: 'a t -> bool
val mem: key -> 'a t -> bool
val add: key -> 'a -> 'a t -> 'a t
val update: key -> ('a option -> 'a option) -> 'a t -> 'a t
val singleton: key -> 'a -> 'a t
val remove: key -> 'a t -> 'a t
val merge:
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val union: (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter: (key -> 'a -> unit) -> 'a t -> unit
val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all: (key -> 'a -> bool) -> 'a t -> bool
val exists: (key -> 'a -> bool) -> 'a t -> bool
val filter: (key -> 'a -> bool) -> 'a t -> 'a t
val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal: 'a t -> int
val bindings: 'a t -> (key * 'a) list
val min_binding: 'a t -> (key * 'a)
val min_binding_opt: 'a t -> (key * 'a) option
val max_binding: 'a t -> (key * 'a)
val max_binding_opt: 'a t -> (key * 'a) option
val choose: 'a t -> (key * 'a)
val choose_opt: 'a t -> (key * 'a) option
val split: key -> 'a t -> 'a t * 'a option * 'a t
val find: key -> 'a t -> 'a
val find_opt: key -> 'a t -> 'a option
val find_first: (key -> bool) -> 'a t -> key * 'a
val find_first_opt: (key -> bool) -> 'a t -> (key * 'a) option
val find_last: (key -> bool) -> 'a t -> key * 'a
val find_last_opt: (key -> bool) -> 'a t -> (key * 'a) option
val map: ('a -> 'b) -> 'a t -> 'b t
val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
(* [AM] additions by Antoine Mine' *)
val of_list: (key * 'a) list -> 'a t
val map2: (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val iter2: (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
val fold2: (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val for_all2: (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val exists2: (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val map2z: (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val iter2z: (key -> 'a -> 'a -> unit) -> 'a t -> 'a t -> unit
val fold2z: (key -> 'a -> 'a -> 'b -> 'b) -> 'a t -> 'a t -> 'b -> 'b
val for_all2z: (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
val exists2z: (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
val map2o: (key -> 'a -> 'c) -> (key -> 'b -> 'c) -> (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
val iter2o: (key -> 'a -> unit) -> (key -> 'b -> unit) -> (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
val fold2o: (key -> 'a -> 'c -> 'c) -> (key -> 'b -> 'c -> 'c) -> (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val for_all2o: (key -> 'a -> bool) -> (key -> 'b -> bool) -> (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val exists2o: (key -> 'a -> bool) -> (key -> 'b -> bool) -> (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
val map2zo: (key -> 'a -> 'a) -> (key -> 'a -> 'a) -> (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
val iter2zo: (key -> 'a -> unit) -> (key -> 'a -> unit) -> (key -> 'a -> 'a -> unit) -> 'a t -> 'a t -> unit
val fold2zo: (key -> 'a -> 'b -> 'b) -> (key -> 'a -> 'b -> 'b) -> (key -> 'a -> 'a -> 'b -> 'b) -> 'a t -> 'a t -> 'b -> 'b
val for_all2zo: (key -> 'a -> bool) -> (key -> 'a -> bool) -> (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
val exists2zo: (key -> 'a -> bool) -> (key -> 'a -> bool) -> (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
val map_slice: (key -> 'a -> 'a) -> 'a t -> key -> key -> 'a t
val iter_slice: (key -> 'a -> unit) -> 'a t -> key -> key -> unit
val fold_slice: (key -> 'a -> 'b -> 'b) -> 'a t -> key -> key -> 'b -> 'b
val for_all_slice: (key -> 'a -> bool) -> 'a t -> key -> key -> bool
val exists_slice: (key -> 'a -> bool) -> 'a t -> key -> key -> bool
val key_equal: 'a t -> 'a t -> bool
val key_subset: 'a t -> 'a t -> bool
val find_greater: key -> 'a t -> key * 'a
val find_less: key -> 'a t -> key * 'a
val find_greater_equal: key -> 'a t -> key * 'a
val find_less_equal: key -> 'a t -> key * 'a
end
module Make(Ord: OrderedType) = (struct
type key = Ord.t
(* BEGIN [MC] compatibility with ocaml < 4.03.0 *)
type 'a node_type = {l:'a t; v:key; d:'a; r:'a t; h:int}
and 'a t =
Empty
| Node of 'a node_type
(* END [MC] *)
let height = function
Empty -> 0
| Node {h;_ } -> h
let create l x d r =
let hl = height l and hr = height r in
Node{l; v=x; d; r; h=(if hl >= hr then hl + 1 else hr + 1)}
let singleton x d = Node{l=Empty; v=x; d; r=Empty; h=1}
let bal l x d r =
let hl = match l with Empty -> 0 | Node {h; _} -> h in
let hr = match r with Empty -> 0 | Node {h; _} -> h in
if hl > hr + 2 then begin
match l with
Empty -> invalid_arg "Map.bal"
| Node{l=ll; v=lv; d=ld; r=lr; _} ->
if height ll >= height lr then
create ll lv ld (create lr x d r)
else begin
match lr with
Empty -> invalid_arg "Map.bal"
| Node{l=lrl; v=lrv; d=lrd; r=lrr; _}->
create (create ll lv ld lrl) lrv lrd (create lrr x d r)
end
end else if hr > hl + 2 then begin
match r with
Empty -> invalid_arg "Map.bal"
| Node{l=rl; v=rv; d=rd; r=rr; _} ->
if height rr >= height rl then
create (create l x d rl) rv rd rr
else begin
match rl with
Empty -> invalid_arg "Map.bal"
| Node{l=rll; v=rlv; d=rld; r=rlr; _} ->
create (create l x d rll) rlv rld (create rlr rv rd rr)
end
end else
Node{l; v=x; d; r; h=(if hl >= hr then hl + 1 else hr + 1)}
let empty = Empty
let is_empty = function Empty -> true | _ -> false
let rec add x data = function
Empty ->
Node{l=Empty; v=x; d=data; r=Empty; h=1}
| Node {l; v; d; r; h} as m ->
let c = Ord.compare x v in
if c = 0 then
if d == data then m else Node{l; v=x; d=data; r; h}
else if c < 0 then
let ll = add x data l in
if l == ll then m else bal ll v d r
else
let rr = add x data r in
if r == rr then m else bal l v d rr
let rec find x = function
Empty ->
raise Not_found
| Node {l; v; d; r; _} ->
let c = Ord.compare x v in
if c = 0 then d
else find x (if c < 0 then l else r)
let rec find_first_aux v0 d0 f = function
Empty ->
(v0, d0)
| Node {l; v; d; r; _} ->
if f v then
find_first_aux v d f l
else
find_first_aux v0 d0 f r
let rec find_first f = function
Empty ->
raise Not_found
| Node {l; v; d; r; _} ->
if f v then
find_first_aux v d f l
else
find_first f r
let rec find_first_opt_aux v0 d0 f = function
Empty ->
Some (v0, d0)
| Node {l; v; d; r; _} ->
if f v then
find_first_opt_aux v d f l
else
find_first_opt_aux v0 d0 f r
let rec find_first_opt f = function
Empty ->
None
| Node {l; v; d; r; _} ->
if f v then
find_first_opt_aux v d f l
else
find_first_opt f r
let rec find_last_aux v0 d0 f = function
Empty ->
(v0, d0)
| Node {l; v; d; r; _} ->
if f v then
find_last_aux v d f r
else
find_last_aux v0 d0 f l
let rec find_last f = function
Empty ->
raise Not_found
| Node {l; v; d; r; _} ->
if f v then
find_last_aux v d f r
else
find_last f l
let rec find_last_opt_aux v0 d0 f = function
Empty ->
Some (v0, d0)
| Node {l; v; d; r; _} ->
if f v then
find_last_opt_aux v d f r
else
find_last_opt_aux v0 d0 f l
let rec find_last_opt f = function
Empty ->
None
| Node {l; v; d; r; _} ->
if f v then
find_last_opt_aux v d f r
else
find_last_opt f l
let rec find_opt x = function
Empty ->
None
| Node {l; v; d; r; _} ->
let c = Ord.compare x v in
if c = 0 then Some d
else find_opt x (if c < 0 then l else r)
let rec mem x = function
Empty ->
false
| Node {l; v; r; _} ->
let c = Ord.compare x v in
c = 0 || mem x (if c < 0 then l else r)
let rec min_binding = function
Empty -> raise Not_found
| Node {l=Empty; v; d; _} -> (v, d)
| Node {l; _} -> min_binding l
let rec min_binding_opt = function
Empty -> None
| Node {l=Empty; v; d; _} -> Some (v, d)
| Node {l; _}-> min_binding_opt l
let rec max_binding = function
Empty -> raise Not_found
| Node {v; d; r=Empty; _} -> (v, d)
| Node {r; _} -> max_binding r
let rec max_binding_opt = function
Empty -> None
| Node {v; d; r=Empty; _} -> Some (v, d)
| Node {r; _} -> max_binding_opt r
let rec remove_min_binding = function
Empty -> invalid_arg "Map.remove_min_elt"
| Node {l=Empty; r; _} -> r
| Node {l; v; d; r; _} -> bal (remove_min_binding l) v d r
let merge t1 t2 =
match (t1, t2) with
(Empty, t) -> t
| (t, Empty) -> t
| (_, _) ->
let (x, d) = min_binding t2 in
bal t1 x d (remove_min_binding t2)
let rec remove x = function
Empty ->
Empty
| (Node {l; v; d; r; _} as m) ->
let c = Ord.compare x v in
if c = 0 then merge l r
else if c < 0 then
let ll = remove x l in if l == ll then m else bal ll v d r
else
let rr = remove x r in if r == rr then m else bal l v d rr
let rec update x f = function
Empty ->
begin match f None with
| None -> Empty
| Some data -> Node{l=Empty; v=x; d=data; r=Empty; h=1}
end
| Node {l; v; d; r; h} as m ->
let c = Ord.compare x v in
if c = 0 then begin
match f (Some d) with
| None -> merge l r
| Some data ->
if d == data then m else Node{l; v=x; d=data; r; h}
end else if c < 0 then
let ll = update x f l in
if l == ll then m else bal ll v d r
else
let rr = update x f r in
if r == rr then m else bal l v d rr
let rec iter f = function
Empty -> ()
| Node {l; v; d; r; _} ->
iter f l; f v d; iter f r
let rec map f = function
Empty ->
Empty
| Node {l; v; d; r; h} ->
let l' = map f l in
let d' = f d in
let r' = map f r in
Node{l=l'; v; d=d'; r=r'; h}
let rec mapi f = function
Empty ->
Empty
| Node {l; v; d; r; h} ->
let l' = mapi f l in
let d' = f v d in
let r' = mapi f r in
Node{l=l'; v; d=d'; r=r'; h}
let rec fold f m accu =
match m with
Empty -> accu
| Node {l; v; d; r; _} ->
fold f r (f v d (fold f l accu))
let rec for_all p = function
Empty -> true
| Node {l; v; d; r; _} -> p v d && for_all p l && for_all p r
let rec exists p = function
Empty -> false
| Node {l; v; d; r; _} -> p v d || exists p l || exists p r
(* Beware: those two functions assume that the added k is *strictly*
smaller (or bigger) than all the present keys in the tree; it
does not test for equality with the current min (or max) key.
Indeed, they are only used during the "join" operation which
respects this precondition.
*)
let rec add_min_binding k x = function
| Empty -> singleton k x
| Node {l; v; d; r; _} ->
bal (add_min_binding k x l) v d r
let rec add_max_binding k x = function
| Empty -> singleton k x
| Node {l; v; d; r; _} ->
bal l v d (add_max_binding k x r)
(* Same as create and bal, but no assumptions are made on the
relative heights of l and r. *)
let rec join l v d r =
match (l, r) with
(Empty, _) -> add_min_binding v d r
| (_, Empty) -> add_max_binding v d l
| (Node{l=ll; v=lv; d=ld; r=lr; h=lh}, Node{l=rl; v=rv; d=rd; r=rr; h=rh}) ->
if lh > rh + 2 then bal ll lv ld (join lr v d r) else
if rh > lh + 2 then bal (join l v d rl) rv rd rr else
create l v d r
(* Merge two trees l and r into one.
All elements of l must precede the elements of r.
No assumption on the heights of l and r. *)
let concat t1 t2 =
match (t1, t2) with
(Empty, t) -> t
| (t, Empty) -> t
| (_, _) ->
let (x, d) = min_binding t2 in
join t1 x d (remove_min_binding t2)
let concat_or_join t1 v d t2 =
match d with
| Some d -> join t1 v d t2
| None -> concat t1 t2
let rec split x = function
Empty ->
(Empty, None, Empty)
| Node {l; v; d; r; _} ->
let c = Ord.compare x v in
if c = 0 then (l, Some d, r)
else if c < 0 then
let (ll, pres, rl) = split x l in (ll, pres, join rl v d r)
else
let (lr, pres, rr) = split x r in (join l v d lr, pres, rr)
let rec merge f s1 s2 =
match (s1, s2) with
(Empty, Empty) -> Empty
| (Node {l=l1; v=v1; d=d1; r=r1; h=h1}, _) when h1 >= height s2 ->
let (l2, d2, r2) = split v1 s2 in
concat_or_join (merge f l1 l2) v1 (f v1 (Some d1) d2) (merge f r1 r2)
| (_, Node {l=l2; v=v2; d=d2; r=r2; _}) ->
let (l1, d1, r1) = split v2 s1 in
concat_or_join (merge f l1 l2) v2 (f v2 d1 (Some d2)) (merge f r1 r2)
| _ ->
assert false
let rec union f s1 s2 =
match (s1, s2) with
| (Empty, s) | (s, Empty) -> s
| (Node {l=l1; v=v1; d=d1; r=r1; h=h1}, Node {l=l2; v=v2; d=d2; r=r2; h=h2}) ->
if h1 >= h2 then
let (l2, d2, r2) = split v1 s2 in
let l = union f l1 l2 and r = union f r1 r2 in
match d2 with
| None -> join l v1 d1 r
| Some d2 -> concat_or_join l v1 (f v1 d1 d2) r
else
let (l1, d1, r1) = split v2 s1 in
let l = union f l1 l2 and r = union f r1 r2 in
match d1 with
| None -> join l v2 d2 r
| Some d1 -> concat_or_join l v2 (f v2 d1 d2) r
let rec filter p = function
Empty -> Empty
| Node {l; v; d; r; _} as m ->
(* call [p] in the expected left-to-right order *)
let l' = filter p l in
let pvd = p v d in
let r' = filter p r in
if pvd then if l==l' && r==r' then m else join l' v d r'
else concat l' r'
let rec partition p = function
Empty -> (Empty, Empty)
| Node {l; v; d; r; _} ->
(* call [p] in the expected left-to-right order *)
let (lt, lf) = partition p l in
let pvd = p v d in
let (rt, rf) = partition p r in
if pvd
then (join lt v d rt, concat lf rf)
else (concat lt rt, join lf v d rf)
type 'a enumeration = End | More of key * 'a * 'a t * 'a enumeration
let rec cons_enum m e =
match m with
Empty -> e
| Node {l; v; d; r; _} -> cons_enum l (More(v, d, r, e))
let compare cmp m1 m2 =
let rec compare_aux e1 e2 =
match (e1, e2) with
(End, End) -> 0
| (End, _) -> -1
| (_, End) -> 1
| (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
let c = Ord.compare v1 v2 in
if c <> 0 then c else
let c = cmp d1 d2 in
if c <> 0 then c else
compare_aux (cons_enum r1 e1) (cons_enum r2 e2)
in compare_aux (cons_enum m1 End) (cons_enum m2 End)
let equal cmp m1 m2 =
let rec equal_aux e1 e2 =
match (e1, e2) with
(End, End) -> true
| (End, _) -> false
| (_, End) -> false
| (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) ->
Ord.compare v1 v2 = 0 && cmp d1 d2 &&
equal_aux (cons_enum r1 e1) (cons_enum r2 e2)
in equal_aux (cons_enum m1 End) (cons_enum m2 End)
let rec cardinal = function
Empty -> 0
| Node {l; r; _} -> cardinal l + 1 + cardinal r
let rec bindings_aux accu = function
Empty -> accu
| Node {l; v; d; r; _} -> bindings_aux ((v, d) :: bindings_aux accu r) l
let bindings s =
bindings_aux [] s
let choose = min_binding
let choose_opt = min_binding_opt
(* [AM] additions by Antoine Mine' *)
(* ******************************* *)
let of_list l =
List.fold_left (fun acc (k,x) -> add k x acc) empty l
(* similar to split, but returns unbalanced trees *)
let rec cut k = function
Empty -> Empty,None,Empty
| Node {l=l1;v=k1;d=d1;r=r1;h=h1} ->
let c = Ord.compare k k1 in
if c < 0 then
let l2,d2,r2 = cut k l1 in (l2,d2,Node {l=r2;v=k1;d=d1;r=r1;h=h1})
else if c > 0 then
let l2,d2,r2 = cut k r1 in (Node {l=l1;v=k1;d=d1;r=l2;h=h1},d2,r2)
else (l1,Some d1,r1)
(* binary operations that fail on maps with different keys *)
(* functions are called in increasing key order *)
let rec map2 f m1 m2 =
match m1 with
| Empty -> if m2 = Empty then Empty else invalid_arg "Mapext.map2"
| Node {l=l1;v=k;d=d1;r=r1;h=h1} ->
match cut k m2 with
| l2, Some d2, r2 ->
Node {l=map2 f l1 l2; v=k; d=f k d1 d2; r=map2 f r1 r2; h=h1}
| _, None, _ -> invalid_arg "Mapext.map2"
let rec iter2 f m1 m2 =
match m1 with
| Empty -> if m2 = Empty then () else invalid_arg "Mapext.iter2"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 -> iter2 f l1 l2; f k d1 d2; iter2 f r1 r2
| _, None, _ -> invalid_arg "Mapext.iter2"
let rec fold2 f m1 m2 acc =
match m1 with
| Empty -> if m2 = Empty then acc else invalid_arg "Mapext.fold2"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
fold2 f r1 r2 (f k d1 d2 (fold2 f l1 l2 acc))
| _, None, _ -> invalid_arg "Mapext.fold2"
let rec for_all2 f m1 m2 =
match m1 with
| Empty -> if m2 = Empty then true else invalid_arg "Mapext.for_all2"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
for_all2 f l1 l2 && f k d1 d2 && for_all2 f r1 r2
| _, None, _ -> invalid_arg "Mapext.for_all2"
let rec exists2 f m1 m2 =
match m1 with
| Empty -> if m2 = Empty then false else invalid_arg "Mapext.exists2"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
exists2 f l1 l2 || f k d1 d2 || exists2 f r1 r2
| _, None, _ -> invalid_arg "Mapext.exists2"
(* as above, but ignore physically equal subtrees
- for map, assumes: f k d d = d
- for iter, assumes: f k d d has no effect
- for fold, assumes: k f d d acc = acc
- for for_all, assumes: f k d d = true
- for exists, assumes: f k d d = false
*)
let rec map2z f m1 m2 =
if m1 == m2 then m1 else
match m1 with
| Empty -> if m2 = Empty then Empty else invalid_arg "Mapext.map2z"
| Node {l=l1;v=k;d=d1;r=r1;h=h1} ->
match cut k m2 with
| l2, Some d2, r2 ->
let d = if d1 == d2 then d1 else f k d1 d2 in
Node {l=map2z f l1 l2; v=k; d=d; r=map2z f r1 r2; h=h1}
| _, None, _ -> invalid_arg "Mapext.map2z"
let rec iter2z f m1 m2 =
if m1 == m2 then () else
match m1 with
| Empty -> if m2 = Empty then () else invalid_arg "Mapext.iter2z"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
iter2z f l1 l2; (if d1 != d2 then f k d1 d2); iter2z f r1 r2
| _, None, _ -> invalid_arg "Mapext.iter2z"
let rec fold2z f m1 m2 acc =
if m1 == m2 then acc else
match m1 with
| Empty -> if m2 = Empty then acc else invalid_arg "Mapext.fold2z"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
let acc = fold2z f l1 l2 acc in
let acc = if d1 == d2 then acc else f k d1 d2 acc in
fold2z f r1 r2 acc
| _, None, _ -> invalid_arg "Mapext.fold2z"
let rec for_all2z f m1 m2 =
(m1 == m2) ||
(match m1 with
| Empty -> if m2 = Empty then true else invalid_arg "Mapext.for_all2z"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
(for_all2z f l1 l2) &&
(d1 == d2 || f k d1 d2) &&
(for_all2z f r1 r2)
| _, None, _ -> invalid_arg "Mapext.for_all2z"
)
let rec exists2z f m1 m2 =
(m1 != m2) &&
(match m1 with
| Empty -> if m2 = Empty then false else invalid_arg "Mapext.exists2z"
| Node {l=l1;v=k;d=d1;r=r1;_} ->
match cut k m2 with
| l2, Some d2, r2 ->
(exists2z f l1 l2) ||
(d1 != d2 && f k d1 d2) ||
(exists2z f r1 r2)
| _, None, _ -> invalid_arg "Mapext.exists2z"
)
(* as above, but allow maps with different keys *)
let rec map2o f1 f2 f m1 m2 =
match m1 with
| Empty -> mapi f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
let l = map2o f1 f2 f l1 l2 in
let d = match d2 with None -> f1 k d1 | Some d2 -> f k d1 d2 in
let r = map2o f1 f2 f r1 r2 in
join l k d r
let rec iter2o f1 f2 f m1 m2 =
match m1 with
| Empty -> iter f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
iter2o f1 f2 f l1 l2;
(match d2 with None -> f1 k d1 | Some d2 -> f k d1 d2);
iter2o f1 f2 f r1 r2
let rec fold2o f1 f2 f m1 m2 acc =
match m1 with
| Empty -> fold f2 m2 acc
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
let acc = fold2o f1 f2 f l1 l2 acc in
let acc = match d2 with
| None -> f1 k d1 acc | Some d2 -> f k d1 d2 acc
in
fold2o f1 f2 f r1 r2 acc
let rec for_all2o f1 f2 f m1 m2 =
match m1 with
| Empty -> for_all f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
(for_all2o f1 f2 f l1 l2) &&
(match d2 with None -> f1 k d1 | Some d2 -> f k d1 d2) &&
(for_all2o f1 f2 f r1 r2)
let rec exists2o f1 f2 f m1 m2 =
match m1 with
| Empty -> exists f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
(exists2o f1 f2 f l1 l2) ||
(match d2 with None -> f1 k d1 | Some d2 -> f k d1 d2) ||
(exists2o f1 f2 f r1 r2)
(* all together now *)
let rec map2zo f1 f2 f m1 m2 =
if m1 == m2 then m1 else
match m1 with
| Empty -> mapi f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
let l = map2zo f1 f2 f l1 l2 in
let d = match d2 with
| None -> f1 k d1
| Some d2 -> if d1 == d2 then d1 else f k d1 d2
in
let r = map2zo f1 f2 f r1 r2 in
join l k d r
let rec iter2zo f1 f2 f m1 m2 =
if m1 == m2 then () else
match m1 with
| Empty -> iter f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
iter2zo f1 f2 f l1 l2;
(match d2 with
| None -> f1 k d1
| Some d2 -> if d1 != d2 then f k d1 d2);
iter2zo f1 f2 f r1 r2
let rec fold2zo f1 f2 f m1 m2 acc =
if m1 == m2 then acc else
match m1 with
| Empty -> fold f2 m2 acc
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
let acc = fold2zo f1 f2 f l1 l2 acc in
let acc = match d2 with
| None -> f1 k d1 acc
| Some d2 -> if d1 == d2 then acc else f k d1 d2 acc
in
fold2zo f1 f2 f r1 r2 acc
let rec for_all2zo f1 f2 f m1 m2 =
(m1 == m2) ||
(match m1 with
| Empty -> for_all f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
(for_all2zo f1 f2 f l1 l2) &&
(match d2 with None -> f1 k d1 | Some d2 -> d1 == d2 || f k d1 d2) &&
(for_all2zo f1 f2 f r1 r2)
)
let rec exists2zo f1 f2 f m1 m2 =
(m1 != m2) &&
(match m1 with
| Empty -> exists f2 m2
| Node {l=l1;v=k;d=d1;r=r1;_} ->
let l2, d2, r2 = cut k m2 in
(exists2zo f1 f2 f l1 l2) ||
(match d2 with None -> f1 k d1 | Some d2 -> d1 != d2 && f k d1 d2) ||
(exists2zo f1 f2 f r1 r2)
)
(* iterators limited to keys between two bounds *)
let rec map_slice f m lo hi =
match m with
| Empty -> Empty
| Node {l;v=k;d;r;h} ->
let c1, c2 = Ord.compare k lo, Ord.compare k hi in
let l = if c1 > 0 then map_slice f l lo k else l in
let d = if c1 >= 0 && c2 <= 0 then f k d else d in
let r = if c2 < 0 then map_slice f r k hi else r in
Node {l;v=k;d;r;h}
let rec iter_slice f m lo hi =
match m with
| Empty -> ()
| Node {l=l;v=k;d=d;r=r;h=_} ->
let c1, c2 = Ord.compare k lo, Ord.compare k hi in
if c1 > 0 then iter_slice f l lo k;
if c1 >= 0 && c2 <= 0 then f k d;
if c2 < 0 then iter_slice f r k hi
let rec fold_slice f m lo hi acc =
match m with
| Empty -> acc
| Node {l=l;v=k;d=d;r=r;h=_} ->
let c1, c2 = Ord.compare k lo, Ord.compare k hi in
let acc = if c1 > 0 then fold_slice f l lo k acc else acc in
let acc = if c1 >= 0 && c2 <= 0 then f k d acc else acc in
if c2 < 0 then fold_slice f r k hi acc else acc
let rec for_all_slice f m lo hi =
match m with
| Empty -> true
| Node {l=l;v=k;d=d;r=r;h=_} ->
let c1, c2 = Ord.compare k lo, Ord.compare k hi in
(c1 <= 0 || for_all_slice f l lo k) &&
(c1 < 0 || c2 > 0 || f k d) &&
(c2 >= 0 || for_all_slice f r k hi)
let rec exists_slice f m lo hi =
match m with
| Empty -> false
| Node {l=l;v=k;d=d;r=r;h=_} ->
let c1, c2 = Ord.compare k lo, Ord.compare k hi in
(c1 > 0 && exists_slice f l lo k) ||
(c1 >= 0 && c2 <= 0 && f k d) ||
(c2 < 0 && exists_slice f r k hi)
(* key set comparison *)
let rec key_equal m1 m2 =
(m1 == m2) ||
(match m1 with
| Empty -> m2 = Empty
| Node {l=l1;v=k;d=_;r=r1;h=_} ->
match cut k m2 with
| _, None, _ -> false
| l2, Some _, r2 -> key_equal l1 l2 && key_equal r1 r2
)
let rec key_subset m1 m2 =
(m1 == m2) ||
(match m1 with
| Empty -> true
| Node {l=l1;v=k;d=_;r=r1;h=_} ->
match cut k m2 with
| _, None, _ -> false
| l2, Some _, r2 -> key_subset l1 l2 && key_subset r1 r2
)
(* nagivation *)
let find_greater_equal k m =
let rec aux m found = match m with
| Empty -> (match found with None -> raise Not_found | Some x -> x)
| Node {l=l;v=kk;d=d;r=r;h=_} ->
let c = Ord.compare k kk in
if c = 0 then kk, d else
if c > 0 then aux r found else
aux l (Some (kk, d))
in
aux m None
let find_greater k m =
let rec aux m found = match m with
| Empty -> (match found with None -> raise Not_found | Some x -> x)
| Node {l=l;v=kk;d=d;r=r;h=_} ->
let c = Ord.compare k kk in
if c >= 0 then aux r found else
aux l (Some (kk, d))
in
aux m None
let find_less_equal k m =
let rec aux m found = match m with
| Empty -> (match found with None -> raise Not_found | Some x -> x)
| Node {l=l;v=kk;d=d;r=r;h=_} ->
let c = Ord.compare k kk in
if c = 0 then kk, d else
if c < 0 then aux l found else
aux r (Some (kk, d))
in
aux m None
let find_less k m =
let rec aux m found = match m with
| Empty -> (match found with None -> raise Not_found | Some x -> x)
| Node {l=l;v=kk;d=d;r=r;h=_} ->
let c = Ord.compare k kk in
if c <= 0 then aux l found else
aux r (Some (kk, d))
in
aux m None
end: S with type key = Ord.t)

588
libs/mapext.mli Normal file
View file

@ -0,0 +1,588 @@
(*
Cours "Semantics and applications to verification"
Antoine Miné 2014
Marc Chevalier 2018
Ecole normale supérieure, Paris, France / CNRS / INRIA
*)
(*
This file is derived from the map.mli file from the OCaml distribution.
Changes are marked with the [AM] symbol.
Based on rev. 10632 2010-07-24 14:16:58Z.
[MC] Updated to follow map.mli as in
Based on rev. 2d6ed01bd89099e93b3a8dd7cad941156f70bce5
Thu Feb 22 14:01:15 2018 +0100
Original copyright follows.
*)
(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
(** Association tables over ordered types.
This module implements applicative association tables, also known as
finite maps or dictionaries, given a total ordering function
over the keys.
All operations over maps are purely applicative (no side-effects).
The implementation uses balanced binary trees, and therefore searching
and insertion take time logarithmic in the size of the map.
For instance:
{[
module IntPairs =
struct
type t = int * int
let compare (x0,y0) (x1,y1) =
match Pervasives.compare x0 x1 with
0 -> Pervasives.compare y0 y1
| c -> c
end
module PairsMap = Map.Make(IntPairs)
let m = PairsMap.(empty |> add (0,1) "hello" |> add (1,0) "world")
]}
This creates a new module [PairsMap], with a new type ['a PairsMap.t]
of maps from [int * int] to ['a]. In this example, [m] contains [string]
values so its type is [string PairsMap.t].
*)
module type OrderedType =
sig
type t
(** The type of the map keys. *)
val compare : t -> t -> int
(** A total ordering function over the keys.
This is a two-argument function [f] such that
[f e1 e2] is zero if the keys [e1] and [e2] are equal,
[f e1 e2] is strictly negative if [e1] is smaller than [e2],
and [f e1 e2] is strictly positive if [e1] is greater than [e2].
Example: a suitable ordering function is the generic structural
comparison function {!Pervasives.compare}. *)
end
(** Input signature of the functor {!Map.Make}. *)
module type S =
sig
type key
(** The type of the map keys. *)
type (+'a) t
(** The type of maps from type [key] to type ['a]. *)
val empty: 'a t
(** The empty map. *)
val is_empty: 'a t -> bool
(** Test whether a map is empty or not. *)
val mem: key -> 'a t -> bool
(** [mem x m] returns [true] if [m] contains a binding for [x],
and [false] otherwise. *)
val add: key -> 'a -> 'a t -> 'a t
(** [add x y m] returns a map containing the same bindings as
[m], plus a binding of [x] to [y]. If [x] was already bound
in [m] to a value that is physically equal to [y],
[m] is returned unchanged (the result of the function is
then physically equal to [m]). Otherwise, the previous binding
of [x] in [m] disappears.
@before 4.03 Physical equality was not ensured. *)
val update: key -> ('a option -> 'a option) -> 'a t -> 'a t
(** [update x f m] returns a map containing the same bindings as
[m], except for the binding of [x]. Depending on the value of
[y] where [y] is [f (find_opt x m)], the binding of [x] is
added, removed or updated. If [y] is [None], the binding is
removed if it exists; otherwise, if [y] is [Some z] then [x]
is associated to [z] in the resulting map. If [x] was already
bound in [m] to a value that is physically equal to [z], [m]
is returned unchanged (the result of the function is then
physically equal to [m]).
@since 4.06.0
*)
val singleton: key -> 'a -> 'a t
(** [singleton x y] returns the one-element map that contains a binding [y]
for [x].
@since 3.12.0
*)
val remove: key -> 'a t -> 'a t
(** [remove x m] returns a map containing the same bindings as
[m], except for [x] which is unbound in the returned map.
If [x] was not in [m], [m] is returned unchanged
(the result of the function is then physically equal to [m]).
@before 4.03 Physical equality was not ensured. *)
val merge:
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
(** [merge f m1 m2] computes a map whose keys is a subset of keys of [m1]
and of [m2]. The presence of each such binding, and the corresponding
value, is determined with the function [f].
In terms of the [find_opt] operation, we have
[find_opt x (merge f m1 m2) = f (find_opt x m1) (find_opt x m2)]
for any key [x], provided that [f None None = None].
@since 3.12.0
*)
val union: (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
(** [union f m1 m2] computes a map whose keys is the union of keys
of [m1] and of [m2]. When the same binding is defined in both
arguments, the function [f] is used to combine them.
This is a special case of [merge]: [union f m1 m2] is equivalent
to [merge f' m1 m2], where
- [f' None None = None]
- [f' (Some v) None = Some v]
- [f' None (Some v) = Some v]
- [f' (Some v1) (Some v2) = f v1 v2]
@since 4.03.0
*)
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
(** Total ordering between maps. The first argument is a total ordering
used to compare data associated with equal keys in the two maps. *)
val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
(** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are
equal, that is, contain equal keys and associate them with
equal data. [cmp] is the equality predicate used to compare
the data associated with the keys. *)
val iter: (key -> 'a -> unit) -> 'a t -> unit
(** [iter f m] applies [f] to all bindings in map [m].
[f] receives the key as first argument, and the associated value
as second argument. The bindings are passed to [f] in increasing
order with respect to the ordering over the type of the keys. *)
val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
(** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)],
where [k1 ... kN] are the keys of all bindings in [m]
(in increasing order), and [d1 ... dN] are the associated data. *)
val for_all: (key -> 'a -> bool) -> 'a t -> bool
(** [for_all p m] checks if all the bindings of the map
satisfy the predicate [p].
@since 3.12.0
*)
val exists: (key -> 'a -> bool) -> 'a t -> bool
(** [exists p m] checks if at least one binding of the map
satisfies the predicate [p].
@since 3.12.0
*)
val filter: (key -> 'a -> bool) -> 'a t -> 'a t
(** [filter p m] returns the map with all the bindings in [m]
that satisfy predicate [p]. If [p] satisfies every binding in [m],
[m] is returned unchanged (the result of the function is then
physically equal to [m])
@since 3.12.0
@before 4.03 Physical equality was not ensured.
*)
val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
(** [partition p m] returns a pair of maps [(m1, m2)], where
[m1] contains all the bindings of [s] that satisfy the
predicate [p], and [m2] is the map with all the bindings of
[s] that do not satisfy [p].
@since 3.12.0
*)
val cardinal: 'a t -> int
(** Return the number of bindings of a map.
@since 3.12.0
*)
val bindings: 'a t -> (key * 'a) list
(** Return the list of all bindings of the given map.
The returned list is sorted in increasing order with respect
to the ordering [Ord.compare], where [Ord] is the argument
given to {!Map.Make}.
@since 3.12.0
*)
val min_binding: 'a t -> (key * 'a)
(** Return the smallest binding of the given map
(with respect to the [Ord.compare] ordering), or raise
[Not_found] if the map is empty.
@since 3.12.0
*)
val min_binding_opt: 'a t -> (key * 'a) option
(** Return the smallest binding of the given map
(with respect to the [Ord.compare] ordering), or [None]
if the map is empty.
@since 4.05
*)
val max_binding: 'a t -> (key * 'a)
(** Same as {!Map.S.min_binding}, but returns the largest binding
of the given map.
@since 3.12.0
*)
val max_binding_opt: 'a t -> (key * 'a) option
(** Same as {!Map.S.min_binding_opt}, but returns the largest binding
of the given map.
@since 4.05
*)
val choose: 'a t -> (key * 'a)
(** Return one binding of the given map, or raise [Not_found] if
the map is empty. Which binding is chosen is unspecified,
but equal bindings will be chosen for equal maps.
@since 3.12.0
*)
val choose_opt: 'a t -> (key * 'a) option
(** Return one binding of the given map, or [None] if
the map is empty. Which binding is chosen is unspecified,
but equal bindings will be chosen for equal maps.
@since 4.05
*)
val split: key -> 'a t -> 'a t * 'a option * 'a t
(** [split x m] returns a triple [(l, data, r)], where
[l] is the map with all the bindings of [m] whose key
is strictly less than [x];
[r] is the map with all the bindings of [m] whose key
is strictly greater than [x];
[data] is [None] if [m] contains no binding for [x],
or [Some v] if [m] binds [v] to [x].
@since 3.12.0
*)
val find: key -> 'a t -> 'a
(** [find x m] returns the current binding of [x] in [m],
or raises [Not_found] if no such binding exists. *)
val find_opt: key -> 'a t -> 'a option
(** [find_opt x m] returns [Some v] if the current binding of [x]
in [m] is [v], or [None] if no such binding exists.
@since 4.05
*)
val find_first: (key -> bool) -> 'a t -> key * 'a
(** [find_first f m], where [f] is a monotonically increasing function,
returns the binding of [m] with the lowest key [k] such that [f k],
or raises [Not_found] if no such key exists.
For example, [find_first (fun k -> Ord.compare k x >= 0) m] will return
the first binding [k, v] of [m] where [Ord.compare k x >= 0]
(intuitively: [k >= x]), or raise [Not_found] if [x] is greater than any
element of [m].
@since 4.05
*)
val find_first_opt: (key -> bool) -> 'a t -> (key * 'a) option
(** [find_first_opt f m], where [f] is a monotonically increasing function,
returns an option containing the binding of [m] with the lowest key [k]
such that [f k], or [None] if no such key exists.
@since 4.05
*)
val find_last: (key -> bool) -> 'a t -> key * 'a
(** [find_last f m], where [f] is a monotonically decreasing function,
returns the binding of [m] with the highest key [k] such that [f k],
or raises [Not_found] if no such key exists.
@since 4.05
*)
val find_last_opt: (key -> bool) -> 'a t -> (key * 'a) option
(** [find_last_opt f m], where [f] is a monotonically decreasing function,
returns an option containing the binding of [m] with the highest key [k]
such that [f k], or [None] if no such key exists.
@since 4.05
*)
val map: ('a -> 'b) -> 'a t -> 'b t
(** [map f m] returns a map with same domain as [m], where the
associated value [a] of all bindings of [m] has been
replaced by the result of the application of [f] to [a].
The bindings are passed to [f] in increasing order
with respect to the ordering over the type of the keys. *)
val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
(** Same as {!Map.S.map}, but the function receives as arguments both the
key and the associated value for each binding of the map. *)
(* [AM] additions *)
(** {2 Additional functions} *)
val of_list: (key * 'a) list -> 'a t
(** [of_list l] converts an association list to a map. *)
val map2: (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
(** [map2 f m1 m2] is similar to [map] but applies [f] to pairs
of bindings [a1] from [m1] and [a2] from [m2] corresponding to
the same key to construct a new map with the same key set.
[m1] and [m2] must have the same key sets.
The binging are passed to [f] in increasing order of key. *)
val iter2: (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
(** [iter2 f m1 m2] is similar to [map] but applies [f] to pairs
of bindings [a1] from [m1] and [a2] from [m2] corresponding to
the same key.
[m1] and [m2] must have the same key sets.
The binging are passed to [f] in increasing order of key. *)
val fold2: (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
(** [fold2 f m1 m2 x] is similar to [fold] but applies [f] to pairs
of bindings [a1] from [m1] and [a2] from [m2] corresponding to
the same key.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val for_all2: (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
(** [for_all2 f m1 m2] is similar to [for_all] but applies [f] to pairs
of bindings [a1] from [m1] and [a2] from [m2] corresponding to
the same key.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val exists2: (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
(** [exists2 f m1 m2] is similar to [exists] but applies [f] to pairs
of bindings [a1] from [m1] and [a2] from [m2] corresponding to
the same key.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val map2z: (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
(** [map2z f m1 m2] is similar to [map2 f m1 m2], but physically
equal subtrees are put unchanged into the result instead of
being traversed.
This is more efficient than [map2], and equivalent if [f] is
side-effect free and idem-potent ([f k a a = a]).
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val iter2z: (key -> 'a -> 'a -> unit) -> 'a t -> 'a t -> unit
(** [iter2z f m1 m2] is similar to [iter2 f m1 m2], but physically
equal subtrees are ignored.
This is more efficient than [iter2], and equivalent if
[f k a a] has no effect.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val fold2z: (key -> 'a -> 'a -> 'b -> 'b) -> 'a t -> 'a t -> 'b -> 'b
(** [fold2z f m1 m2 a] is similar to [fold2 f m1 m2 a], but physically
equal subtrees are ignored.
This is more efficient than [fold2], and equivalent if
[f k a a x = x] and has no effect.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val for_all2z: (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
(** [for_all2z f m1 m2] is similar to [for_all2 f m1 m2], but returns
[true] for physically equal subtrees without traversing them.
This is more efficient than [for_all2z], and equivalent if
[f k a a = true] and has no effect.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val exists2z: (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
(** [exists2z f m1 m2] is similar to [exists2 f m1 m2], but returns
[false] for physically equal subtrees without traversing them.
This is more efficient than [exists2z], and equivalent if
[f k a a = false] and has no effect.
[m1] and [m2] must have the same key sets.
The bindings are passed to [f] in increasing order of keys. *)
val map2o: (key -> 'a -> 'c) -> (key -> 'b -> 'c) -> (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
(** [map2o f1 f2 f m1 m2] is similar to [map2 f m1 m2], but
accepts maps defined over different sets of keys.
To get a new binding, [f1] is used for keys appearing only
in [m1], [f2] for keys appearing only in [m2], and [f] for
keys appearing in both maps.
The returned map has bindings for all keys appearing in either
[m1] or [m2].
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val iter2o: (key -> 'a -> unit) -> (key -> 'b -> unit) -> (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
(** [iter2o f1 f2 f m1 m2] is similar to [iter2 f m1 m2], but
accepts maps defined over different sets of keys.
[f1] is called for keys appearing only in [m1],
[f2] for keys appearing only in [m2],
and [f] for keys appearing in both maps.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val fold2o: (key -> 'a -> 'c -> 'c) -> (key -> 'b -> 'c -> 'c) -> (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
(** [fold2o f1 f2 f m1 m2 a] is similar to [fold2 f m1 m2 a], but
accepts maps defined over different sets of keys.
[f1] is called for keys appearing only in [m1],
[f2] for keys appearing only in [m2],
and [f] for keys appearing in both maps.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val for_all2o: (key -> 'a -> bool) -> (key -> 'b -> bool) -> (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
(** [for_all2o f1 f2 f m1 m2] is similar to [for_all2 f m1 m2], but
accepts maps defined over different sets of keys.
[f1] is called for keys appearing only in [m1],
[f2] for keys appearing only in [m2],
and [f] for keys appearing in both maps.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val exists2o: (key -> 'a -> bool) -> (key -> 'b -> bool) -> (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool
(** [fexists2o f1 f2 f m1 m2] is similar to [fexists2 f m1 m2], but
accepts maps defined over different sets of keys.
[f1] is called for keys appearing only in [m1],
[f2] for keys appearing only in [m2],
and [f] for keys appearing in both maps.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val map2zo: (key -> 'a -> 'a) -> (key -> 'a -> 'a) -> (key -> 'a -> 'a -> 'a) -> 'a t -> 'a t -> 'a t
(** [map2zo f1 f2 f m1 m2] is similar to [map2o f1 f2 f m1 m2] but,
similary to [map2z], [f] is not called on physically equal
subtrees.
This is more efficient than [map2o], and equivalent if [f] is
side-effect free and idem-potent ([f k a a = a]).
The returned map has bindings for all keys appearing in either
[m1] or [m2].
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val iter2zo: (key -> 'a -> unit) -> (key -> 'a -> unit) -> (key -> 'a -> 'a -> unit) -> 'a t -> 'a t -> unit
(** [iter2zo f1 f2 f m1 m2] is similar to [iter2o f1 f2 f m1 m2] but,
similary to [iter2z], [f] is not called on physically equal
subtrees.
This is more efficient than [iter2o], and equivalent if [f] is
side-effect free.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val fold2zo: (key -> 'a -> 'b -> 'b) -> (key -> 'a -> 'b -> 'b) -> (key -> 'a -> 'a -> 'b -> 'b) -> 'a t -> 'a t -> 'b -> 'b
(** [fold2zo f1 f2 f m1 m2 a] is similar to [fold2o f1 f2 f m1 m2 a] but,
similary to [fold2z], [f] is not called on physically equal
subtrees.
This is more efficient than [fold2o], and equivalent if
[f k a a x = x] and has no side-effect.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val for_all2zo: (key -> 'a -> bool) -> (key -> 'a -> bool) -> (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
(** [for_all2zo f1 f2 f m1 m2] is similar to [for_all2o f1 f2 f m1 m2] but,
similary to [for_all2z], [f] is not called on physically equal
subtrees.
This is more efficient than [for_all2o], and equivalent if
[f k a a = true] and has no side-effect.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val exists2zo: (key -> 'a -> bool) -> (key -> 'a -> bool) -> (key -> 'a -> 'a -> bool) -> 'a t -> 'a t -> bool
(** [exists2zo f1 f2 f m1 m2] is similar to [exists2o f1 f2 f m1 m2] but,
similary to [exists2z], [f] is not called on physically equal
subtrees.
This is more efficient than [exists2o], and equivalent if
[f k a a = false] and has no side-effect.
The bindings are passed to [f], [f1], [f2] in increasing order of keys. *)
val map_slice: (key -> 'a -> 'a) -> 'a t -> key -> key -> 'a t
(** [map_slice f m k1 k2] is similar to [map f m], but only applies
[f] to bindings with key greater or equal to [k1] and smaller
or equal to [k2] to construct the returned map. Bindings with
keys outside this range in [m] are put unchanged in the result.
It is as if, outside this range, [f k a = a] and has no effect.
The result has the same key set as [m].
The bindings are passed to [f] in increasing order of keys,
between [k1] and [k2]. *)
val iter_slice: (key -> 'a -> unit) -> 'a t -> key -> key -> unit
(** [iter_slice f m k1 k2] is similar to [iter f m], but only calls
[f] on bindings with key greater or equal to [k1] and smaller
or equal to [k2].
It is as if, outside this range, [f k a] has no effect.
The bindings are passed to [f] in increasing order of keys,
between [k1] and [k2]. *)
val fold_slice: (key -> 'a -> 'b -> 'b) -> 'a t -> key -> key -> 'b -> 'b
(** [fold_slice f m k1 k2 a] is similar to [fold f m], but only calls
[f] on bindings with key greater or equal to [k1] and smaller
or equal to [k2].
It is as if, outside this range, [f k a x = x] and has no effect.
The bindings are passed to [f] in increasing order of keys,
between [k1] and [k2]. *)
val for_all_slice: (key -> 'a -> bool) -> 'a t -> key -> key -> bool
(** [for_all_slice f m k1 k2 a] is similar to [for_all f m], but only calls
[f] on bindings with key greater or equal to [k1] and smaller
or equal to [k2].
It is as if, outside this range, [f k a = true] and has no effect.
The bindings are passed to [f] in increasing order of keys,
between [k1] and [k2]. *)
val exists_slice: (key -> 'a -> bool) -> 'a t -> key -> key -> bool
(** [exists_slice f m k1 k2 a] is similar to [exists f m], but only calls
[f] on bindings with key greater or equal to [k1] and smaller
or equal to [k2].
It is as if, outside this range, [f k a = false] and has no effect.
The bindings are passed to [f] in increasing order of keys,
between [k1] and [k2]. *)
val key_equal: 'a t -> 'a t -> bool
(** [key_equal m1 m2] returns true if [m1] and [m2] are defined
over exactly the same set of keys (but with possibly different
values).
*)
val key_subset: 'a t -> 'a t -> bool
(** [key_equal m1 m2] returns true if [m1] is defined on a subset of
the keys of [m2] (but with possibly different values).
*)
val find_greater: key -> 'a t -> key * 'a
(** [find_greater k m] returns the binding (key and value) in [m]
with key strictly greater than [k] and as small as possible.
Raises [Not_found] if [m] has no binding for a key strictly greater
than [k].
*)
val find_less: key -> 'a t -> key * 'a
(** [find_less k m] returns the binding (key and value) in [m]
with key strictly less than [k] and as large as possible.
Raises [Not_found] if [m] has no binding for a key strictly less
than [k].
*)
val find_greater_equal: key -> 'a t -> key * 'a
(** [find_greater_euql k m] returns the binding (key and value) in [m]
with key greater or equal to [k] and as small as possible.
Raises [Not_found] if [m] has no binding for a key greater or equal
to [k].
*)
val find_less_equal: key -> 'a t -> key * 'a
(** [find_less_equal k m] returns the binding (key and value) in [m]
with key less or equal to [k] and as large as possible.
Raises [Not_found] if [m] has no binding for a key less or equal
to [k].
*)
end
(** Output signature of the functor {!Map.Make}. *)
module Make (Ord : OrderedType) : S with type key = Ord.t
(** Functor building an implementation of the map structure
given a totally ordered type. *)

95
scripts/style.css Normal file
View file

@ -0,0 +1,95 @@
h1, h2, h3, h4, h5, h6, div.h7, div.h8, div.h9 {
font-style: monospace;
/*font-family: 'Inria Serif';*/
font-size: 2.5rem;
border: 1px solid #000;
margin-top: 20px;
margin-bottom: 2px;
text-align: center;
padding: 8px;
font-weight: normal;
}
h1 {
/* font-family: 'Inria Serif'; */
font-size: 4rem;
padding: 10px;
background-color: #90FDFF;
width: 100%;
}
h2 { background-color: #90BDFF; }
h3 { background-color: #90DDFF; }
h4 { background-color: #90EDFF; }
h5 { background-color: #90FDFF; }
h6 { background-color: #90BDFF; }
div.h7 { background-color: #90DDFF; }
div.h8 { background-color: #F0FFFF; }
div.h9 { background-color: #FFFFFF; }
body {
font-family: 'Inria Sans';
background-color : #f7f7f7;
font-size: 20px;
max-width: 80%;
margin: auto;
padding-bottom: 4em;
/* white-space: pre-wrap; */
}
td, th {
border: 1px solid black;
padding: 3px 25px;
}
th.bench {
padding: 10px 25px;
background-color: #ccc;
}
table {
border: 1px solid black;
margin-left: auto;
margin-right: auto;
}
div.c {
font-size: 1.5rem;
font-family: 'Ubuntu Mono';
max-width: 130rem;
white-space: pre-wrap;
font-style: monospace;
}
pre {
margin: 0px;
background-color: #e9e9e9;
}
a {
text-decoration: none;
color: #000;
}
a:hover {
text-decoration: underline;
}
footer {
background-color: #bbbbbb;
position: fixed;
width: 100%;
bottom: 0;
size: 10pt;
text-align: center;
left: 0;
bottom: 0;
margin-left: auto;
margin-right: auto;
}
footer a {
color: #4659ff;
}

271
scripts/test.sh Executable file
View file

@ -0,0 +1,271 @@
#!/bin/bash
#
# Cours "Sémantique et Application à la Vérification de programmes"
#
# Josslin Giet 2021
# Ecole normale supérieure, Paris, France / CNRS / INRIA
#
shopt -s lastpipe
RED="\e[91m"
GREEN="\e[92m"
BOLD="\e[1m"
RESET="\e[0m"
BLUE="\e[94m"
fill=" "
# Default solver path. You can change it if you need
analyzer_path=$1
analyzer=$analyzer_path/analyzer
options=$analyzer_path/options.txt
result_folder="results"
index_html="${result_folder}/index.html"
nb_test=0
timeout=0
failure=0
completness=0
soundness=0
# max time allowed
max_time="5s"
all_opts="$2"
if [ "$all_opts" != "" ]; then
echo "Launching code with extra options: '${all_opts}'"
fi
# Pattern for failure in log
patt_assert="line [0-9]*: Assertion failure"
# Pattern for expêctyed failure in file
patt_ko="assert.*//@KO"
create_file() {
file=$1
filename=$(basename $file)
file_html="${result_folder}/${filename}.html"
if [[ ! -e "$file_html" ]]
then
cat "scripts/header.html" > $file_html
sed -i "s@TITLE@${filename}@" $file_html
echo "<h1>${filename}</h1>" >> $file_html
echo "<div class=\"c\">" >> $file_html
cat $file >> $file_html
echo "</div>" >> $file_html
file_svg=$(basename ${file})".svg"
echo "<img src=\"./${file_svg}\" alt=\"graph\">" >> $file_html
fi
}
end_file() {
# After the analysis the cfg.dot should correspond to the current test
dot -Tsvg cfg.dot -o ${result_folder}/${filename}.svg
cat "scripts/footer.html" >> $file_html
}
get_nth_line() {
line=$1
file=$2
sed "${line}q;d" $file
}
treat_file() {
file=$1
log=$2
expected_folder=$3
need_new_line=true
sound_loc=0
compl_loc=0
col_sound="green"
col_compl="green"
# first, we compute the expected failures
if [[ "$expected_folder" == "" ]]
then
nb_expected=$(grep -n "${patt_ko}" $file| wc -l)
expected=$(grep -n "${patt_ko}" $file | grep -o "^[0-9]*")
else
file_folder=$(dirname $file)
file=$(basename $file)
res="${file_folder}/${expected_folder}/${file}.log"
nb_expected=$(grep "${patt_assert}" $res | wc -l)
expected=$(grep "${patt_assert}" $res | grep -o "line [0-9]*" | grep -o "[0-9]*")
fi
# then, we compute the failed assertions
nb_failures=$(grep "${patt_assert}" $log| wc -l)
failures=$(grep "${patt_assert}" $log | grep -o "line [0-9]*" | grep -o "[0-9]*")
echo "<p><span style=\"color: blue;\">Expected:</span> ${expected} </p>" >> $file_html
echo "<p><span style=\"color: blue;\">Failures:</span> ${failures} </p>" >> $file_html
# echo -e "\nnb_expected: ${nb_expected}"
# echo -e "expected:\n--\n${expected}\n--"
# echo -e "nb_failures: ${nb_failures}"
# echo -e "failures:\n--\n${failures}\n--"
# Soundness part: for line number in expected,
# we search for it in failures
for nb in `seq 1 $nb_expected`;
do
cmd="echo \"${expected}\" | head -${nb} | tail -1"
line_nb=$(eval "${cmd}")
echo "${failures}" | grep -q "^${line_nb}$"
found=$?
if [[ $found -ne 0 ]]
then
line=$(get_nth_line $line_nb $file)
col_sound="red"
soundness=$((soundness+1))
sound_loc=$((sound_loc+1))
if [ "$need_new_line" = true ]
then
echo -e "\n${BOLD}${RED} SOUNDNESS ERRORS${RESET}"
need_new_line=false
else
echo -e "${BOLD}${RED} SOUNDNESS ERRORS${RESET}"
fi
echo -e "${RED}missing fail assertions:${RESET}${line}"
echo "<p>${line_nb}<span style=\"color: red;\">${line}</span></p>" >> $file_html
fi
done
# Completness part: for each line number in failures,
# we search for it in expected
for nb in `seq 1 $nb_failures`;
do
cmd="echo \"${failures}\" | head -${nb} | tail -1"
line_nb=$(eval "${cmd}")
echo "${expected}" | grep -q "^${line_nb}$"
found=$?
if [[ $found -ne 0 ]]
then
completness=$((completness+1))
compl_loc=$((compl_loc+1))
col_compl="blue"
line=$(grep "${patt_assert}" $log | head -${nb} | tail -1)
if [ "$need_new_line" = true ]
then
echo -e "\n${BOLD}${BLUE} COMPLETNESS ERROR${RESET}"
need_new_line=false
else
echo -e "${BOLD}${BLUE} COMPLETNESS ERROR${RESET}"
fi
echo -e "${BLUE}unexpected fail assertions:${RESET} ${line}"
echo "<p><span style=\"color: blue;\">${line}</span></p>" >> $file_html
fi
done
echo "<h3>LOG</h3>" >> $file_html
echo "<pre>" >> $file_html
cat $log >> $file_html
echo "</pre>" >> $file_html
if [ "$need_new_line" = false ]
then
echo -e ""
fi
echo -n "<a href=\"../${log}\" target=\"_parent\">" >> $index_html
echo -n "<span style=\"color: ${col_sound};\">${sound_loc}</span>, " >> $index_html
echo -n "<span style=\"color: ${col_compl};\">${compl_loc}</span>" >> $index_html
echo "</a>" >> $index_html
}
treat_examples() {
folder="examples/${1}"
bench_name=$2
options="$3 $all_opts" # analyzer CLI options
expected_folder=$4 # subfolder containing expected result
bench_regexp="${folder}/*.c"
nb_file=$(find $folder -iname "*.c" | wc -l)
nb_test=$(( nb_test + nb_file ))
if [[ $nb_file -eq 0 ]]
then
echo "bench ${bench_name}: No files found (${bench_regexp})"
return
fi
echo "<tr><th colspan=\"100\" class=\"bench\">${bench_name} ${options}</th></tr>" >> $index_html
for file in $(find "${folder}" -iname "*.c" | sort)
do
filename=$(basename $file)
create_file $file
echo "<tr><td><a href=\"${filename}.html\"><pre>${filename}</pre></a></td>" >> $index_html
echo "<td>" >> $index_html
solved=$(($solved+1))
echo -ne "\r\t$file $option $fill"
opt_replaced=$(echo "${options}" | sed "s/ /_/g")
log="${result_folder}/${filename}.${opt_replaced}.txt"
echo "<h2><a href=\"../${log}\">${analyzer} ${options}</a></h2>" >> $file_html
timeout $max_time $analyzer $options $file > $log 2>&1
out=$?
if [[ $out -eq 127 ]]
then
timeout=$((timeout+1))
echo "<a href=\"../${log}\"><span style=\"color: red;\">TO</span></a>" >> $index_html
echo "<span style=\"color: red;\">TO</span>" >> $file_html
echo -e "\n ${BOLD}${RED}TO ${RESET}\n"
echo "<h3>LOG</h3>" >> $file_html
echo "<pre>" >> $file_html
cat $log >> $file_html
echo "</pre>" >> $file_html
elif [[ $out -ne 0 ]]
then
failure=$((failure+1))
echo "<a href=\"../${log}\"><span style=\"color: red;\">FAIL</span></a>" >> $index_html
echo "<span style=\"color: red;\">FAIL</span>" >> $file_html
echo -e "\n ${BOLD}${RED}FAILED ($out) ${RESET}\n"
echo "<h3>LOG</h3>" >> $file_html
echo "<pre>" >> $file_html
cat $log >> $file_html
echo "</pre>" >> $file_html
else
treat_file $file $log $expected_folder
fi
echo "</td>" >> $index_html
echo "</tr>" >> $index_html
end_file $file
done
}
print_end() {
echo " "
echo -e " test:\t${nb_test} (files: ${total})"
if [[ $timeout != 0 ]]
then
echo -e " ${BOLD}Timeout${RED}\tKO (${timeout}) ${RESET}"
fi
if [[ $failure != 0 ]]
then
echo -e " ${BOLD}Failure${RED}\tKO (${failure}) ${RESET}"
fi
if [[ $soundness != 0 ]]
then
echo -e " ${BOLD}Soudness${RED}\tKO (${soundness}) ${RESET}"
else
echo -e " ${BOLD}Soudness${GREEN}\tOK ${RESET}"
fi
if [[ $completness != 0 ]]
then
echo -e " ${BOLD}Completness${RED}\tKO (${completness}) ${RESET}"
else
echo -e " ${BOLD}Completness${GREEN}\tOK ${RESET}"
fi
echo -e "${BOLD}${BLUE}Results written in${RESET}: ${index_html}"
}
mkdir ${result_folder}
cat "scripts/header_main.html" > $index_html
echo "<h1>Overview</h1>" >> $index_html
echo "<table>" >> $index_html
total=$(find $bench -iname "*.c" | wc -l)
solved=0
treat_examples "bool" "Boolean operations" "--domain constants" ""
treat_examples "bool" "Boolean operations" "--domain interval" ""
treat_examples "constant" "Constants operations" "--domain constants" ""
treat_examples "constant_loop" "Constants loops" "--domain constants" ""
treat_examples "constant" "Constants operations (I)" "--domain interval" ""
treat_examples "interval" "Interval operations" "--domain interval" ""
treat_examples "constant_loop" "Constants loops (I)" "--domain interval" ""
treat_examples "interval_loop" "Interval loops" "--domain interval" ""
echo "</table>" >> $index_html
echo "</body>" >> $index_html
echo "</html>" >> $index_html
print_end