Merge pull request #1717 from goblint/c2po-fix-lazy

Use LazyEval instead of Lazy in C2PODomain.

Author: jerhard

src/analyses/c2poAnalysis.ml

@@ -32,7 +32,8 @@ struct
   (* Returns Some true if we know for sure that it is true,
      and Some false if we know for sure that it is false,
      and None if we don't know anyhing. *)
-  let eval_guard ask cc e ik =
+  let eval_guard ask d e ik =
+    let cc = d.data in
     let open Queries in
     let prop_list = T.prop_of_cil ask e true in
     match split prop_list with
@@ -71,28 +72,30 @@ struct
     let open Queries in
     match ctx.local with
     | `Bot -> Result.top q
-    | `Lifted cc ->
+    | `Lifted d ->
       match q with
       | EvalInt e ->
         let ik = Cilfacade.get_ikind_exp e in
-        eval_guard (ask_of_man ctx) cc e ik
+        eval_guard (ask_of_man ctx) d e ik
       | Queries.Invariant context ->
         let scope = Node.find_fundec ctx.node in
-        let t = D.remove_vars_not_in_scope scope cc in
-        let conj = get_conjunction t in
+        let cc = D.remove_vars_not_in_scope scope d.data in
+        let conj = get_conjunction_from_data cc in
         let ask = ask_of_man ctx in
         conj_to_invariant ask conj
       | _ ->
         Result.top q
 
   (** Assign the right hand side rhs (that is already
       converted to a C-2PO term) to the term `lterm`. *)
-  let assign_term cc ask lterm rhs lval_t =
+  let assign_term d ask lterm rhs lval_t =
+    let cc = d.data in
     (* ignore assignments to values that are not 64 bits *)
     match T.get_element_size_in_bits lval_t, rhs with
     (* Indefinite assignment *)
     | lval_size, (None, _) ->
-      D.remove_may_equal_terms ask lval_size lterm cc
+      let cc = D.remove_may_equal_terms ask lval_size lterm cc in
+      data_to_t cc
     (* Definite assignment *)
     | lval_size, (Some rterm, Some roffset) ->
       let dummy_var = MayBeEqual.dummy_var lval_t in
@@ -106,8 +109,8 @@ struct
       meet_conjs_opt equal_dummy_rterm |>
       D.remove_may_equal_terms ask lval_size lterm |>
       meet_conjs_opt equal_dummy_lterm |>
-      D.remove_terms_containing_aux_variable
-
+      D.remove_terms_containing_aux_variable |>
+      data_to_t
     | _ -> (* this is impossible *)
       C2PODomain.top ()
 
@@ -131,8 +134,8 @@ struct
     match ctx.local with
     | `Bot ->
       `Bot
-    | `Lifted cc ->
-      let cc = assign_lval cc ask lval (T.of_cil ask expr) in
+    | `Lifted d ->
+      let cc = assign_lval d ask lval (T.of_cil ask expr) in
       let cc = reset_normal_form cc in
       let res = `Lifted cc in
       if M.tracing then M.trace "c2po-assign" "assign: var: %a; expr: %a; result: %s.\n" d_lval lval d_plainexp expr (D.show res);
@@ -144,13 +147,13 @@ struct
     let res =
       match ctx.local with
       | `Bot -> `Bot
-      | `Lifted cc ->
+      | `Lifted d ->
         if List.is_empty valid_props then
-          `Lifted cc
+          `Lifted d
         else
           try
-            let meet = meet_conjs_opt valid_props cc in
-            let t = reset_normal_form meet in
+            let meet = meet_conjs_opt valid_props d.data in
+            let t = data_to_t meet in
             `Lifted t
           with Unsat ->
             `Bot
@@ -167,8 +170,8 @@ struct
     match T.of_cil ask expr with
     | (Some term, Some offset) ->
       let ret_var_eq_term = [Equal (return_var, term, offset)] in
-      let assign_by_meet = meet_conjs_opt ret_var_eq_term d in
-      reset_normal_form assign_by_meet
+      let assign_by_meet = meet_conjs_opt ret_var_eq_term d.data in
+      data_to_t assign_by_meet
     | _ -> d
 
   let return ctx exp_opt f =
@@ -194,25 +197,27 @@ struct
     let ask = ask_of_man ctx in
     match ctx.local with
     | `Bot -> `Bot
-    | `Lifted cc ->
+    | `Lifted d ->
       let t =
         begin match lval_opt with
           | None ->
-            cc
+            d
           | Some lval ->
             (* forget information about var,
                but ignore assignments to values that are not 64 bits *)
             try
               let size = T.get_element_size_in_bits (typeOfLval lval) in
               let lterm = T.of_lval ask lval in
-              let cc = D.remove_may_equal_terms ask size lterm cc in
-              begin match desc.special exprs with
+              let cc = D.remove_may_equal_terms ask size lterm d.data in
+              let cc = begin match desc.special exprs with
                 | Malloc _
                 | Calloc _
                 | Alloca _ ->
                   add_block_diseqs cc lterm
                 | _ -> cc
               end
+              in
+              data_to_t cc
             with T.UnsupportedCilExpression _ ->
               C2PODomain.top ()
         end
@@ -224,7 +229,7 @@ struct
         else
           branch ctx exp true
       | _ ->
-        `Lifted (reset_normal_form t)
+        `Lifted t
 
   (** First all local variables of the function are duplicated,
       then we remember the value of each local variable at the beginning of the function by using the analysis startState.
@@ -233,13 +238,14 @@ struct
     (* add duplicated variables, and set them equal to the original variables *)
     match ctx.local with
     | `Bot -> [`Bot, `Bot]
-    | `Lifted cc ->
+    | `Lifted d ->
       let ghost_equality v =
         Equal (T.term_of_varinfo (DuplicVar v), T.term_of_varinfo (NormalVar v), Z.zero)
       in
       let ghost_equalities_for_params = List.map ghost_equality f.sformals in
       let equalities_to_add = T.filter_valid_pointers ghost_equalities_for_params in
-      let state_with_ghosts = meet_conjs_opt equalities_to_add cc in
+      let state_with_ghosts = meet_conjs_opt equalities_to_add d.data in
+      let state_with_ghosts = data_to_t state_with_ghosts in
       if M.tracing then begin
         let dummy_lval = Var (Var.dummy_varinfo (TVoid [])), NoOffset in
         let lval = BatOption.default dummy_lval var_opt in
@@ -250,7 +256,8 @@ struct
         let reachable = f.sformals @ f.slocals @ reachable_from_args ctx args in
         Var.from_varinfo reachable f.sformals
       in
-      let new_state = D.remove_terms_not_containing_variables reachable_variables state_with_ghosts in
+      let new_state = D.remove_terms_not_containing_variables reachable_variables state_with_ghosts.data in
+      let new_state = data_to_t new_state in
       if M.tracing then M.trace "c2po-function" "enter2: result: %s\n" (C2PODomain.show new_state);
       let new_state = reset_normal_form new_state in
       [ctx.local, `Lifted new_state]
@@ -264,7 +271,7 @@ struct
   let combine_env ctx lval_opt expr f args t_context_opt f_d (f_ask: Queries.ask) =
     match ctx.local with
     | `Bot -> `Bot
-    | `Lifted cc ->
+    | `Lifted d ->
       let caller_ask = ask_of_man ctx in
       (* assign function parameters to duplicated values *)
       let arg_assigns = GobList.combine_short f.sformals args in
@@ -273,30 +280,32 @@ struct
         let arg = T.of_cil f_ask arg in
         assign_term st caller_ask ghost_var arg var.vtype
       in
-      let state_with_assignments = List.fold_left assign_term cc arg_assigns in
+      let state_with_assignments = List.fold_left assign_term d arg_assigns in
 
       if M.tracing then M.trace "c2po-function" "combine_env0: state_with_assignments: %s\n" (C2PODomain.show state_with_assignments);
 
       (*remove all variables that were tainted by the function*)
       let tainted = f_ask.f (MayBeTainted) in
       if M.tracing then M.trace "c2po-tainted" "combine_env1: %a\n" MayBeEqual.AD.pretty tainted;
 
-      let local = D.remove_tainted_terms caller_ask tainted state_with_assignments in
+      let local = D.remove_tainted_terms caller_ask tainted state_with_assignments.data in
+      let local = data_to_t local in
       match D.meet (`Lifted local) f_d with
       | `Bot -> `Bot
-      | `Lifted cc ->
-        let cc = reset_normal_form @@ remove_out_of_scope_vars cc f in
+      | `Lifted d ->
+        let cc = remove_out_of_scope_vars d.data f in
+        let d = data_to_t cc in
         if M.tracing then begin
           let dummy_lval = Var (Var.dummy_varinfo (TVoid[])), NoOffset in
           let lval = BatOption.default dummy_lval lval_opt in
-          M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show cc)
+          M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
         end;
-        `Lifted cc
+        `Lifted d
 
   let combine_assign ctx var_opt expr f args t_context_opt f_d (f_ask: Queries.ask) =
     match ctx.local with
     | `Bot -> `Bot
-    | `Lifted cc ->
+    | `Lifted d ->
       let caller_ask = ask_of_man ctx in
       (* assign function parameters to duplicated values *)
       let arg_assigns = GobList.combine_short f.sformals args in
@@ -305,24 +314,24 @@ struct
         let arg = T.of_cil f_ask arg in
         assign_term st caller_ask ghost_var arg var.vtype
       in
-      let state_with_assignments = List.fold_left assign_term cc arg_assigns in
+      let state_with_assignments = List.fold_left assign_term d arg_assigns in
       match D.meet (`Lifted state_with_assignments) f_d with
       | `Bot -> `Bot
-      | `Lifted cc ->
-        let cc = match var_opt with
+      | `Lifted d ->
+        let d = match var_opt with
           | None ->
-            cc
+            d
           | Some lval ->
             let return_type = typeOfLval lval in
             let return_var = MayBeEqual.return_var return_type  in
             let return_var = (Some return_var, Some Z.zero) in
-            assign_lval cc f_ask lval return_var
+            assign_lval d f_ask lval return_var
         in
-        if M.tracing then M.trace "c2po-function" "combine_assign1: assigning return value: %s\n" (C2PODomain.show cc);
-        let cc = remove_out_of_scope_vars cc f in
-        let cc = reset_normal_form cc in
-        if M.tracing then M.trace "c2po-function" "combine_assign2: result: %s\n" (C2PODomain.show cc);
-        `Lifted cc
+        if M.tracing then M.trace "c2po-function" "combine_assign1: assigning return value: %s\n" (C2PODomain.show d);
+        let d = remove_out_of_scope_vars d.data f in
+        let d = data_to_t d in
+        if M.tracing then M.trace "c2po-function" "combine_assign2: result: %s\n" (C2PODomain.show d);
+        `Lifted d
 
   let startstate v =
     D.top ()