Merge pull request #45 from paveon/paveon/LOOPER-1

[looper] Remove guards

Author: paveon

infer/src/backend/Summary.ml

@@ -132,10 +132,6 @@ module LooperSummary = struct
     ; err_log }
 
 
-  (* module SQLite = SqliteUtils.MarshalledDataNOTForComparison (struct
-       type nonrec t = t
-     end) *)
-
   let merge ~into x = Errlog.merge ~into:into.err_log x.err_log
 
   module SQLite = struct

infer/src/looper/DifferenceConstraint.ml

@@ -27,7 +27,16 @@ let make ?(const_part = (Binop.PlusA None, IntLit.zero)) lhs_norm rhs_norm =
 
 let make_value_rhs ?(const_part = (Binop.PlusA None, IntLit.zero)) rhs_norm =
   let op, rhs_const = const_part in
-  match op with Binop.PlusA _ | Binop.Shiftrt -> (rhs_norm, op, rhs_const) | _ -> assert false
+  match op with
+  | Binop.PlusA _ ->
+      let rhs_const =
+        if IntLit.lt rhs_const IntLit.minus_one then IntLit.minus_one else rhs_const
+      in
+      (rhs_norm, op, rhs_const)
+  | Binop.Shiftrt ->
+      (rhs_norm, op, rhs_const)
+  | _ ->
+      assert false
 
 
 let rec is_constant (lhs_norm, rhs) =

infer/src/looper/DifferenceConstraintProgram.ml

@@ -6,21 +6,16 @@ module F = Format
 module DC = DifferenceConstraint
 module LTS = LabeledTransitionSystem
 
-(* Difference Constraint Program *)
-type edge_output_type = GuardedDCP | DCP [@@deriving compare]
-
 module EdgeData = struct
   type t =
     { backedge: bool
     ; branch_info: (Sil.if_kind * bool * Location.t) option
     ; mutable calls: EdgeExp.CallPair.Set.t
     ; mutable constraints: DC.t list
-    ; mutable guards: EdgeExp.Set.t
     ; mutable condition_norms: EdgeExp.Set.t list
     ; mutable bound: EdgeExp.T.t option
     ; mutable bound_norms: EdgeExp.Set.t list
-    ; mutable computing_bound: bool
-    ; mutable edge_type: edge_output_type }
+    ; mutable computing_bound: bool }
   [@@deriving compare]
 
   let equal = [%compare.equal: t]
@@ -30,12 +25,10 @@ module EdgeData = struct
     ; branch_info= lts_edge_data.branch_info
     ; calls= lts_edge_data.calls
     ; constraints= []
-    ; guards= EdgeExp.Set.empty
     ; condition_norms= lts_edge_data.condition_norms
     ; bound= None
     ; bound_norms= []
-    ; computing_bound= false
-    ; edge_type= DCP }
+    ; computing_bound= false }
 
 
   let get_dc key constraints =
@@ -77,63 +70,20 @@ module EdgeData = struct
 
   let is_backedge edge = edge.backedge
 
-  let active_guards edge =
-    let normal_guards =
-      EdgeExp.Set.fold
-        (fun guard acc ->
-          match get_dc guard edge.constraints with
-          | Some dc ->
-              if DC.is_decreasing dc && DC.same_norms dc then acc else EdgeExp.Set.add guard acc
-          | _ ->
-              EdgeExp.Set.add guard acc )
-        edge.guards EdgeExp.Set.empty
-    in
-    let guards_via_constant_reset =
-      List.filter_map edge.constraints ~f:(fun (lhs_norm, rhs) ->
-          let process_value (rhs_norm, op, const) =
-            if EdgeExp.is_zero rhs_norm then
-              match op with
-              | (Binop.PlusA _ | Binop.PlusPI) when IntLit.gt const IntLit.zero ->
-                  true
-              | _ ->
-                  false
-            else
-              match EdgeExp.evaluate_const_exp rhs_norm with
-              | Some value ->
-                  let total_value = EdgeExp.eval_consts op value const in
-                  if IntLit.gt total_value IntLit.zero then true else false
-              | None ->
-                  false
-          in
-          match rhs with
-          | DC.Value v ->
-              if process_value v then Some lhs_norm else None
-          | DC.Pair (lb, ub) ->
-              if process_value lb && process_value ub then Some lhs_norm else None )
-    in
-    EdgeExp.Set.union normal_guards (EdgeExp.Set.of_list guards_via_constant_reset)
-
-
   (* Required by Graph module interface *)
   let default =
     { backedge= false
     ; branch_info= None
-    ; edge_type= DCP
     ; constraints= []
     ; calls= EdgeExp.CallPair.Set.empty
-    ; guards= EdgeExp.Set.empty
     ; condition_norms= []
     ; bound= None
     ; bound_norms= []
     ; computing_bound= false }
 
 
-  let set_edge_output_type edge output_type = edge.edge_type <- output_type
-
   let branch_type edge = match edge.branch_info with Some (_, branch, _) -> branch | _ -> false
 
-  let add_guards edge guards = edge.guards <- guards
-
   let add_constraint edge dc =
     (* debug_log "[DC derivation] Adding new DC: %a\n" DC.pp dc; *)
     edge.constraints <- edge.constraints @ [dc]
@@ -189,9 +139,7 @@ let edge_attributes : E.t -> 'a list =
                 F.asprintf "%s : %a" (EdgeExp.call_to_string call) Location.pp loc
             | EdgeExp.CallPair.P (((_, _, _, loc1) as lb_call), ub_call) ->
                 F.asprintf "[%s; %s] : %a" (EdgeExp.call_to_string lb_call)
-                  (EdgeExp.call_to_string ub_call) Location.pp loc1
-            | _ ->
-                assert false )
+                  (EdgeExp.call_to_string ub_call) Location.pp loc1 )
       in
       Some (String.concat ~sep:"\n" call_list)
   in
@@ -222,19 +170,6 @@ let edge_attributes : E.t -> 'a list =
   let label_parts =
     [edge_label edge_data; backedge_label; local_bounds_label; calls_str; condition_norms]
   in
-  let label_parts =
-    match edge_data.edge_type with
-    | GuardedDCP ->
-        let guards =
-          Some
-            ( List.map (EdgeExp.Set.elements edge_data.guards) ~f:(fun guard ->
-                  F.asprintf "[GUARD] %s > 0" (EdgeExp.to_string guard) )
-            |> String.concat ~sep:"\n" )
-        in
-        label_parts @ [guards]
-    | DCP ->
-        label_parts
-  in
   let constraints =
     Some (List.map edge_data.constraints ~f:(fun dc -> DC.to_string dc) |> String.concat ~sep:"\n")
   in

infer/src/looper/DifferenceConstraintProgram.mli

@@ -5,21 +5,16 @@ module F = Format
 module DC = DifferenceConstraint
 module LTS = LabeledTransitionSystem
 
-(* Difference Constraint Program *)
-type edge_output_type = GuardedDCP | DCP [@@deriving compare]
-
 module EdgeData : sig
   type t =
     { backedge: bool
     ; branch_info: (Sil.if_kind * bool * Location.t) option
     ; mutable calls: EdgeExp.CallPair.Set.t
     ; mutable constraints: DC.t list
-    ; mutable guards: EdgeExp.Set.t
     ; mutable condition_norms: EdgeExp.Set.t list
     ; mutable bound: EdgeExp.T.t option
     ; mutable bound_norms: EdgeExp.Set.t list
-    ; mutable computing_bound: bool
-    ; mutable edge_type: edge_output_type }
+    ; mutable computing_bound: bool }
   [@@deriving compare]
 
   val equal : t -> t -> bool
@@ -32,17 +27,11 @@ module EdgeData : sig
 
   val is_backedge : t -> bool
 
-  val active_guards : t -> EdgeExp.Set.t
-
   (* Required by Graph module interface *)
   val default : t
 
-  val set_edge_output_type : t -> edge_output_type -> unit
-
   val branch_type : t -> bool
 
-  val add_guards : t -> EdgeExp.Set.t -> unit
-
   val add_constraint : t -> DC.t -> unit
 end
 

infer/src/looper/GraphConstructor.ml

@@ -382,7 +382,9 @@ let exec_instr :
                   (fun ptr_arg (lb, ub) acc ->
                     debug_log "Side-effect: %a  --->  [%a, %a]@," EdgeExp.pp ptr_arg EdgeExp.pp lb
                       EdgeExp.pp ub ;
-                    let arg_access = HilExp.AccessExpression.dereference_2 (extract_access ptr_arg) in
+                    let arg_access =
+                      HilExp.AccessExpression.dereference_2 (extract_access ptr_arg)
+                    in
                     let output_bound = EdgeExp.ValuePair.P (lb, ub) in
                     LTS.EdgeData.add_assignment acc arg_access output_bound )
                   call_model.side_effects graph_data.edge_data
@@ -1057,16 +1059,13 @@ let process_split_node node successors predecessors (graph_data, proc_data) =
       let prev_is_loop_head = Procdesc.is_loop_head graph_data.proc_desc prev_node in
       let current_is_loop_head = Procdesc.is_loop_head graph_data.proc_desc node in
       let node_map, loop_heads =
-        if prev_is_loop_head then (
+        if prev_is_loop_head then
           let node_map = Procdesc.NodeMap.add prev_node prune_node graph_data.node_map in
-          node_map, graph_data.loop_heads
-        ) else if current_is_loop_head then (
+          (node_map, graph_data.loop_heads)
+        else if current_is_loop_head then
           let loop_heads = prune_node :: graph_data.loop_heads in
-          Procdesc.NodeMap.add node prune_node graph_data.node_map, loop_heads
-        ) else (
-          Procdesc.NodeMap.add node prune_node graph_data.node_map, 
-          graph_data.loop_heads
-        )
+          (Procdesc.NodeMap.add node prune_node graph_data.node_map, loop_heads)
+        else (Procdesc.NodeMap.add node prune_node graph_data.node_map, graph_data.loop_heads)
       in
       let graph_data =
         { graph_data with
@@ -1357,7 +1356,7 @@ let construct : LooperSummary.t InterproceduralAnalysis.t -> procedure_data =
       let nodes = LTS.NodeSet.remove node const_nodes in
       let backedge_in_edges, in_edges =
         List.partition_tf (LTS.pred_e proc_data.lts node)
-          ~f:(fun (_, (edge_data : LTS.EdgeData.t), _) -> edge_data.backedge)
+          ~f:(fun (_, (edge_data : LTS.EdgeData.t), _) -> edge_data.backedge )
       in
       let shared_const_assignments =
         List.map in_edges ~f:(fun ((_, edge_data, _) as edge) ->
@@ -1470,7 +1469,7 @@ let construct : LooperSummary.t InterproceduralAnalysis.t -> procedure_data =
   let rec cut_branch access_edge node =
     let _, in_edges =
       List.partition_tf (LTS.pred_e proc_data.lts node)
-        ~f:(fun (_, (edge_data : LTS.EdgeData.t), _) -> edge_data.backedge)
+        ~f:(fun (_, (edge_data : LTS.EdgeData.t), _) -> edge_data.backedge )
     in
     LTS.remove_edge_e proc_data.lts access_edge ;
     if Int.equal (List.length in_edges) 1 then (

infer/src/looper/LabeledTransitionSystem.ml

@@ -171,78 +171,7 @@ module EdgeData = struct
         EdgeExp.ValuePair.V (EdgeExp.T.Access lhs_access)
 
 
-  let derive_guards edge why3_norms tenv (prover_data : Provers.prover_data) =
-    let selected_theory = prover_data.real_data in
-    let or_terms =
-      List.fold edge.conditions ~init:[] ~f:(fun or_terms and_terms ->
-          let condition_set =
-            EdgeExp.Set.fold
-              (fun cond acc ->
-                match cond with
-                | EdgeExp.T.BinOp (_, EdgeExp.T.Const _, EdgeExp.T.Const _) ->
-                    acc
-                | EdgeExp.T.UnOp _ | EdgeExp.T.BinOp _ -> (
-                  try
-                    debug_log "Transforming: %a@," EdgeExp.pp cond ;
-                    let cond_why3, type_conditions =
-                      EdgeExp.to_why3_expr cond tenv ~selected_theory prover_data
-                    in
-                    Why3.Term.Sterm.add cond_why3 (Why3.Term.Sterm.union type_conditions acc)
-                  with error ->
-                    debug_log
-                      "Failed to transform condition '%a' to Why3 expression, skipping: %a@,"
-                      EdgeExp.pp cond Exn.pp error ;
-                    acc )
-                | _ ->
-                    L.(die InternalError)
-                      "[Guards] Condition of form '%a' is not supported" EdgeExp.pp cond )
-              and_terms Why3.Term.Sterm.empty
-          in
-          if Why3.Term.Sterm.is_empty condition_set then or_terms
-          else (Why3.Term.Sterm.elements condition_set |> Why3.Term.t_and_l) :: or_terms )
-    in
-    if List.is_empty or_terms then EdgeExp.Set.empty
-    else
-      let lhs = Why3.Term.t_or_l or_terms in
-      let gt = selected_theory.get_op ">" in
-      let zero_const = selected_theory.mk_const (Why3.BigInt.of_int 0) in
-      let goal_symbol = Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "is_guard") in
-      let lhs_vars = Why3.Term.Mvs.keys (Why3.Term.t_vars lhs) in
-      let is_norm_guard why3_norm =
-        let rhs = Why3.Term.t_app_infer gt [why3_norm; zero_const] in
-        let formula = Why3.Term.t_implies lhs rhs in
-        let rhs_vars = Why3.Term.Mvs.keys (Why3.Term.t_vars rhs) in
-        let free_vars = lhs_vars @ rhs_vars in
-        let quantified_fmla = Why3.Term.t_forall_close free_vars [] formula in
-        let task = Why3.Task.use_export None selected_theory.theory in
-        let task = Why3.Task.add_prop_decl task Why3.Decl.Pgoal goal_symbol quantified_fmla in
-        let prover_call =
-          Why3.Driver.prove_task prover_data.driver task ~config:prover_data.main
-            ~command:prover_data.prover_conf.command
-            ~limit:{Why3.Call_provers.empty_limit with limit_time= 5.}
-        in
-        let result = Why3.Call_provers.wait_on_call prover_call in
-        match result.pr_answer with
-        | Why3.Call_provers.Valid ->
-            (* Implication [conditions] => [norm > 0] always holds *)
-            true
-        | Why3.Call_provers.Invalid | Why3.Call_provers.Unknown _ ->
-            false
-        | _ ->
-            debug_log "Failed task: %a\n" Why3.Pretty.print_task task ;
-            debug_log "Fail: %s\n" result.pr_output ;
-            assert false
-      in
-      let guards =
-        List.fold why3_norms ~init:EdgeExp.Set.empty ~f:(fun guard_acc (norm, why3_norm) ->
-            if is_norm_guard why3_norm then EdgeExp.Set.add norm guard_acc else guard_acc )
-      in
-      guards
-
-
   let derive_constraint edge_data (norm, used_assignments) formals tenv proc_name =
-    (* List.iter edge_data.assignments ~f:(fun (lhs, rhs) ->
-        debug_log "Assignment: %a = %a@," HilExp.AccessExpression.pp lhs EdgeExp.ValuePair.pp rhs ) ; *)
     let get_assignment lhs_access =
       debug_log "get_assignment: %a@," HilExp.AccessExpression.pp lhs_access ;
       let lhs_access_stripped =
@@ -333,25 +262,6 @@ module EdgeData = struct
                   else EdgeExp.AssignmentSet.empty
                 in
                 (accesses, Some rhs)
-              (* if
-                   (not (EdgeExp.equal norm rhs_exp))
-                   && AccessExpressionSet.mem access used_assignments
-                 then (
-                   (* debug_log "############ FAIL ###########@,"; *)
-                   (* L.die InternalError "[%a] Edge '%a = %a' assignment previously used " Procname.pp
-                      proc_name HilExp.AccessExpression.pp access EdgeExp.pp rhs *)
-                   L.user_warning
-                     "[%a] Edge '%a = %a' assignment previously used, skipping substitution...@."
-                     Procname.pp proc_name HilExp.AccessExpression.pp access EdgeExp.pp rhs ;
-                   debug_log "Returning rhs: %a@," EdgeExp.pp norm ;
-                   (AccessExpressionSet.empty, Some norm) )
-                 else
-                   let accesses =
-                     if (not (EdgeExp.equal norm rhs)) && not (EdgeExp.is_zero rhs) then
-                       AccessExpressionSet.singleton access
-                     else AccessExpressionSet.empty
-                   in
-                   (accesses, Some rhs) *)
             in
             match rhs with
             | EdgeExp.ValuePair.P (lower_bound, upper_bound) -> (

infer/src/looper/LabeledTransitionSystem.mli

@@ -66,9 +66,6 @@ module EdgeData : sig
 
   val get_assignment_rhs : t -> HilExp.access_expression -> EdgeExp.ValuePair.t
 
-  val derive_guards :
-    t -> (EdgeExp.T.t * Why3.Term.term) list -> Tenv.t -> Provers.prover_data -> EdgeExp.Set.t
-
   (* Derive difference constraint "x <= y + c" based on edge assignments *)
   val derive_constraint :
        t