Abstract interpretation gives good results on the limiter example.

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