diff options
| -rw-r--r-- | abstract/environment_domain.ml | 1 | ||||
| -rw-r--r-- | abstract/interpret.ml | 30 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 10 | ||||
| -rw-r--r-- | abstract/relational_apron.ml | 10 | ||||
| -rw-r--r-- | libs/util.ml | 6 |
5 files changed, 38 insertions, 19 deletions
diff --git a/abstract/environment_domain.ml b/abstract/environment_domain.ml index 404548c..b2d18c4 100644 --- a/abstract/environment_domain.ml +++ b/abstract/environment_domain.ml @@ -25,6 +25,7 @@ module type ENVIRONMENT_DOMAIN = sig (* order *) val subset : t -> t -> bool + val eq : t -> t -> bool (* pretty-printing *) val var_str : t -> id list -> string diff --git a/abstract/interpret.ml b/abstract/interpret.ml index f6a6cb4..e28bf84 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -76,7 +76,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct | _ -> env end - let rec interp_stmt env stat = + let rec interp_stmt_a show_asserts env stat = + let interp_stmt = interp_stmt_a show_asserts in begin match fst stat with | AST_block b -> (* remember to remove vars that have gone out of scope at the end *) @@ -107,25 +108,30 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct let env, u_u = unroll env 3 in (* widening *) let widen_delay = 3 in - let fsharp i = - let next_step = interp_stmt (condition cond i) body in + let fsharp a i = + let next_step = interp_stmt_a a (condition cond i) body in E.join env next_step in let rec iter n i = let i' = - (if n < widen_delay then E.join else E.widen) - i - (fsharp i) + if n < widen_delay + then E.join i (fsharp show_asserts i) + else E.widen i (fsharp false i) in - if i = i' then i else iter (n+1) i' + if E.eq i i' then i else iter (n+1) i' in let x = iter 0 env in - let y = fix fsharp x in (* decreasing iteration *) - E.join (condition (neg cond) y) u_u + let y = fix E.eq (fsharp false) x in (* decreasing iteration *) + let z = + if show_asserts then + (* last iteration : show real assert failures *) + fsharp true y + else y in + E.join (condition (neg cond) z) u_u | AST_HALT -> bottom_with_vars (E.vars env) | AST_assert cond -> - if not - (E.is_bot (condition (neg cond) env)) + if show_asserts && + not (E.is_bot (condition (neg cond) env)) then begin Format.printf "%s: ERROR: assertion failure@." (Abstract_syntax_printer.string_of_extent (snd stat)); @@ -147,6 +153,8 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct vars | _ -> assert false (* not implemented *) end + + let interp_stmt = interp_stmt_a true let interpret prog = let result = List.fold_left diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index 188c8bc..530b373 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -113,6 +113,16 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct (fun _ v -> v = V.top) (fun _ a b -> V.subset a b) m n + + let eq a b = match a, b with + | Bot, Bot -> true + | Env m, Env n -> + VarMap.for_all2o + (fun _ _ -> false) + (fun _ _ -> false) + (fun _ a b -> a = b) + m n + | _ -> false (* pretty-printing *) let var_str env vars = diff --git a/abstract/relational_apron.ml b/abstract/relational_apron.ml index 926d2a9..4541b0e 100644 --- a/abstract/relational_apron.ml +++ b/abstract/relational_apron.ml @@ -59,9 +59,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct let env2 = Environment.add env [| Var.of_string id |] [||] in Abstract1.change_environment manager x env2 false let rmvar x id = + let v = [| Var.of_string id |] in let env = Abstract1.env x in - let env2 = Environment.remove env [| Var.of_string id |] in - Abstract1.change_environment manager x env2 false + let env2 = Environment.remove env v in + let y = Abstract1.forget_array manager x v false in + Abstract1.change_environment manager y env2 false let vars x = List.map Var.to_string @@ Array.to_list @@ fst @@ Environment.vars @@ Abstract1.env x @@ -98,13 +100,11 @@ module RelationalDomain : ENVIRONMENT_DOMAIN = struct let widen = Abstract1.widening manager let subset = Abstract1.is_leq manager + let eq = Abstract1.is_eq manager let var_str x idl = let prevars = vars x in let rm_vars_l = List.filter (fun id -> not (List.mem id idl)) prevars in - (* print_list "prevars" prevars; - print_list "idl" idl; - print_list "rm_vars_l" rm_vars_l; *) let rm_vars = Array.of_list (List.map Var.of_string rm_vars_l) in let xx = Abstract1.forget_array manager x rm_vars false in let b = Buffer.create 80 in diff --git a/libs/util.ml b/libs/util.ml index b1fcdc4..30cf5bf 100644 --- a/libs/util.ml +++ b/libs/util.ml @@ -2,11 +2,11 @@ exception TypeError module VarMap = Mapext.Make(String) -let rec fix f s = +let rec fix equal f s = let fs = f s in - if fs = s + if equal fs s then fs - else fix f fs + else fix equal f fs let (@@) f x = f x |