diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 17 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 40 | ||||
| -rw-r--r-- | abstract/transform.ml | 6 | ||||
| -rw-r--r-- | abstract/value_domain.ml | 2 |
4 files changed, 31 insertions, 34 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index 4f66540..4c3fddb 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -56,7 +56,7 @@ end = struct | AST_activate (b, _) -> let rec do_branch = function | AST_activate_body b -> - List.map (fun (p, id, t) -> p, node^"/"^b.act_id^"."^id, t) b.act_locals + List.map (fun (p, id, t) -> p, node^"/"^id, t) b.act_locals @ extract_all_vars p (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> @@ -81,15 +81,15 @@ end = struct E.init all_vars in - - - let init_f = Transform.init_f_of_prog p root in - let env = E.apply_f env init_f in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f; + Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars; + + let env = E.apply_f env init_f in + { p; root_scope; f; cl; all_vars; env } (* @@ -142,7 +142,7 @@ end = struct E.join acc0 j in - let widen_delay = 2 in + let widen_delay = 10 in let rec iter n i = let i' = if n < widen_delay @@ -170,10 +170,11 @@ end = struct E.print_all stay; Format.printf "Probes:@[<hov>"; - List.iter (fun (p, id, _) -> if p then Format.printf "@ %a ∊ %a," Formula_printer.print_id id E.print_itv (E.var_itv stay id)) - st.all_vars + st.all_vars; + Format.printf "@]@." + end diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index b83edc1..3cdcc31 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -69,20 +69,26 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | Env env -> V.to_itv (get_var env id) (* Set-theoretic operations *) + let f_in_merge f _ a b = match a, b with + | Some a, None -> Some a + | None, Some b -> Some b + | Some a, Some b -> Some (f a b) + | _ -> assert false + let join a b = match a, b with | Bot, x | x, Bot -> x | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.join a b) m n) + strict (VarMap.merge (f_in_merge V.join) m n) let meet a b = match a, b with | Bot, _ | _, Bot -> Bot | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.meet a b) m n) + strict (VarMap.merge (f_in_merge V.meet) m n) let widen a b = match a, b with | Bot, x | x, Bot -> x | Env m, Env n -> - strict (VarMap.map2z (fun _ a b -> V.widen a b) m n) + strict (VarMap.merge (f_in_merge V.widen) m n) (* Inclusion and equality *) let subset a b = match a, b with @@ -161,27 +167,17 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct List.fold_left restrict_var env (extract_var (expr, zop, NIntConst 0)) - let rec apply_cl x (cons, rest) = - let apply_cl_l x = List.fold_left apply_cons x cons in - - let y = fix eq apply_cl_l x in - if debug then Format.printf "-[@."; - let z = apply_cl_r y rest in - if debug then Format.printf "-]@."; - fix eq apply_cl_l z - - and apply_cl_r x = function - | CLTrue -> x + let rec apply_cl x (cons, rest) = match rest with + | CLTrue -> + let apply_cl_l x = List.fold_left apply_cons x cons in + fix eq apply_cl_l x | CLFalse -> vbottom x | CLAnd(a, b) -> - let y = apply_cl_r x a in - apply_cl_r y b - | CLOr(a, b) -> - if debug then Format.printf "<<@."; - let y = apply_cl x a in - if debug then Format.printf "\\/@."; - let z = apply_cl x b in - if debug then Format.printf ">>@."; + let y = apply_cl x (cons, a) in + apply_cl y (cons, b) + | CLOr((ca, ra), (cb, rb)) -> + let y = apply_cl x (cons@ca, ra) in + let z = apply_cl x (cons@cb, rb) in join y z let apply_f x f = apply_cl x (conslist_of_f f) diff --git a/abstract/transform.ml b/abstract/transform.ml index 40390dd..b141cc6 100644 --- a/abstract/transform.ml +++ b/abstract/transform.ml @@ -164,7 +164,7 @@ and f_of_scope active td (node, prefix, eqs) = in let rec do_tree_act = function | AST_activate_body b -> - f_of_scope true td (node, b.act_id^"_", b.body) + f_of_scope true td (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> BOr( f_and (f_of_bexpr td (node, prefix) c) @@ -174,7 +174,7 @@ and f_of_scope active td (node, prefix, eqs) = ) and do_tree_inact = function | AST_activate_body b -> - f_of_scope false td (node, b.act_id^"_", b.body) + f_of_scope false td (node, b.act_id^".", b.body) | AST_activate_if(_, a, b) -> f_and (do_tree_inact a) (do_tree_inact b) in @@ -223,7 +223,7 @@ let rec init_f_of_scope p (node, prefix, eqs) = | AST_activate (b, _) -> let rec cond_eq = function | AST_activate_body b -> - init_f_of_scope p (node, b.act_id^"_", b.body) + init_f_of_scope p (node, b.act_id^".", b.body) | AST_activate_if(c, a, b) -> f_and (expr_eq c) (f_and (cond_eq a) (cond_eq b)) diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index 7b9d557..bb27126 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -8,7 +8,7 @@ let string_of_bound = function | Int i -> string_of_int i let string_of_itv = function | Bot -> "⊥" - | Itv(a, b) -> "[" ^ (string_of_bound a) ^ ";" ^ (string_of_bound b) ^ "]" + | Itv(a, b) -> "[" ^ (string_of_bound a) ^ "; " ^ (string_of_bound b) ^ "]" module type VALUE_DOMAIN = sig type t |