caterinaurban · naim-mr · Aug 20, 2024 · Aug 29, 2024 · Aug 29, 2024 · Aug 29, 2024
diff --git a/domains/DecisionTree.ml b/domains/DecisionTree.ml
@@ -86,7 +86,15 @@ struct
       | Node ((c,_),l,r) -> Format.fprintf fmt "\n%sNODE %a%a%a" ind 
                               (C.print vars) c (aux (ind ^ "  ")) l (aux (ind ^ "  ")) r
     in aux "" fmt t
-
+  let output_json vars t:Yojson.Safe.t= 
+
+    let rec aux  t = 
+      match t with
+      | Bot -> `String "BOT"
+      | Leaf f -> `Assoc [("Leaf", `String (Format.asprintf "%a"  (F.print) f))]
+      | Node ((c,_),l,r) -> 
+            `Assoc [("Node",`Assoc [("constraint",`String (Format.asprintf "%a" (C.print vars) c  ));("left", aux l );("right", aux r)] )]
+     in aux t.tree
   (**
      Prints a tree in graphviz 'dot' format for visualization. 
      http://www.graphviz.org/content/dot-language

diff --git a/domains/Domain.ml b/domains/Domain.ml
@@ -43,6 +43,7 @@ sig
 
   val compress : t -> t
   val print : Format.formatter -> t -> unit
+  val output_json : var list -> t -> Yojson.Safe.t
   val print_graphviz_dot : Format.formatter -> t -> unit
 
 end
diff --git a/domains/dune b/domains/dune
@@ -1,7 +1,7 @@
 (library
  (name domains)
  (libraries utils frontend banal apron apron.boxMPQ apron.octMPQ
-   apron.polkaMPQ)
+   apron.polkaMPQ yojson)
  (flags
   (:standard -open Utils -open Banal -open Frontend -open Apron)))
 

diff --git a/main/CFGCTLIterator.ml b/main/CFGCTLIterator.ml
@@ -5,7 +5,7 @@ open Apron
 open Domain
 open Partition
 open Functions
-open Iterator
+open Config
 open ForwardIterator
 
 
@@ -334,6 +334,7 @@ module CFGCTLIterator(D: RANKING_FUNCTION) = struct
     let inv = compute cfg main loop_heads domSets property in
     let programInvariant = NodeMap.find main.func_entry inv in
     let precondition = Conversion.of_bool_expr precondition in
+    tree := (D.output_json  (List.map (Cfgfrontend.Conversion.of_var) cfg.cfg_vars) programInvariant);
     D.defined ~condition:precondition programInvariant
 
 end

diff --git a/main/CFGForwardIterator.ml b/main/CFGForwardIterator.ml
@@ -9,7 +9,7 @@
 open Cfg
 open CFGInterpreter
 open Partition
-open Iterator
+open Config
 
 module CFGForwardIterator (B: PARTITION) = struct
 

diff --git a/main/CFGInterpreter.ml b/main/CFGInterpreter.ml
@@ -9,7 +9,7 @@
 (***************************************************)
 
 open Cfg
-open Iterator
+open Config
 
 
 (* log worklist algorithm *)

diff --git a/main/CTLIterator.ml b/main/CTLIterator.ml
@@ -5,7 +5,7 @@ open Apron
 open Domain
 open Partition
 open Functions
-open Iterator
+open Config
 open ForwardIterator
 
 (* type for CTL properties, instantiated with bExp for atomic propositions *)
@@ -196,6 +196,7 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
         if !tracebwd && not !minimal then Format.fprintf !fmt "### %a ###:\n%a\n" label_print blockLabel D.print in_state;
         addInv blockLabel in_state
       | A_block (blockLabel,(stmt,_),nextBlock) ->
+        let pre_dom = if !refine then Some (fwdInv blockLabel) else None in 
         let invBlockKeep = InvMap.find blockLabel inv_keep in 
         let invBlockReset = InvMap.find blockLabel inv_reset in
         let d_until = fun t -> D.until t invBlockKeep invBlockReset in
@@ -204,21 +205,22 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
         let in_state = match stmt with 
           | A_label (l,_) -> out_state
           | A_return -> bot
-          | A_assign ((l,_),(e,_)) -> bwd_assign out_state (l,e)
-          | A_assert (b,_) -> bwd_filter out_state b
+          | A_assign ((l,_),(e,_)) -> bwd_assign  ?domain: pre_dom out_state (l,e)
+          | A_assert (b,_) -> bwd_filter ?domain: pre_dom out_state b
           | A_if ((b,ba),s1,s2) ->
             let in_if = bwd out_state s1 in (* compute 'in state for if-block*)
             let in_else = bwd out_state s2 in (* compute 'in state for else-block *)
-            let in_if_filtered = bwd_filter in_if b in (* filter *)
-            let in_else_filtered = bwd_filter in_else (fst (negBExp (b,ba))) in (* filter *)
+            let in_if_filtered = bwd_filter ?domain:pre_dom in_if b in (* filter *)
+            let in_else_filtered = bwd_filter ?domain:pre_dom in_else (fst (negBExp (b,ba))) in (* filter *)
             branch_join in_if_filtered in_else_filtered (* join the two branches *)
           | A_while (l,(b,ba),loop_body) ->
-            let out_exit = bwd_filter out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *)
+            let pre_dom = if !refine then Some (fwdInv l) else None in 
+            let out_exit = bwd_filter ?domain:pre_dom out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *)
             let rec aux (* recursive function that iteratively computes fixed point for 'in' state at loop head *)
                 in_state (* 'in' state of the previous iteration *)
                 out_enter (* current 'out' state when entering the loop body *)
                 n = (* iteration counter *)
-              let in_state' = d_until (D.join APPROXIMATION out_exit out_enter) in (* 'in' state for this iteration *)
+              let in_state' = d_until (branch_join out_exit out_enter) in (* 'in' state for this iteration *)
               if !tracebwd && not !minimal then begin
                 Format.fprintf !fmt "### %a:%i ###:\n" label_print l n;
                 Format.fprintf !fmt "out_exit: %a\n" D.print out_exit;
@@ -228,33 +230,54 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
               end;
               let isLeqComp = D.isLeq COMPUTATIONAL in_state' in_state in
               let isLeqApprox = D.isLeq APPROXIMATION in_state' in_state in
-              if isLeqComp && isLeqApprox then
+              let jokers = max 0 (!retrybwd * (!Ordinals.max + 1) - n + !joinbwd) in
+              if isLeqComp then
+                if isLeqApprox then begin
                 (* fixed-point reached *)
                 let fixed_point = in_state in
                 if !tracebwd && not !minimal then begin
                   Format.fprintf !fmt "### %a:FIXPOINT ###:\n" label_print l;
                   Format.fprintf !fmt "in_state: %a\n" D.print fixed_point;
                 end;
                 fixed_point
-              else
-                (*fixed-point not yet reached, continue with next iteration*)
+                end
+              else begin
+               (*fixed-point not yet reached, continue with next iteration*)
                 let in_state'' = 
                   if n <= !joinbwd then 
                     in_state' (* iteration count below widening threshold *)
-                  else if (not isLeqComp) then 
-                    D.widen in_state (D.join COMPUTATIONAL in_state in_state') (* widening threshold reached, apply widening *)
-                      (* NOTE: the join might be necessary to ensure termination because of a bug (???) *)
-                  else 
-                    D.widen in_state in_state' (* widening threshold reached, apply widening *)
+                else
+                    D.widen ~jokers:jokers in_state in_state' (* widening threshold reached, apply widening *)
+
                 in
                 if !tracebwd && not !minimal then Format.fprintf !fmt "in'': %a\n" D.print in_state'';
-                let out_enter' = bwd_filter (bwd in_state'' loop_body) b in (* process loop body again with updated 'in' state *)
+                let out_enter' = bwd_filter  ?domain: pre_dom (bwd in_state'' loop_body) b in (* process loop body again with updated 'in' state *)
                 aux in_state'' out_enter' (n+1) (* run next iteration *)
+              end
+              else
+                let in_state'' =
+                  if n <= !joinbwd then
+                  in_state'
+                  else
+                    D.widen ~jokers:jokers in_state
+                      (D.join COMPUTATIONAL in_state in_state')
+                      (* NOTE: the join might be necessary to ensure termination because of a bug (???) *)
+                in
+                if !tracebwd && not !minimal then
+                  Format.fprintf !fmt "in'': %a\n" D.print in_state'';
+                let out_enter' = 
+                  (bwd in_state'' loop_body) in
+                let out_enter' = D.filter ?domain:pre_dom out_enter' b in
+                aux in_state'' out_enter' (n + 1)
             in
-            let initial_in = bot in (* start with bottom as initial 'in' state *)
-            let initial_out_enter = bwd_filter (bwd initial_in loop_body) b in (* process loop body with initial 'in' state *)
+            let initial_in = D.bot ?domain:pre_dom program.environment program.variables  in (* start with bottom as initial 'in' state *)
+            let initial_out_enter = D.filter ?domain:pre_dom (bwd initial_in loop_body) b in (* process loop body with initial 'in' state *)
             let final_in_state = aux initial_in initial_out_enter 1 in (* compute fixed point for loop-head *)
-            addInv l final_in_state 
+            let ret = addInv l final_in_state in 
+            if !refine then
+              D.refine ret (Option.get pre_dom)
+            else
+              ret
           | A_call (f,ss) -> raise (Invalid_argument "bwdStm:A_call")
           | A_recall (f,ss) -> raise (Invalid_argument "bwdStm:A_recall")
         in
@@ -299,18 +322,20 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
         let out = if !refine then D.refine out (fwdInv blockLabel) else out in
         addInv blockLabel (D.mask current_in out) 
       | A_block (blockLabel, (stmt,_), nextBlock) ->
+        let pre_dom = if !refine then Some (fwdInv blockLabel) else None in 
         let out_state = bwd out nextBlock in (* recursively process the rest of the program, this gives us the 'out' state for this statement *)
         let new_in = match stmt with 
           | A_label (l,_) -> out_state
           | A_return -> if use_sink_state then zero else bot 
-          | A_assign ((l,_),(e,_)) -> D.mask current_in (bwd_assign out_state (l,e))
-          | A_assert (b,_) -> D.mask current_in (bwd_filter out_state b)
+          | A_assign ((l,_),(e,_)) -> D.mask current_in (bwd_assign ?domain:pre_dom out_state (l,e))
+          | A_assert (b,_) -> D.mask current_in (bwd_filter ?domain:pre_dom out_state b)
           | A_if ((b,ba),s1,s2) ->
-            let out_if = bwd_filter (bwd out_state s1) b in (* compute 'out' state for if-block*)
-            let out_else = bwd_filter (bwd out_state s2) (fst (negBExp (b,ba))) in (* compute 'out' state for else-block *)
+            let out_if = bwd_filter ?domain:pre_dom (bwd out_state s1) b in (* compute 'out' state for if-block*)
+            let out_else = bwd_filter ?domain:pre_dom (bwd out_state s2) (fst (negBExp (b,ba))) in (* compute 'out' state for else-block *)
             D.mask current_in (branch_join out_if out_else) (* join the two branches and combine with current 'in' state using mask *)
           | A_while (l,(b,ba),loop_body) ->
-            let out_exit = bwd_filter out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *)
+            let pre_dom = if !refine then Some (fwdInv l) else None in 
+            let out_exit = bwd_filter ?domain:pre_dom  out_state (fst (negBExp (b,ba))) in (* 'out' state when not entering the loop body *)
             let rec aux (* recursive function that iteratively computes fixed point for 'in' state at loop head *)
                 (current_in:D.t) (* 'in' state of the previous iteration *)
                 (out_enter:D.t) (* current 'out' state when entering the loop body *)
@@ -337,11 +362,11 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
                   if n <= !joinbwd then updated_in (* widening threshold not yet reached *)
                   else D.dual_widen current_in updated_in (* use dual_widen after widening threshold reached *)
                 in
-                let out_enter' = bwd_filter (bwd updated_in' loop_body) b in (* process loop body again with updated 'in' state *)
+                let out_enter' = bwd_filter ?domain:pre_dom (bwd updated_in' loop_body) b in (* process loop body again with updated 'in' state *)
                 (* next iteration *)
                 aux updated_in' out_enter' (n+1)
             in
-            let initial_out_enter = bwd_filter (bwd current_in loop_body) b in (* process loop body with current 'in' state at loop-head *)
+            let initial_out_enter = bwd_filter ?domain:pre_dom (bwd current_in loop_body) b in (* process loop body with current 'in' state at loop-head *)
             let final_in_state = aux current_in initial_out_enter 1 in (* compute fixed point for while-loop starting with current 'in' state at loop-head *)
             addInv l final_in_state 
           | A_call (f,ss) -> raise (Invalid_argument "bwdStm:A_call")
@@ -397,8 +422,6 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
     aux program.mainFunction.funcBody bot ();
     let zero_leafs t = D.until t top t in (* set all defined leafs of the decision trees to zero *)
     InvMap.map zero_leafs !invMap 
-
-
   (* 
     Assign atomic state to those blocks that match the label and bot to all others
   *)
@@ -534,6 +557,7 @@ module CTLIterator(D: RANKING_FUNCTION) = struct
     let inv = compute program property in
     let initialLabel = block_label program.mainFunction.funcBody in
     let programInvariant = InvMap.find initialLabel inv in
+    tree := (D.output_json  program.variables programInvariant);
     D.defined ?condition:precondition programInvariant
 
 

diff --git a/main/ForwardIterator.ml b/main/ForwardIterator.ml
@@ -7,7 +7,7 @@ open AbstractSyntax
 open InvMap
 open Apron
 open Functions
-open Iterator
+open Config
 open Domain
 open Partition
 

diff --git a/main/GuaranteeIterator.ml b/main/GuaranteeIterator.ml
@@ -9,7 +9,7 @@ open ForwardIterator
 open Apron
 open Domain
 open Functions
-open Iterator
+open Config
 
 module GuaranteeIterator (D: RANKING_FUNCTION) =
 struct
@@ -149,6 +149,7 @@ struct
           Format.fprintf !fmt "\nBackward Analysis:\n";
         bwdMap_print !fmt !bwdInvMap;
       end;
+    tree := (D.output_json  vars i);
     D.defined ~condition:precondition i
 
 end