From 9714afeb275360110161c870b50627128fda75a0 Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Wed, 14 May 2014 17:23:57 +0200 Subject: Many things work! --- Makefile | 1 + abstract/constant_domain.ml | 25 +++++++-- abstract/environment_domain.ml | 4 +- abstract/interpret.ml | 124 +++++++++++++++++++++++++++++++++-------- abstract/intervals_domain.ml | 122 ++++++++++++++++++++++++++++++++++++++++ abstract/nonrelational.ml | 38 ++++++++----- main.ml | 44 ++++++++++++--- tests/test.sh | 26 +++++++++ 8 files changed, 331 insertions(+), 53 deletions(-) create mode 100644 abstract/intervals_domain.ml create mode 100755 tests/test.sh diff --git a/Makefile b/Makefile index 51d9995..00cda6d 100644 --- a/Makefile +++ b/Makefile @@ -5,6 +5,7 @@ SRCDIRS=libs,frontend,abstract SRC= main.ml \ abstract/constant_domain.ml \ + abstract/intervals_domain.ml \ abstract/environment_domain.ml \ abstract/interpret.ml \ abstract/nonrelational.ml \ diff --git a/abstract/constant_domain.ml b/abstract/constant_domain.ml index d142228..44a13fc 100644 --- a/abstract/constant_domain.ml +++ b/abstract/constant_domain.ml @@ -9,7 +9,7 @@ module Constants : VALUE_DOMAIN = struct let top = Top let bottom = Bot let const i = Int i - let rand i j = if i <> j then Top else Int i + let rand i j = if i > j then Bot else if i <> j then Top else Int i let subset a b = match a, b with | _, Top -> true @@ -27,7 +27,7 @@ module Constants : VALUE_DOMAIN = struct | Int a, Int b when a = b -> Int a | _ -> Bot - let widen = meet (* pas besoin d'accélerer la convergence au-delà *) + let widen = join (* pas besoin d'accélerer la convergence au-delà *) let neg = function | Int a -> Int (Z.neg a) @@ -39,13 +39,26 @@ module Constants : VALUE_DOMAIN = struct | _ -> Top let add = b_aux Z.add let sub = b_aux Z.sub - let mul = b_aux Z.mul - let div = b_aux Z.div - let rem = b_aux Z.rem + let mul a b = match a, b with + | Int x, Int y -> Int (Z.mul x y) + | Bot, _ | _, Bot -> Bot + | Int x, _ when x = Z.zero -> Int Z.zero + | _, Int x when x = Z.zero -> Int (Z.zero) + | _ -> Top + let div a b = match a, b with + | Int x, Int y -> Int (Z.div x y) + | Bot, _ | _, Bot -> Bot + | Int x, _ when x = Z.zero -> Int Z.zero + | _ -> Top + let rem a b = match a, b with + | Int x, Int y -> Int (Z.rem x y) + | Bot, _ | _, Bot -> Bot + | Int x, _ when x = Z.zero -> Int Z.zero + | _ -> Top let leq a b = match a, b with - | Int a, Int b when Z.leq a b -> + | Int a, Int b -> if Z.leq a b then Int a, Int b else Bot, Bot diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml index 254f755..05473aa 100644 --- a/abstract/environment_domain.ml +++ b/abstract/environment_domain.ml @@ -11,6 +11,7 @@ module type ENVIRONMENT_DOMAIN = sig (* variable management *) val addvar : t -> id -> t val rmvar : t -> id -> t + val vars : t -> id list (* abstract operation *) val assign : t -> id -> expr ext -> t (* S[id <- expr] *) @@ -25,8 +26,7 @@ module type ENVIRONMENT_DOMAIN = sig val subset : t -> t -> bool (* pretty-printing *) - val var_str : t -> id list -> string - val all_vars_str : t -> string + val var_str : t -> id list -> string end diff --git a/abstract/interpret.ml b/abstract/interpret.ml index fe998a6..79d4d2c 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -7,30 +7,79 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct let neg (e, l) = (AST_unary(AST_NOT, (e, l))), l + let binop op (e, l) e2 = + (AST_binary (op, (e,l), e2)), l + let m1 (e, l) = + binop AST_MINUS (e, l) (AST_int_const("1", l), l) + let p1 (e, l) = + binop AST_PLUS (e, l) (AST_int_const("1", l), l) + let rec condition cond env = begin match fst cond with | AST_binary (AST_LESS_EQUAL, e1, e2) -> E.compare env e1 e2 - | AST_binary (AST_GREATER_EQUAL, e1, e2) -> - E.compare env e2 e1 | AST_binary (AST_AND, e1, e2) -> E.meet (condition e1 env) (condition e2 env) | AST_binary (AST_OR, e1, e2) -> E.join (condition e1 env) (condition e2 env) - (* transformations *) + + (* transformations : remove not *) + | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) -> + condition cond env | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) -> condition (AST_binary(AST_OR, neg e1, neg e2), x) env | AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) -> condition (AST_binary(AST_AND, neg e1, neg e2), x) env - | _ -> env (* TODO : encode some more transformations *) + + | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) -> + let op2 = match op with + | AST_LESS_EQUAL -> AST_GREATER + | AST_LESS -> AST_GREATER_EQUAL + | AST_GREATER_EQUAL -> AST_LESS + | AST_GREATER -> AST_LESS_EQUAL + | AST_EQUAL -> AST_NOT_EQUAL + | AST_NOT_EQUAL -> AST_EQUAL + | _ -> assert false + in + condition (binop op2 e1 e2) env + + (* transformations : encode everything with leq *) + | AST_binary(AST_LESS, e1, e2) -> + condition + (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2)) + (binop AST_LESS_EQUAL (p1 e1) e2)) + env + | AST_binary (AST_GREATER_EQUAL, e1, e2) -> + condition + (binop AST_LESS_EQUAL e2 e1) + env + | AST_binary (AST_GREATER, e1, e2) -> + condition + (binop AST_LESS e2 e1) + env + | AST_binary (AST_EQUAL, e1, e2) -> + condition + (binop AST_AND (binop AST_LESS_EQUAL e1 e2) (binop AST_LESS_EQUAL e2 e1)) + env + | AST_binary (AST_NOT_EQUAL, e1, e2) -> + condition + (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1)) + env + + | _ -> env end let rec interp_stmt env stat = begin match fst stat with | AST_block b -> - List.fold_left interp_stmt env b + (* remember to remove vars that have gone out of scope at the end *) + let prevars = E.vars env in + let env2 = List.fold_left interp_stmt env b in + let postvars = E.vars env2 in + let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in + List.fold_left E.rmvar env2 rmvars | AST_assign ((id, _), exp) -> E.assign env id exp | AST_if (cond, tb, None) -> @@ -38,27 +87,57 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct (interp_stmt (condition cond env) tb) (condition (neg cond) env) | AST_if (cond, tb, Some eb) -> - E.join - (interp_stmt (condition cond env) tb) - (interp_stmt (condition (neg cond) env) eb) - | AST_while (cond, (body, _)) -> - (* TODO *) - env + let e1 = (interp_stmt (condition cond env) tb) in + let e2 = (interp_stmt (condition (neg cond) env) eb) in + E.join e1 e2 + | AST_while (cond, body) -> + let unroll_count = 3 in + let rec iter n i x = + (* Format.printf "(iter %d) i:%s x:%s @." n (E.var_str i (E.vars i)) + (E.var_str x (E.vars x)); *) + let out_state = condition (neg cond) i in + let next_step = interp_stmt (condition cond i) body in + (* Format.printf ". next step: %s@." (E.var_str next_step (E.vars next_step)); *) + if n < unroll_count then + E.join + out_state + (iter (n+1) next_step x) + else + let env2 = + E.widen + i + next_step + in + if env2 = i + then env2 + else E.join + out_state + (iter (n+1) env2 x) + in + condition (neg cond) (iter 0 env env) | AST_HALT -> E.bottom - | AST_assert (cond, l) -> + | AST_assert cond -> if not - (E.is_bot (condition (neg (cond, l)) env)) + (E.is_bot (condition (neg cond) env)) then begin - print_string (Abstract_syntax_printer.string_of_extent l); - print_string ": ERROR: assertion failure\n" + Format.printf "%s: ERROR: assertion failure@." + (Abstract_syntax_printer.string_of_extent (snd stat)); end; - condition (cond, l) env + condition cond env | AST_print items -> - print_string (Abstract_syntax_printer.string_of_extent (snd stat)); - print_string ": "; - print_string (E.var_str env (List.map fst items)); - print_string "\n"; + Format.printf "%s: %s@." + (Abstract_syntax_printer.string_of_extent (snd stat)) + (E.var_str env (List.map fst items)); env + | AST_local ((ty, _), vars) -> + List.fold_left + (fun env ((id, _), init) -> + let env2 = E.addvar env id in + match init with + | Some e -> E.assign env2 id e + | None -> env2) + env + vars | _ -> assert false (* not implemented *) end @@ -70,7 +149,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct E.init (fst prog) in - print_string "Output: "; - print_string (E.all_vars_str result); - print_string "\n" + Format.printf "Output: %s@." + (E.var_str result (E.vars result)) end diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml new file mode 100644 index 0000000..98f4daf --- /dev/null +++ b/abstract/intervals_domain.ml @@ -0,0 +1,122 @@ +open Value_domain + +module Intervals : VALUE_DOMAIN = struct + type bound = Int of Z.t | PInf | MInf + + type t = Itv of bound * bound | Bot + + (* utilities *) + let bound_leq a b = (* a <= b ? *) + match a, b with + | MInf, _ | _, PInf -> true + | Int a, Int b -> Z.leq a b + | x, y -> x = y + + let bound_add a b = + match a, b with + | MInf, Int a | Int a, MInf -> MInf + | PInf, Int a | Int a, PInf -> PInf + | MInf, MInf -> MInf + | PInf, PInf -> PInf + | Int a, Int b -> Int (Z.add a b) + | _ -> assert false + let bound_mul a b = + match a, b with + | PInf, Int(x) | Int(x), PInf -> + if x > Z.zero then PInf + else if x < Z.zero then MInf + else Int Z.zero + | MInf, Int(x) | Int(x), MInf -> + if x < Z.zero then PInf + else if x > Z.zero then MInf + else Int Z.zero + | Int(x), Int(y) -> Int(Z.mul x y) + | MInf, PInf | PInf, MInf -> MInf + | MInf, MInf | PInf, PInf -> PInf + + let bound_min a b = match a, b with + | MInf, _ | _, MInf -> MInf + | Int a, Int b -> Int (min a b) + | Int a, PInf -> Int a + | PInf, Int a -> Int a + | PInf, PInf -> PInf + let bound_max a b = match a, b with + | PInf, _ | _, PInf -> PInf + | Int a, Int b -> Int (max a b) + | Int a, MInf | MInf, Int a -> Int a + | MInf, MInf -> MInf + + let bound_neg = function + | PInf -> MInf + | MInf -> PInf + | Int i -> Int (Z.neg i) + + (* implementation *) + let top = Itv(MInf, PInf) + let bottom = Bot + let const i = Itv(Int i, Int i) + let rand i j = + if Z.leq i j then Itv(Int i, Int j) else Bot + + let subset a b = match a, b with + | Bot, _ -> true + | _, Bot -> false + | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b + + let join a b = match a, b with + | Bot, x | x, Bot -> x + | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d) + + let meet a b = match a, b with + | Bot, x | x, Bot -> Bot + | Itv(a, b), Itv(c, d) -> + let u, v = bound_max a c, bound_min b d in + if bound_leq u v + then Itv(u, v) + else Bot + + let widen a b = match a, b with + | x, Bot | Bot, x -> x + | Itv(a, b), Itv(c, d) -> + Itv( + (if not (bound_leq a c) then MInf else a), + (if not (bound_leq d b) then PInf else b)) + + let neg = function + | Bot -> Bot + | Itv(a, b) -> Itv(bound_neg b, bound_neg a) + let add a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d) + let sub a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c)) + let mul a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Itv(a, b), Itv(c, d) -> + Itv( + (bound_min (bound_min (bound_mul a c) (bound_mul a d)) + (bound_min (bound_mul b c) (bound_mul b d))), + (bound_max (bound_max (bound_mul a c) (bound_mul a d)) + (bound_max (bound_mul b c) (bound_mul b d)))) + + + let div a b = top (* TODO *) + let rem a b = top (* TODO *) + + let leq a b = match a, b with + | Bot, _ | _, Bot -> Bot, Bot + | Itv(a, b), Itv(c, d) -> + if not (bound_leq a d) + then Bot, Bot + else Itv(a, bound_min b d), Itv(bound_max a c, d) + + let bound_str = function + | MInf -> "-oo" + | PInf -> "+oo" + | Int i -> Z.to_string i + let to_string = function + | Bot -> "bot" + | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]" + +end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index d4118da..7221df1 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -66,16 +66,25 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | AST_identifier(a, _), AST_identifier(b, _) -> let v1, v2 = get_var env a, get_var env b in let v1', v2' = V.leq v1 v2 in - Env (VarMap.add a v1' (VarMap.add b v1' env)) - | AST_identifier(a, _), AST_int_const(s, _) -> - let v1, v2 = get_var env a, V.const (Z.of_string s) in - let v1', _ = V.leq v1 v2 in - Env (VarMap.add a v1' env) - | AST_int_const(s, _), AST_identifier(b, _) -> - let v1, v2 = V.const (Z.of_string s), get_var env b in - let _, v2' = V.leq v1 v2 in - Env (VarMap.add b v2' env) - | _ -> Env env) + Env (VarMap.add a v1' (VarMap.add b v2' env)) + | AST_identifier(a, _), _ -> + let v1, v2 = get_var env a, eval env e2 in + let v1', v2' = V.leq v1 v2 in + if V.bottom = v2' + then Bot + else Env (VarMap.add a v1' env) + | _, AST_identifier(b, _) -> + let v1, v2 = eval env e1, get_var env b in + let v1', v2' = V.leq v1 v2 in + if V.bottom = v1' + then Bot + else Env (VarMap.add b v2' env) + | _ -> + let v1, v2 = eval env e1, eval env e2 in + let v1', v2' = V.leq v1 v2 in + if V.bottom = v1' ||V.bottom = v2' + then Bot + else Env env) x let join a b = match a, b with @@ -106,7 +115,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct (* pretty-printing *) let var_str env vars = match env with - | Bot -> "bot" + | Bot -> "bottom" | Env env -> let v = List.fold_left (fun s id -> @@ -118,8 +127,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct in "[ " ^ v ^ " ]" - let all_vars_str env = - match env with - | Bot -> "bot" - | Env map -> var_str env (List.map fst (VarMap.bindings map)) + let vars env = match env with + | Bot -> [] + | Env env -> List.map fst (VarMap.bindings env) end diff --git a/main.ml b/main.ml index e09ac0e..8f33d2d 100644 --- a/main.ml +++ b/main.ml @@ -13,19 +13,49 @@ open Abstract_syntax_tree -module Env_dom = Nonrelational.NonRelational(Constant_domain.Constants) -module Interp = Interpret.Make(Env_dom) +module Env_dom_const = Nonrelational.NonRelational(Constant_domain.Constants) +module Interp_const = Interpret.Make(Env_dom_const) + +module Env_dom_interv = Nonrelational.NonRelational(Intervals_domain.Intervals) +module Interp_interv = Interpret.Make(Env_dom_interv) + +(* option parsing *) +let dump = ref false +let const_interp = ref false +let interv_interp = ref false +let poly_interp = ref false +let get_interp () = + if !interv_interp + then Interp_interv.interpret + else Interp_const.interpret + +let ifile = ref "" +let set_var v s = v := s + +let usage = "usage: analyzer [options] file.c" + +let options = [ + "--dump", Arg.Set dump, "Dump program source."; + "--const-interp", Arg.Set const_interp, "Use constant lattice interpreter."; + "--interv-interp", Arg.Set interv_interp, "Use interval lattice interpreter."; + "--poly-interp", Arg.Set poly_interp, "Use polyhedra lattice interpreter."; +] (* parse and print filename *) let doit filename = let prog = File_parser.parse_file filename in - Abstract_syntax_printer.print_prog Format.std_formatter prog; - Interp.interpret prog + if !dump then Abstract_syntax_printer.print_prog Format.std_formatter prog; + (get_interp ()) prog (* parses arguments to get filename *) let main () = - match Array.to_list Sys.argv with - | _::filename::_ -> doit filename - | _ -> invalid_arg "no source file specified" + Arg.parse options (set_var ifile) usage; + + if !ifile = "" then begin + Format.eprintf "No input file...@."; + exit 1 + end; + + doit !ifile let _ = main () diff --git a/tests/test.sh b/tests/test.sh new file mode 100755 index 0000000..443868a --- /dev/null +++ b/tests/test.sh @@ -0,0 +1,26 @@ +#!/bin/bash + +echo "== CONSTANT ABSTRACT DOMAIN" +for a in sources/*.c; do + if ../analyze --const-interp $a > /tmp/analyze_out.txt; + then + if diff -B /tmp/analyze_out.txt results/`basename -s .c $a`.constants.txt > /dev/null + then echo "OK $a" + else echo "FAIL $a" + fi + else echo "TODO $a"; + fi; +done; + +echo "== INTERVALS ABSTRACT DOMAIN" +for a in sources/*.c; do + if ../analyze --interv-interp $a > /tmp/analyze_out.txt; + then + if diff -B /tmp/analyze_out.txt results/`basename -s .c $a`.intervals.txt > /dev/null + then echo "OK $a" + else echo "FAIL $a" + fi + else echo "TODO $a"; + fi; +done; + -- cgit v1.2.3