diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..09c32ad --- /dev/null +++ b/.gitignore @@ -0,0 +1,8 @@ +*.html +analyzer +results/ +_build/ +*.dot +*.pdf +*.svg +*.tar.gz diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..bf4490c --- /dev/null +++ b/Makefile @@ -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 . diff --git a/analyzer.ml b/analyzer.ml new file mode 100644 index 0000000..8249800 --- /dev/null +++ b/analyzer.ml @@ -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 "@[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 (); diff --git a/domains/constant.ml b/domains/constant.ml new file mode 100644 index 0000000..cdf095e --- /dev/null +++ b/domains/constant.ml @@ -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 + diff --git a/domains/domain.ml b/domains/domain.ml new file mode 100644 index 0000000..03d4e16 --- /dev/null +++ b/domains/domain.ml @@ -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 + diff --git a/domains/dune b/domains/dune new file mode 100644 index 0000000..c61e523 --- /dev/null +++ b/domains/dune @@ -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 )) diff --git a/domains/naked.ml b/domains/naked.ml new file mode 100644 index 0000000..b9229f6 --- /dev/null +++ b/domains/naked.ml @@ -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 diff --git a/domains/sign.ml b/domains/sign.ml new file mode 100644 index 0000000..fbf271c --- /dev/null +++ b/domains/sign.ml @@ -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 diff --git a/domains/value_domain.ml b/domains/value_domain.ml new file mode 100644 index 0000000..0d2e342 --- /dev/null +++ b/domains/value_domain.ml @@ -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 "@[Bot@]" + | E map -> begin Format.fprintf out "@[{"; + 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 diff --git a/dune b/dune new file mode 100644 index 0000000..9202d9c --- /dev/null +++ b/dune @@ -0,0 +1,4 @@ +(executable + (name analyzer) + (libraries libs frontend zarith iterator domains) + (flags (:standard -warn-error -A))) diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..1e91b03 --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 2.7) +(using menhir 2.1) diff --git a/examples/bool/assert_false.c b/examples/bool/assert_false.c new file mode 100644 index 0000000..aa29b1b --- /dev/null +++ b/examples/bool/assert_false.c @@ -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 +} \ No newline at end of file diff --git a/examples/bool/assert_false_false.c b/examples/bool/assert_false_false.c new file mode 100644 index 0000000..0bccbe5 --- /dev/null +++ b/examples/bool/assert_false_false.c @@ -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 +} \ No newline at end of file diff --git a/examples/bool/assert_not_false.c b/examples/bool/assert_not_false.c new file mode 100644 index 0000000..7df81e6 --- /dev/null +++ b/examples/bool/assert_not_false.c @@ -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); +} \ No newline at end of file diff --git a/examples/bool/assert_not_rand.c b/examples/bool/assert_not_rand.c new file mode 100644 index 0000000..5a066d6 --- /dev/null +++ b/examples/bool/assert_not_rand.c @@ -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 +} \ No newline at end of file diff --git a/examples/bool/assert_not_true.c b/examples/bool/assert_not_true.c new file mode 100644 index 0000000..3025694 --- /dev/null +++ b/examples/bool/assert_not_true.c @@ -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 +} \ No newline at end of file diff --git a/examples/bool/assert_rand.c b/examples/bool/assert_rand.c new file mode 100644 index 0000000..2304e3b --- /dev/null +++ b/examples/bool/assert_rand.c @@ -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 +} \ No newline at end of file diff --git a/examples/bool/assert_rand_false.c b/examples/bool/assert_rand_false.c new file mode 100644 index 0000000..fd13446 --- /dev/null +++ b/examples/bool/assert_rand_false.c @@ -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 +} \ No newline at end of file diff --git a/examples/bool/assert_true.c b/examples/bool/assert_true.c new file mode 100644 index 0000000..9fb9623 --- /dev/null +++ b/examples/bool/assert_true.c @@ -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); +} \ No newline at end of file diff --git a/examples/constant/constant_add.c b/examples/constant/constant_add.c new file mode 100644 index 0000000..d3b4270 --- /dev/null +++ b/examples/constant/constant_add.c @@ -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); +} diff --git a/examples/constant/constant_cmp.c b/examples/constant/constant_cmp.c new file mode 100644 index 0000000..4093c55 --- /dev/null +++ b/examples/constant/constant_cmp.c @@ -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 +} \ No newline at end of file diff --git a/examples/constant/constant_cmp_add.c b/examples/constant/constant_cmp_add.c new file mode 100644 index 0000000..ffea34a --- /dev/null +++ b/examples/constant/constant_cmp_add.c @@ -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); +} \ No newline at end of file diff --git a/examples/constant/constant_cmp_mul.c b/examples/constant/constant_cmp_mul.c new file mode 100644 index 0000000..9d41233 --- /dev/null +++ b/examples/constant/constant_cmp_mul.c @@ -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 +} diff --git a/examples/constant/constant_cmp_simple.c b/examples/constant/constant_cmp_simple.c new file mode 100644 index 0000000..ac5fdc9 --- /dev/null +++ b/examples/constant/constant_cmp_simple.c @@ -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 +} diff --git a/examples/constant/constant_div.c b/examples/constant/constant_div.c new file mode 100644 index 0000000..558e49e --- /dev/null +++ b/examples/constant/constant_div.c @@ -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); +} \ No newline at end of file diff --git a/examples/constant/constant_div_zero.c b/examples/constant/constant_div_zero.c new file mode 100644 index 0000000..b60d974 --- /dev/null +++ b/examples/constant/constant_div_zero.c @@ -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 +} diff --git a/examples/constant/constant_mul_zero.c b/examples/constant/constant_mul_zero.c new file mode 100644 index 0000000..bffcb4a --- /dev/null +++ b/examples/constant/constant_mul_zero.c @@ -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); +} \ No newline at end of file diff --git a/examples/constant/constant_rem.c b/examples/constant/constant_rem.c new file mode 100644 index 0000000..986bc07 --- /dev/null +++ b/examples/constant/constant_rem.c @@ -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); +} \ No newline at end of file diff --git a/examples/constant_loop/constant_loop_1.c b/examples/constant_loop/constant_loop_1.c new file mode 100644 index 0000000..f4c2ee2 --- /dev/null +++ b/examples/constant_loop/constant_loop_1.c @@ -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); +} diff --git a/examples/constant_loop/constant_loop_2.c b/examples/constant_loop/constant_loop_2.c new file mode 100644 index 0000000..e589034 --- /dev/null +++ b/examples/constant_loop/constant_loop_2.c @@ -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); +} \ No newline at end of file diff --git a/examples/constant_loop/constant_loop_3.c b/examples/constant_loop/constant_loop_3.c new file mode 100644 index 0000000..edb8050 --- /dev/null +++ b/examples/constant_loop/constant_loop_3.c @@ -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 +} \ No newline at end of file diff --git a/examples/interval/interval_add.c b/examples/interval/interval_add.c new file mode 100644 index 0000000..38a8d55 --- /dev/null +++ b/examples/interval/interval_add.c @@ -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 +} \ No newline at end of file diff --git a/examples/interval/interval_cmp_eq.c b/examples/interval/interval_cmp_eq.c new file mode 100644 index 0000000..c7e1178 --- /dev/null +++ b/examples/interval/interval_cmp_eq.c @@ -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 + } +} \ No newline at end of file diff --git a/examples/interval/interval_cmp_gt_add.c b/examples/interval/interval_cmp_gt_add.c new file mode 100644 index 0000000..b7a66e7 --- /dev/null +++ b/examples/interval/interval_cmp_gt_add.c @@ -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 + } +} \ No newline at end of file diff --git a/examples/interval/interval_cmp_leq.c b/examples/interval/interval_cmp_leq.c new file mode 100644 index 0000000..9f5966b --- /dev/null +++ b/examples/interval/interval_cmp_leq.c @@ -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); +} \ No newline at end of file diff --git a/examples/interval/interval_cmp_leq2.c b/examples/interval/interval_cmp_leq2.c new file mode 100644 index 0000000..1dd2dd5 --- /dev/null +++ b/examples/interval/interval_cmp_leq2.c @@ -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 + } +} \ No newline at end of file diff --git a/examples/interval/interval_cmp_simple.c b/examples/interval/interval_cmp_simple.c new file mode 100644 index 0000000..de966e1 --- /dev/null +++ b/examples/interval/interval_cmp_simple.c @@ -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 +} \ No newline at end of file diff --git a/examples/interval/interval_goto.c b/examples/interval/interval_goto.c new file mode 100644 index 0000000..102c03b --- /dev/null +++ b/examples/interval/interval_goto.c @@ -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); +} \ No newline at end of file diff --git a/examples/interval/interval_mul.c b/examples/interval/interval_mul.c new file mode 100644 index 0000000..5a377fc --- /dev/null +++ b/examples/interval/interval_mul.c @@ -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 +} \ No newline at end of file diff --git a/examples/interval_loop/interval_loop.c b/examples/interval_loop/interval_loop.c new file mode 100644 index 0000000..6861eca --- /dev/null +++ b/examples/interval_loop/interval_loop.c @@ -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); +} \ No newline at end of file diff --git a/frontend/abstract_syntax_tree.ml b/frontend/abstract_syntax_tree.ml new file mode 100644 index 0000000..ac34388 --- /dev/null +++ b/frontend/abstract_syntax_tree.ml @@ -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 diff --git a/frontend/add_assert_div.ml b/frontend/add_assert_div.ml new file mode 100644 index 0000000..528a30b --- /dev/null +++ b/frontend/add_assert_div.ml @@ -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 diff --git a/frontend/cfg.ml b/frontend/cfg.ml new file mode 100644 index 0000000..0718571 --- /dev/null +++ b/frontend/cfg.ml @@ -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 *) + } + diff --git a/frontend/cfg_printer.ml b/frontend/cfg_printer.ml new file mode 100644 index 0000000..07957d8 --- /dev/null +++ b/frontend/cfg_printer.ml @@ -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 + diff --git a/frontend/dune b/frontend/dune new file mode 100644 index 0000000..26b2071 --- /dev/null +++ b/frontend/dune @@ -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)) diff --git a/frontend/errors.ml b/frontend/errors.ml new file mode 100644 index 0000000..b32c81f --- /dev/null +++ b/frontend/errors.ml @@ -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 diff --git a/frontend/file_parser.ml b/frontend/file_parser.ml new file mode 100644 index 0000000..bda9099 --- /dev/null +++ b/frontend/file_parser.ml @@ -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 diff --git a/frontend/file_parser.mli b/frontend/file_parser.mli new file mode 100644 index 0000000..c093e15 --- /dev/null +++ b/frontend/file_parser.mli @@ -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. *) + diff --git a/frontend/lexer.mll b/frontend/lexer.mll new file mode 100644 index 0000000..15bf95c --- /dev/null +++ b/frontend/lexer.mll @@ -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 } diff --git a/frontend/options.ml b/frontend/options.ml new file mode 100644 index 0000000..9c21226 --- /dev/null +++ b/frontend/options.ml @@ -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 () + diff --git a/frontend/parser.messages b/frontend/parser.messages new file mode 100644 index 0000000..dad4e24 --- /dev/null +++ b/frontend/parser.messages @@ -0,0 +1,1523 @@ +file: TOK_INT TOK_SEMICOLON TOK_int +## +## Ends in an error in state: 170. +## +## list(toplevel) -> toplevel . list(toplevel) [ TOK_EOF ] +## +## The known suffix of the stack is as follows: +## toplevel +## + +Expected declaration. + +file: TOK_INT TOK_id TOK_COMMA TOK_id TOK_int +## +## Ends in an error in state: 135. +## +## init_declarator -> TOK_id . [ TOK_SEMICOLON TOK_COMMA ] +## init_declarator -> TOK_id . TOK_EQUAL int_expr [ TOK_SEMICOLON TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id +## + +Expected ',', ';' or '='. + +file: TOK_INT TOK_id TOK_COMMA TOK_int +## +## Ends in an error in state: 142. +## +## separated_nonempty_list(TOK_COMMA,init_declarator) -> init_declarator TOK_COMMA . separated_nonempty_list(TOK_COMMA,init_declarator) [ TOK_SEMICOLON ] +## +## The known suffix of the stack is as follows: +## init_declarator TOK_COMMA +## + +Expected identifier. + +file: TOK_INT TOK_id TOK_EQUAL TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 32. +## +## int_expr -> TOK_LPAREN . int_expr TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_LPAREN +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_LPAREN TOK_int TOK_int +## +## Ends in an error in state: 33. +## +## int_expr -> TOK_LPAREN int_expr . TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## +## The known suffix of the stack is as follows: +## TOK_LPAREN int_expr +## + +Expected operator. + +file: TOK_INT TOK_id TOK_EQUAL TOK_MINUS TOK_WHILE +## +## Ends in an error in state: 31. +## +## int_expr -> TOK_MINUS . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_MINUS +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_MINUS TOK_int TOK_int +## +## Ends in an error in state: 45. +## +## int_expr -> TOK_MINUS int_expr . [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_MINUS int_expr +## + +Expected operator. + +file: TOK_INT TOK_id TOK_EQUAL TOK_PLUS TOK_WHILE +## +## Ends in an error in state: 30. +## +## int_expr -> TOK_PLUS . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_PLUS +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_PLUS TOK_int TOK_int +## +## Ends in an error in state: 46. +## +## int_expr -> TOK_PLUS int_expr . [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_PLUS int_expr +## + +Expected operator. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_LPAREN TOK_MINUS TOK_id +## +## Ends in an error in state: 24. +## +## sign_int_literal -> TOK_MINUS . TOK_int [ TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_MINUS +## + +Expected integer. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_LPAREN TOK_PLUS TOK_id +## +## Ends in an error in state: 22. +## +## sign_int_literal -> TOK_PLUS . TOK_int [ TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_PLUS +## + +Expected integer. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_LPAREN TOK_id +## +## Ends in an error in state: 20. +## +## int_expr -> TOK_RAND TOK_LPAREN . sign_int_literal TOK_COMMA sign_int_literal TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_RAND TOK_LPAREN +## + +Expected integer. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_LPAREN TOK_int TOK_COMMA TOK_id +## +## Ends in an error in state: 27. +## +## int_expr -> TOK_RAND TOK_LPAREN sign_int_literal TOK_COMMA . sign_int_literal TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_RAND TOK_LPAREN sign_int_literal TOK_COMMA +## + +Expected integer. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_LPAREN TOK_int TOK_COMMA TOK_int TOK_int +## +## Ends in an error in state: 28. +## +## int_expr -> TOK_RAND TOK_LPAREN sign_int_literal TOK_COMMA sign_int_literal . TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_RAND TOK_LPAREN sign_int_literal TOK_COMMA sign_int_literal +## + +Expected ')'. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_LPAREN TOK_int TOK_int +## +## Ends in an error in state: 26. +## +## int_expr -> TOK_RAND TOK_LPAREN sign_int_literal . TOK_COMMA sign_int_literal TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_RAND TOK_LPAREN sign_int_literal +## + +Expected ','. + +file: TOK_INT TOK_id TOK_EQUAL TOK_RAND TOK_int +## +## Ends in an error in state: 19. +## +## int_expr -> TOK_RAND . TOK_LPAREN sign_int_literal TOK_COMMA sign_int_literal TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_RAND +## + +Expected '('. + +file: TOK_INT TOK_id TOK_EQUAL TOK_WHILE +## +## Ends in an error in state: 136. +## +## init_declarator -> TOK_id TOK_EQUAL . int_expr [ TOK_SEMICOLON TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_EQUAL +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_id TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 18. +## +## int_expr -> TOK_id TOK_LPAREN . int_expr_list TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_LPAREN +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_id TOK_LPAREN TOK_int TOK_COMMA TOK_WHILE +## +## Ends in an error in state: 52. +## +## separated_nonempty_list(TOK_COMMA,ext(int_expr)) -> int_expr TOK_COMMA . separated_nonempty_list(TOK_COMMA,ext(int_expr)) [ TOK_RPAREN ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_COMMA +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_id TOK_LPAREN TOK_int TOK_int +## +## Ends in an error in state: 51. +## +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## separated_nonempty_list(TOK_COMMA,ext(int_expr)) -> int_expr . [ TOK_RPAREN ] +## separated_nonempty_list(TOK_COMMA,ext(int_expr)) -> int_expr . TOK_COMMA separated_nonempty_list(TOK_COMMA,ext(int_expr)) [ TOK_RPAREN ] +## +## The known suffix of the stack is as follows: +## int_expr +## + +Expected ','. + +file: TOK_INT TOK_id TOK_EQUAL TOK_id TOK_int +## +## Ends in an error in state: 17. +## +## int_expr -> TOK_id . [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> TOK_id . TOK_LPAREN int_expr_list TOK_RPAREN [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_id +## + +Expected function call or operator. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_DIVIDE TOK_WHILE +## +## Ends in an error in state: 41. +## +## int_expr -> int_expr TOK_DIVIDE . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_DIVIDE +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_MINUS TOK_WHILE +## +## Ends in an error in state: 43. +## +## int_expr -> int_expr TOK_MINUS . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_MINUS +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_MINUS TOK_int TOK_int +## +## Ends in an error in state: 44. +## +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr TOK_MINUS int_expr . [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_MINUS int_expr +## + +Expected operator. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_PERCENT TOK_WHILE +## +## Ends in an error in state: 39. +## +## int_expr -> int_expr TOK_PERCENT . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_PERCENT +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_PLUS TOK_WHILE +## +## Ends in an error in state: 37. +## +## int_expr -> int_expr TOK_PLUS . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_PLUS +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_PLUS TOK_int TOK_int +## +## Ends in an error in state: 38. +## +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr TOK_PLUS int_expr . [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_PLUS int_expr +## + +Expected operator. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_STAR TOK_WHILE +## +## Ends in an error in state: 34. +## +## int_expr -> int_expr TOK_STAR . int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE TOK_COMMA TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_STAR +## + +Expected expression. + +file: TOK_INT TOK_id TOK_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 137. +## +## init_declarator -> TOK_id TOK_EQUAL int_expr . [ TOK_SEMICOLON TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_EQUAL int_expr +## + +Expected operator. + +file: TOK_INT TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_int +## +## Ends in an error in state: 167. +## +## fun_decl -> typ TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY . list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## typ TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY +## + +Expected statement. + +file: TOK_INT TOK_id TOK_LPAREN TOK_RPAREN TOK_int +## +## Ends in an error in state: 166. +## +## fun_decl -> typ TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN . TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## typ TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN +## + +Expected statement. + +file: TOK_INT TOK_id TOK_LPAREN TOK_int +## +## Ends in an error in state: 164. +## +## fun_decl -> typ TOK_id TOK_LPAREN . loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## typ TOK_id TOK_LPAREN +## + +Expected parameter list. + +file: TOK_INT TOK_id TOK_int +## +## Ends in an error in state: 163. +## +## fun_decl -> typ TOK_id . TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## init_declarator -> TOK_id . [ TOK_SEMICOLON TOK_COMMA ] +## init_declarator -> TOK_id . TOK_EQUAL int_expr [ TOK_SEMICOLON TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## typ TOK_id +## + +Expected '(', ';' or '='. + +file: TOK_INT TOK_int +## +## Ends in an error in state: 162. +## +## fun_decl -> typ . TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## var_decl -> typ . loption(separated_nonempty_list(TOK_COMMA,init_declarator)) TOK_SEMICOLON [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## typ +## + +Expected identifier. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_INT TOK_id TOK_COMMA TOK_int +## +## Ends in an error in state: 9. +## +## separated_nonempty_list(TOK_COMMA,param_decl) -> param_decl TOK_COMMA . separated_nonempty_list(TOK_COMMA,param_decl) [ TOK_RPAREN ] +## +## The known suffix of the stack is as follows: +## param_decl TOK_COMMA +## + +Expected identifier. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_INT TOK_id TOK_int +## +## Ends in an error in state: 8. +## +## separated_nonempty_list(TOK_COMMA,param_decl) -> param_decl . [ TOK_RPAREN ] +## separated_nonempty_list(TOK_COMMA,param_decl) -> param_decl . TOK_COMMA separated_nonempty_list(TOK_COMMA,param_decl) [ TOK_RPAREN ] +## +## The known suffix of the stack is as follows: +## param_decl +## + +Expected initializer, ';' or ','. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_INT TOK_int +## +## Ends in an error in state: 5. +## +## param_decl -> typ . TOK_id [ TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## typ +## + +Expected identifier. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_ASSERT TOK_LPAREN TOK_TRUE TOK_RPAREN TOK_int +## +## Ends in an error in state: 131. +## +## stat -> TOK_ASSERT TOK_LPAREN bool_expr TOK_RPAREN . TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_ASSERT TOK_LPAREN bool_expr TOK_RPAREN +## + +Expected ';'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_ASSERT TOK_LPAREN TOK_TRUE TOK_int +## +## Ends in an error in state: 130. +## +## bool_expr -> bool_expr . TOK_AND_AND bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_BAR_BAR bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## stat -> TOK_ASSERT TOK_LPAREN bool_expr . TOK_RPAREN TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_ASSERT TOK_LPAREN bool_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_ASSERT TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 129. +## +## stat -> TOK_ASSERT TOK_LPAREN . bool_expr TOK_RPAREN TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_ASSERT TOK_LPAREN +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_ASSERT TOK_int +## +## Ends in an error in state: 128. +## +## stat -> TOK_ASSERT . TOK_LPAREN bool_expr TOK_RPAREN TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_ASSERT +## + +Expected '('. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_BREAK TOK_int +## +## Ends in an error in state: 126. +## +## stat -> TOK_BREAK . TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_BREAK +## + +Expected ';'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_SEMICOLON TOK_SEMICOLON TOK_RPAREN TOK_int +## +## Ends in an error in state: 125. +## +## stat -> TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list TOK_RPAREN . stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list TOK_RPAREN +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_SEMICOLON TOK_SEMICOLON TOK_id TOK_MINUS_MINUS TOK_SEMICOLON +## +## Ends in an error in state: 124. +## +## stat -> TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list . TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 147, spurious reduction of production separated_nonempty_list(TOK_COMMA,ext(assign)) -> assign +## In state 118, spurious reduction of production loption(separated_nonempty_list(TOK_COMMA,ext(assign))) -> separated_nonempty_list(TOK_COMMA,ext(assign)) +## In state 119, spurious reduction of production assign_list -> loption(separated_nonempty_list(TOK_COMMA,ext(assign))) +## + +Expected ')'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_SEMICOLON TOK_SEMICOLON TOK_int +## +## Ends in an error in state: 123. +## +## stat -> TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON . assign_list TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON +## + +Expected assignment. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_SEMICOLON TOK_TRUE TOK_int +## +## Ends in an error in state: 150. +## +## bool_expr -> bool_expr . TOK_AND_AND bool_expr [ TOK_SEMICOLON TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_BAR_BAR bool_expr [ TOK_SEMICOLON TOK_BAR_BAR TOK_AND_AND ] +## option(ext(bool_expr)) -> bool_expr . [ TOK_SEMICOLON ] +## +## The known suffix of the stack is as follows: +## bool_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_SEMICOLON TOK_WHILE +## +## Ends in an error in state: 121. +## +## stat -> TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON . option(ext(bool_expr)) TOK_SEMICOLON assign_list TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR TOK_LPAREN assign_list TOK_SEMICOLON +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_id TOK_MINUS_MINUS TOK_COMMA TOK_int +## +## Ends in an error in state: 148. +## +## separated_nonempty_list(TOK_COMMA,ext(assign)) -> assign TOK_COMMA . separated_nonempty_list(TOK_COMMA,ext(assign)) [ TOK_SEMICOLON TOK_RPAREN ] +## +## The known suffix of the stack is as follows: +## assign TOK_COMMA +## + +Expected assignment. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_id TOK_MINUS_MINUS TOK_RPAREN +## +## Ends in an error in state: 120. +## +## stat -> TOK_FOR TOK_LPAREN assign_list . TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR TOK_LPAREN assign_list +## +## WARNING: This example involves spurious reductions. +## This implies that, although the LR(1) items shown above provide an +## accurate view of the past (what has been recognized so far), they +## may provide an INCOMPLETE view of the future (what was expected next). +## In state 147, spurious reduction of production separated_nonempty_list(TOK_COMMA,ext(assign)) -> assign +## In state 118, spurious reduction of production loption(separated_nonempty_list(TOK_COMMA,ext(assign))) -> separated_nonempty_list(TOK_COMMA,ext(assign)) +## In state 119, spurious reduction of production assign_list -> loption(separated_nonempty_list(TOK_COMMA,ext(assign))) +## + +Expected ';'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_id TOK_MINUS_MINUS TOK_int +## +## Ends in an error in state: 147. +## +## separated_nonempty_list(TOK_COMMA,ext(assign)) -> assign . [ TOK_SEMICOLON TOK_RPAREN ] +## separated_nonempty_list(TOK_COMMA,ext(assign)) -> assign . TOK_COMMA separated_nonempty_list(TOK_COMMA,ext(assign)) [ TOK_SEMICOLON TOK_RPAREN ] +## +## The known suffix of the stack is as follows: +## assign +## + +Expected ',' or ';'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_id TOK_int +## +## Ends in an error in state: 117. +## +## assign -> TOK_id . TOK_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_STAR_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_DIVIDE_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_PERCENT_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_PLUS_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_MINUS_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_PLUS_PLUS [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## assign -> TOK_id . TOK_MINUS_MINUS [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_LPAREN TOK_int +## +## Ends in an error in state: 116. +## +## stat -> TOK_FOR TOK_LPAREN . assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR TOK_LPAREN +## + +Expected assignment. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_FOR TOK_int +## +## Ends in an error in state: 115. +## +## stat -> TOK_FOR . TOK_LPAREN assign_list TOK_SEMICOLON option(ext(bool_expr)) TOK_SEMICOLON assign_list TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_FOR +## + +Expected '('. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_GOTO TOK_id TOK_int +## +## Ends in an error in state: 113. +## +## stat -> TOK_GOTO TOK_id . TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_GOTO TOK_id +## + +Expected ';'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_GOTO TOK_int +## +## Ends in an error in state: 112. +## +## stat -> TOK_GOTO . TOK_id TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_GOTO +## + +Expected label. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_IF TOK_LPAREN TOK_TRUE TOK_RPAREN TOK_SEMICOLON TOK_ELSE TOK_int +## +## Ends in an error in state: 152. +## +## stat -> TOK_IF TOK_LPAREN bool_expr TOK_RPAREN stat TOK_ELSE . stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_IF TOK_LPAREN bool_expr TOK_RPAREN stat TOK_ELSE +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_IF TOK_LPAREN TOK_TRUE TOK_RPAREN TOK_SEMICOLON TOK_int +## +## Ends in an error in state: 151. +## +## stat -> TOK_IF TOK_LPAREN bool_expr TOK_RPAREN stat . [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## stat -> TOK_IF TOK_LPAREN bool_expr TOK_RPAREN stat . TOK_ELSE stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_IF TOK_LPAREN bool_expr TOK_RPAREN stat +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_IF TOK_LPAREN TOK_TRUE TOK_RPAREN TOK_int +## +## Ends in an error in state: 111. +## +## stat -> TOK_IF TOK_LPAREN bool_expr TOK_RPAREN . stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## stat -> TOK_IF TOK_LPAREN bool_expr TOK_RPAREN . stat TOK_ELSE stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_IF TOK_LPAREN bool_expr TOK_RPAREN +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_IF TOK_LPAREN TOK_TRUE TOK_int +## +## Ends in an error in state: 110. +## +## bool_expr -> bool_expr . TOK_AND_AND bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_BAR_BAR bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## stat -> TOK_IF TOK_LPAREN bool_expr . TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## stat -> TOK_IF TOK_LPAREN bool_expr . TOK_RPAREN stat TOK_ELSE stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_IF TOK_LPAREN bool_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_IF TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 109. +## +## stat -> TOK_IF TOK_LPAREN . bool_expr TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## stat -> TOK_IF TOK_LPAREN . bool_expr TOK_RPAREN stat TOK_ELSE stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_IF TOK_LPAREN +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_IF TOK_int +## +## Ends in an error in state: 108. +## +## stat -> TOK_IF . TOK_LPAREN bool_expr TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## stat -> TOK_IF . TOK_LPAREN bool_expr TOK_RPAREN stat TOK_ELSE stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_IF +## + +Expected '('. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_INT TOK_int +## +## Ends in an error in state: 134. +## +## var_decl -> typ . loption(separated_nonempty_list(TOK_COMMA,init_declarator)) TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## typ +## + +Expected identifier. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_LCURLY TOK_int +## +## Ends in an error in state: 107. +## +## stat -> TOK_LCURLY . list(ext(stat)) TOK_RCURLY [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_LCURLY +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_RETURN TOK_WHILE +## +## Ends in an error in state: 103. +## +## stat -> TOK_RETURN . option(ext(int_expr)) TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_RETURN +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_RETURN TOK_int TOK_int +## +## Ends in an error in state: 106. +## +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE ] +## option(ext(int_expr)) -> int_expr . [ TOK_SEMICOLON ] +## +## The known suffix of the stack is as follows: +## int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_SEMICOLON TOK_int +## +## Ends in an error in state: 154. +## +## list(ext(stat)) -> stat . list(ext(stat)) [ TOK_RCURLY ] +## +## The known suffix of the stack is as follows: +## stat +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_EXCLAIM TOK_WHILE +## +## Ends in an error in state: 77. +## +## bool_expr -> TOK_EXCLAIM . bool_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_EXCLAIM +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_LPAREN TOK_TRUE TOK_int +## +## Ends in an error in state: 94. +## +## bool_expr -> TOK_LPAREN bool_expr . TOK_RPAREN [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_AND_AND bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_BAR_BAR bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## TOK_LPAREN bool_expr +## + +Expected operator or ')'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 75. +## +## bool_expr -> TOK_LPAREN . bool_expr TOK_RPAREN [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> TOK_LPAREN . int_expr TOK_RPAREN [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## +## The known suffix of the stack is as follows: +## TOK_LPAREN +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_LPAREN TOK_int TOK_int +## +## Ends in an error in state: 93. +## +## bool_expr -> int_expr . TOK_LESS int_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_GREATER int_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_LESS_EQUAL int_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_GREATER_EQUAL int_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_EQUAL_EQUAL int_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_NOT_EQUAL int_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> TOK_LPAREN int_expr . TOK_RPAREN [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## +## The known suffix of the stack is as follows: +## TOK_LPAREN int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_TRUE TOK_AND_AND TOK_WHILE +## +## Ends in an error in state: 98. +## +## bool_expr -> bool_expr TOK_AND_AND . bool_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## bool_expr TOK_AND_AND +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_TRUE TOK_BAR_BAR TOK_TRUE TOK_int +## +## Ends in an error in state: 97. +## +## bool_expr -> bool_expr . TOK_AND_AND bool_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_BAR_BAR bool_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr TOK_BAR_BAR bool_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## bool_expr TOK_BAR_BAR bool_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_TRUE TOK_BAR_BAR TOK_WHILE +## +## Ends in an error in state: 96. +## +## bool_expr -> bool_expr TOK_BAR_BAR . bool_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## bool_expr TOK_BAR_BAR +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_TRUE TOK_RPAREN TOK_int +## +## Ends in an error in state: 101. +## +## stat -> TOK_WHILE TOK_LPAREN bool_expr TOK_RPAREN . stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_WHILE TOK_LPAREN bool_expr TOK_RPAREN +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_TRUE TOK_int +## +## Ends in an error in state: 100. +## +## bool_expr -> bool_expr . TOK_AND_AND bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> bool_expr . TOK_BAR_BAR bool_expr [ TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## stat -> TOK_WHILE TOK_LPAREN bool_expr . TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_WHILE TOK_LPAREN bool_expr +## + +Expected expression or ')'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 73. +## +## stat -> TOK_WHILE TOK_LPAREN . bool_expr TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_WHILE TOK_LPAREN +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_EQUAL_EQUAL TOK_WHILE +## +## Ends in an error in state: 90. +## +## bool_expr -> int_expr TOK_EQUAL_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_EQUAL_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_EQUAL_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 91. +## +## bool_expr -> int_expr TOK_EQUAL_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_EQUAL_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_GREATER TOK_WHILE +## +## Ends in an error in state: 88. +## +## bool_expr -> int_expr TOK_GREATER . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_GREATER +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_GREATER TOK_int TOK_int +## +## Ends in an error in state: 89. +## +## bool_expr -> int_expr TOK_GREATER int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_GREATER int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_GREATER_EQUAL TOK_WHILE +## +## Ends in an error in state: 86. +## +## bool_expr -> int_expr TOK_GREATER_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_GREATER_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_GREATER_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 87. +## +## bool_expr -> int_expr TOK_GREATER_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_GREATER_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_LESS TOK_WHILE +## +## Ends in an error in state: 84. +## +## bool_expr -> int_expr TOK_LESS . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_LESS +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_LESS TOK_int TOK_int +## +## Ends in an error in state: 85. +## +## bool_expr -> int_expr TOK_LESS int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_LESS int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_LESS_EQUAL TOK_WHILE +## +## Ends in an error in state: 82. +## +## bool_expr -> int_expr TOK_LESS_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_LESS_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_LESS_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 83. +## +## bool_expr -> int_expr TOK_LESS_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_LESS_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_NOT_EQUAL TOK_WHILE +## +## Ends in an error in state: 80. +## +## bool_expr -> int_expr TOK_NOT_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_NOT_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_NOT_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 81. +## +## bool_expr -> int_expr TOK_NOT_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_BAR_BAR TOK_AND_AND ] +## +## The known suffix of the stack is as follows: +## int_expr TOK_NOT_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_LPAREN TOK_int TOK_int +## +## Ends in an error in state: 79. +## +## bool_expr -> int_expr . TOK_LESS int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_GREATER int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_LESS_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_GREATER_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_EQUAL_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## bool_expr -> int_expr . TOK_NOT_EQUAL int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_BAR_BAR TOK_AND_AND ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_PLUS TOK_PERCENT TOK_NOT_EQUAL TOK_MINUS TOK_LESS_EQUAL TOK_LESS TOK_GREATER_EQUAL TOK_GREATER TOK_EQUAL_EQUAL TOK_DIVIDE ] +## +## The known suffix of the stack is as follows: +## int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_WHILE TOK_int +## +## Ends in an error in state: 72. +## +## stat -> TOK_WHILE . TOK_LPAREN bool_expr TOK_RPAREN stat [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_WHILE +## + +Expected '('. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_DIVIDE_EQUAL TOK_WHILE +## +## Ends in an error in state: 69. +## +## assign -> TOK_id TOK_DIVIDE_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_DIVIDE_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_DIVIDE_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 70. +## +## assign -> TOK_id TOK_DIVIDE_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_DIVIDE_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_EQUAL TOK_WHILE +## +## Ends in an error in state: 67. +## +## assign -> TOK_id TOK_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 68. +## +## assign -> TOK_id TOK_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_LPAREN TOK_RPAREN TOK_int +## +## Ends in an error in state: 65. +## +## stat -> TOK_id TOK_LPAREN int_expr_list TOK_RPAREN . TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_LPAREN int_expr_list TOK_RPAREN +## + +Expected ';'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_LPAREN TOK_WHILE +## +## Ends in an error in state: 63. +## +## stat -> TOK_id TOK_LPAREN . int_expr_list TOK_RPAREN TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_LPAREN +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_MINUS_EQUAL TOK_WHILE +## +## Ends in an error in state: 61. +## +## assign -> TOK_id TOK_MINUS_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_MINUS_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_MINUS_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 62. +## +## assign -> TOK_id TOK_MINUS_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_MINUS_EQUAL int_expr +## + +Expected expression + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_MINUS_MINUS TOK_int +## +## Ends in an error in state: 145. +## +## stat -> assign . TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## assign +## + +Expected ';' + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_PERCENT_EQUAL TOK_WHILE +## +## Ends in an error in state: 58. +## +## assign -> TOK_id TOK_PERCENT_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_PERCENT_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_PERCENT_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 59. +## +## assign -> TOK_id TOK_PERCENT_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_PERCENT_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_PLUS_EQUAL TOK_WHILE +## +## Ends in an error in state: 56. +## +## assign -> TOK_id TOK_PLUS_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_PLUS_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_PLUS_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 57. +## +## assign -> TOK_id TOK_PLUS_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_PLUS_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_STAR_EQUAL TOK_WHILE +## +## Ends in an error in state: 15. +## +## assign -> TOK_id TOK_STAR_EQUAL . int_expr [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_STAR_EQUAL +## + +Expected expression. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_STAR_EQUAL TOK_int TOK_int +## +## Ends in an error in state: 54. +## +## assign -> TOK_id TOK_STAR_EQUAL int_expr . [ TOK_SEMICOLON TOK_RPAREN TOK_COMMA ] +## int_expr -> int_expr . TOK_STAR int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_DIVIDE int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PERCENT int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_PLUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## int_expr -> int_expr . TOK_MINUS int_expr [ TOK_STAR TOK_SEMICOLON TOK_RPAREN TOK_PLUS TOK_PERCENT TOK_MINUS TOK_DIVIDE TOK_COMMA ] +## +## The known suffix of the stack is as follows: +## TOK_id TOK_STAR_EQUAL int_expr +## + +Expected operator. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_id TOK_int +## +## Ends in an error in state: 14. +## +## assign -> TOK_id . TOK_EQUAL int_expr [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_STAR_EQUAL int_expr [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_DIVIDE_EQUAL int_expr [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_PERCENT_EQUAL int_expr [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_PLUS_EQUAL int_expr [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_MINUS_EQUAL int_expr [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_PLUS_PLUS [ TOK_SEMICOLON ] +## assign -> TOK_id . TOK_MINUS_MINUS [ TOK_SEMICOLON ] +## stat -> TOK_id . TOK_LPAREN int_expr_list TOK_RPAREN TOK_SEMICOLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## stat -> TOK_id . TOK_COLON [ TOK_id TOK_WHILE TOK_SEMICOLON TOK_RETURN TOK_RCURLY TOK_LCURLY TOK_INT TOK_IF TOK_GOTO TOK_FOR TOK_ELSE TOK_BREAK TOK_ASSERT ] +## +## The known suffix of the stack is as follows: +## TOK_id +## + +Expected assignment operator, function call or label definition. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_LCURLY TOK_int +## +## Ends in an error in state: 13. +## +## fun_decl -> TOK_VOID TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY . list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## TOK_VOID TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY +## + +Expected statement. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_RPAREN TOK_int +## +## Ends in an error in state: 12. +## +## fun_decl -> TOK_VOID TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN . TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## TOK_VOID TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN +## + +Expected '{'. + +file: TOK_VOID TOK_id TOK_LPAREN TOK_int +## +## Ends in an error in state: 3. +## +## fun_decl -> TOK_VOID TOK_id TOK_LPAREN . loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## TOK_VOID TOK_id TOK_LPAREN +## + +Expected parameter or ')'. + +file: TOK_VOID TOK_id TOK_int +## +## Ends in an error in state: 2. +## +## fun_decl -> TOK_VOID TOK_id . TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## TOK_VOID TOK_id +## + +Expected '('. + +file: TOK_VOID TOK_int +## +## Ends in an error in state: 1. +## +## fun_decl -> TOK_VOID . TOK_id TOK_LPAREN loption(separated_nonempty_list(TOK_COMMA,param_decl)) TOK_RPAREN TOK_LCURLY list(ext(stat)) TOK_RCURLY [ TOK_VOID TOK_INT TOK_EOF ] +## +## The known suffix of the stack is as follows: +## TOK_VOID +## + +Expected function name. + +file: TOK_int +## +## Ends in an error in state: 0. +## +## file' -> . file [ # ] +## +## The known suffix of the stack is as follows: +## +## + +Expected declaration. + diff --git a/frontend/parser.mly b/frontend/parser.mly new file mode 100644 index 0000000..8dc0669 --- /dev/null +++ b/frontend/parser.mly @@ -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 TOK_id +%token 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 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) } + + +%% diff --git a/frontend/tree_to_cfg.ml b/frontend/tree_to_cfg.ml new file mode 100644 index 0000000..e3d56f6 --- /dev/null +++ b/frontend/tree_to_cfg.ml @@ -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; + } + diff --git a/iterator/dune b/iterator/dune new file mode 100644 index 0000000..a26a9fc --- /dev/null +++ b/iterator/dune @@ -0,0 +1,5 @@ +(library + (name iterator) + (wrapped false) + (libraries libs zarith menhirLib apron frontend domains)) + diff --git a/iterator/iterator.ml b/iterator/iterator.ml new file mode 100644 index 0000000..9f9b7ec --- /dev/null +++ b/iterator/iterator.ml @@ -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 "@[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 "@[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 "@["; + 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 "@[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:@ @["; + List.iter iter_node cfg.cfg_nodes; + Format.printf "@]"*) +*) diff --git a/libs/dune b/libs/dune new file mode 100644 index 0000000..6e57202 --- /dev/null +++ b/libs/dune @@ -0,0 +1,4 @@ +(library + (name libs) + (wrapped false) + (flags (:standard -warn-error -A))) diff --git a/libs/mapext.ml b/libs/mapext.ml new file mode 100644 index 0000000..3c2b490 --- /dev/null +++ b/libs/mapext.ml @@ -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) diff --git a/libs/mapext.mli b/libs/mapext.mli new file mode 100644 index 0000000..66c9622 --- /dev/null +++ b/libs/mapext.mli @@ -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. *) diff --git a/scripts/style.css b/scripts/style.css new file mode 100644 index 0000000..e317b08 --- /dev/null +++ b/scripts/style.css @@ -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; +} \ No newline at end of file diff --git a/scripts/test.sh b/scripts/test.sh new file mode 100755 index 0000000..89b8a50 --- /dev/null +++ b/scripts/test.sh @@ -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 "

${filename}

" >> $file_html + echo "
" >> $file_html + cat $file >> $file_html + echo "
" >> $file_html + file_svg=$(basename ${file})".svg" + echo "\"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 "

Expected: ${expected}

" >> $file_html + echo "

Failures: ${failures}

" >> $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 "

${line_nb}${line}

" >> $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 "

${line}

" >> $file_html + fi + done + echo "

LOG

" >> $file_html + echo "
" >> $file_html
+  cat $log >> $file_html
+  echo "
" >> $file_html + if [ "$need_new_line" = false ] + then + echo -e "" + fi + echo -n "" >> $index_html + echo -n "${sound_loc}, " >> $index_html + echo -n "${compl_loc}" >> $index_html + echo "" >> $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 "${bench_name} ${options}" >> $index_html + for file in $(find "${folder}" -iname "*.c" | sort) + do + filename=$(basename $file) + create_file $file + echo "
${filename}
" >> $index_html + echo "" >> $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 "

${analyzer} ${options}

" >> $file_html + timeout $max_time $analyzer $options $file > $log 2>&1 + out=$? + if [[ $out -eq 127 ]] + then + timeout=$((timeout+1)) + echo "TO" >> $index_html + echo "TO" >> $file_html + echo -e "\n ${BOLD}${RED}TO ${RESET}\n" + echo "

LOG

" >> $file_html + echo "
" >> $file_html
+      cat $log >> $file_html
+      echo "
" >> $file_html + elif [[ $out -ne 0 ]] + then + failure=$((failure+1)) + echo "FAIL" >> $index_html + echo "FAIL" >> $file_html + echo -e "\n ${BOLD}${RED}FAILED ($out) ${RESET}\n" + echo "

LOG

" >> $file_html + echo "
" >> $file_html
+      cat $log >> $file_html
+      echo "
" >> $file_html + else + treat_file $file $log $expected_folder + fi + echo "" >> $index_html + echo "" >> $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 "

Overview

" >> $index_html +echo "" >> $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 "
" >> $index_html +echo "" >> $index_html +echo "" >> $index_html +print_end