[cost] Simplifications

Reviewed By: sblackshear

Differential Revision: D7774956

fbshipit-source-id: bb66803

infer/src/checkers/control.ml

@@ -73,7 +73,7 @@ module TransferFunctionsDataDeps (CFG : ProcCfg.S) = struct
 
 
   let pp_session_name node fmt =
-    F.fprintf fmt "data depenedency analysis %a" CFG.pp_id (CFG.id node)
+    F.fprintf fmt "data dependency analysis %a" CFG.pp_id (CFG.id node)
 end
 
 module ControlDepSet = VarSet
@@ -115,7 +115,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct
 
 
   let pp_session_name node fmt =
-    F.fprintf fmt "control depenedency analysis %a" CFG.pp_id (CFG.id node)
+    F.fprintf fmt "control dependency analysis %a" CFG.pp_id (CFG.id node)
 end
 
 module CFG = ProcCfg.Normal

infer/src/checkers/cost.ml

@@ -371,8 +371,8 @@ return the addends of the sum x_j1+x_j2+..+x_j_n*)
     type t = Node.id * Node.IdSet.t [@@deriving compare]
   end)
 
-  let rec minimum_propagation (bound_map: BoundMap.t) (q: Node.id) (visited: Node.IdSet.t)
+  let minimum_propagation (bound_map: BoundMap.t) (constraints: StructuralConstraints.t list) self
-      (constraints: StructuralConstraints.t list) global_built_tree_map =
+      ((q, visited): Node.id * Node.IdSet.t) =
     let rec build_min node branch visited_acc worklist =
       match worklist with
       | [] ->
@@ -398,44 +398,50 @@ return the addends of the sum x_j1+x_j2+..+x_j_n*)
             in
             build_min node branch visited_acc' worklist'
     in
-    match BuiltTreeMap.find_opt (q, visited) !global_built_tree_map with
+    let node, branch, visited_res = build_min (Min []) SetOfSetsOfNodes.empty visited [q] in
-    | Some tree ->
+    SetOfSetsOfNodes.fold
-        tree
+      (fun addend i_node ->
-    | None ->
+        if Node.IdSet.cardinal addend < 2 then assert false
-        let node, branch, visited_res = build_min (Min []) SetOfSetsOfNodes.empty visited [q] in
+        else (
-        SetOfSetsOfNodes.fold
+          L.(debug Analysis Medium) "@\n\n|Set addends| = %i  {" (Node.IdSet.cardinal addend) ;
-          (fun addend i_node ->
+          Node.IdSet.iter (fun e -> L.(debug Analysis Medium) " %a, " Node.pp_id e) addend ;
-            if Node.IdSet.cardinal addend < 2 then assert false
+          L.(debug Analysis Medium) " }@\n " ) ;
-            else (
+        let plus_node =
-              L.(debug Analysis Medium) "@\n\n|Set addends| = %i  {" (Node.IdSet.cardinal addend) ;
+          Node.IdSet.fold
-              Node.IdSet.iter (fun e -> L.(debug Analysis Medium) " %a, " Node.pp_id e) addend ;
+            (fun n acc ->
-              L.(debug Analysis Medium) " }@\n " ) ;
+              let child = self (n, visited_res) in
-            let plus_node =
+              add_child acc child )
-              Node.IdSet.fold
+            addend (Plus [])
-                (fun n acc ->
+        in
-                  let child =
+        (* without this check it would add plus node with just one child, and give wrong results *)
-                    minimum_propagation bound_map n visited_res constraints global_built_tree_map
+        if is_well_formed_plus_node plus_node then add_child i_node plus_node else i_node )
-                  in
+      branch node
-                  global_built_tree_map :=
-                    BuiltTreeMap.add (n, visited_res) child !global_built_tree_map ;
-                  add_child acc child )
-                addend (Plus [])
-            in
-            (* without this check it would add plus node with just one child, and give wrong results *)
-            if is_well_formed_plus_node plus_node then add_child i_node plus_node else i_node )
-          branch node
 
 
-  let compute_trees_from_contraints bound_map node_cfg constraints =
+  let with_cache f =
     (* a map used for bookkeeping of the min trees that we have already built *)
     let global_built_tree_map : mt_node BuiltTreeMap.t ref = ref BuiltTreeMap.empty in
+    let rec f_with_cache x =
+      match BuiltTreeMap.find_opt x !global_built_tree_map with
+      | Some v ->
+          v
+      | None ->
+          let v = f f_with_cache x in
+          global_built_tree_map := BuiltTreeMap.add x v !global_built_tree_map ;
+          v
+    in
+    Staged.stage f_with_cache
+
+
+  let compute_trees_from_contraints bound_map node_cfg constraints =
+    let minimum_propagation =
+      with_cache (minimum_propagation bound_map constraints) |> Staged.unstage
+    in
     let min_trees =
       List.fold
         ~f:(fun acc node ->
           let nid = Node.id node in
-          let tree =
+          let tree = minimum_propagation (nid, Node.IdSet.empty) in
-            minimum_propagation bound_map nid Node.IdSet.empty constraints global_built_tree_map
-          in
           (nid, tree) :: acc )
         ~init:[] (NodeCFG.nodes node_cfg)
     in
@@ -615,15 +621,11 @@ let checker {Callbacks.tenv; summary; proc_desc} : Specs.summary =
       ~init:Node.IdMap.empty min_trees
   in
   let initWCET = (Itv.Bound.zero, ReportedOnNodes.empty) in
-  let invariant_map_WCETFinal =
+  match
-    (* Final map with nodes cost *)
+    AnalyzerWCET.compute_post
-    AnalyzerWCET.exec_cfg instr_cfg
       (ProcData.make proc_desc tenv
          {basic_cost_map= invariant_map_NodesBasicCost; min_trees_map= trees_valuation; summary})
-      ~initial:initWCET ~debug:true
+      ~debug:true ~initial:initWCET
-  in
-  match
-    AnalyzerWCET.extract_post (InstrCFG.id (InstrCFG.exit_node instr_cfg)) invariant_map_WCETFinal
   with
   | Some (exit_cost, _) ->
       L.internal_error "  PROCEDURE COST = %a @\n" Itv.Bound.pp exit_cost ;