Modular analysis: Collect graphs

Author: jerhard

src/analyses/base.ml

@@ -514,7 +514,7 @@ struct
     in
     List.fold_right f vals []
 
-  let rec reachable_from_value (ask: Q.ask) (gs:glob_fun) st (value: value) (t: typ) (description: string)  =
+  let rec reachable_from_value (ask: ValueDomainQueries.t) (gs:glob_fun) st (value: value) (t: typ) (description: string)  =
     let empty = AD.empty () in
     if M.tracing then M.trace "reachability" "Checking value %a\n" VD.pretty value;
     match value with
@@ -530,7 +530,7 @@ struct
       ValueDomain.Unions.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) u empty
     (* For arrays, we ask to read from an unknown index, this will cause it
      * join all its values. *)
-    | Array a -> reachable_from_value ask gs st (ValueDomain.CArrays.get (Queries.to_value_domain_ask ask) a (None, ValueDomain.ArrIdxDomain.top ())) t description
+    | Array a -> reachable_from_value ask gs st (ValueDomain.CArrays.get ask a (None, ValueDomain.ArrIdxDomain.top ())) t description
     | Blob (e,_,_) -> reachable_from_value ask gs st e t description
     | Struct s -> ValueDomain.Structs.fold (fun k v acc -> AD.join (reachable_from_value ask gs st v t description) acc) s empty
     | Int _ -> empty
@@ -545,7 +545,8 @@ struct
    * pointers. We return a flattend representation, thus simply an address (set). *)
   let reachable_from_address (ask: Q.ask) (gs:glob_fun) st (adr: address): address =
     if M.tracing then M.tracei "reachability" "Checking for %a\n" AD.pretty adr;
-    let res = reachable_from_value ask gs st (get ask gs st adr None) (AD.type_of adr) (AD.show adr) in
+    let value_domain_ask = Queries.to_value_domain_ask ask in
+    let res = reachable_from_value value_domain_ask gs st (get ask gs st adr None) (AD.type_of adr) (AD.show adr) in
     if M.tracing then M.traceu "reachability" "Reachable addresses: %a\n" AD.pretty res;
     res
 
@@ -1230,33 +1231,54 @@ struct
       Invariant.none
 
 
-  module ADGraph = MapDomain.MapBot_LiftTop (Addr) (AD)
+  let is_prefix_of m1 m2 =
+    let m1 = Addr.to_mval m1 in
+    let m2 = Addr.to_mval m2 in
+    match m1, m2 with
+    | Some m1, Some m2 -> Option.is_some (Addr.Mval.prefix m1 m2)
+    | _ -> false
 
   (* Given a set of addresses, collect graph
      that contains all paths with which these addresses are reachable with a depth-first search *)
-  let collect_graph ctx (start: AD.t) (goal: AD.t) =
-    let rec dfs node (visited, graph) : bool * ADGraph.t =
-      let node = node in
-      let visited = AD.join visited (AD.singleton node) in
-      let reachable_from_node = reachable_from_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local (AD.singleton node) in
-      let dfs_add_edge n found =
-        let goal_reached = AD.subset (AD.singleton n) goal in
-        let found, graph = dfs n (visited, graph) in
-        let found = found || goal_reached in
-        if found then
-          let graph = ADGraph.add node (AD.singleton n) graph in
-          (true, graph)
-        else
-          (found, graph)
+  let collect_graph (local: CPA.t) (start: AD.t) (goal: AD.t) =
+    if AD.is_empty start || AD.is_empty goal then
+      ValueDomain.ADGraph.bot ()
+    else
+      let ask: Queries.ask = { Queries.f = (fun (type a) (q: a Queries.t) -> Queries.Result.top q)} in
+      let state = D.top () in
+      let local = {state with cpa = local} in
+      let rec dfs node (visited, graph) : bool * ValueDomain.ADGraph.t =
+        let node = node in
+        let visited = AD.join visited (AD.singleton node) in
+        let glob_fun = fun _ -> failwith "Should not lookup globals." in
+        let reachable_from_node = reachable_from_address ask glob_fun local (AD.singleton node) in
+        let dfs_add_edge n found =
+          let goal_reached = AD.exists (fun g -> is_prefix_of n g)  goal in
+          let already_visited = AD.subset (AD.singleton n) visited in
+          if already_visited then
+            false, graph
+          else if goal_reached then
+            let graph = ValueDomain.ADGraph.add node (AD.singleton n) graph in
+            (true, graph)
+          else begin
+            let found, graph = dfs n (visited, graph) in
+            if found then
+              let graph = ValueDomain.ADGraph.add node (AD.singleton n) graph in
+              (true, graph)
+            else
+              (found, graph)
+          end
+        in
+        AD.fold dfs_add_edge reachable_from_node (false, ValueDomain.ADGraph.bot ())
       in
-      AD.fold dfs_add_edge reachable_from_node (false, ADGraph.bot ())
-    in
-    let dfs_combine node graph =
-      let _, graph = dfs node (AD.empty (), graph) in
-      graph
-    in
-    let empty_graph = ADGraph.empty () in
-    AD.fold dfs_combine start empty_graph
+      let dfs_combine node graph =
+        let _, graph = dfs node (AD.empty (), graph) in
+        graph
+      in
+      let empty_graph = ValueDomain.ADGraph.empty () in
+      let result = AD.fold dfs_combine start empty_graph in
+      if M.tracing then M.tracel "collect_graph" "From %a to %a, in graph %a\n" AD.pretty start AD.pretty goal ValueDomain.ADGraph.pretty result;
+      result
 
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
@@ -1442,6 +1464,8 @@ struct
       query_invariant_global ctx g
     | Q.BaseCPA ->
       ctx.local.cpa
+    | Q.CollectGraph (cpa,start, goal) ->
+      collect_graph cpa start goal
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =
@@ -1916,9 +1940,10 @@ struct
    **************************************************************************)
 
   (** From a list of expressions, collect a list of addresses that they might point to, or contain pointers to. *)
-  let collect_funargs ask ?(warn=false) (gs:glob_fun) (st:store) (exps: exp list) =
+  let collect_funargs (ask: Q.ask) ?(warn=false) (gs:glob_fun) (st:store) (exps: exp list) =
+    let value_domain_ask = Queries.to_value_domain_ask ask in
     let do_exp e =
-      let immediately_reachable = reachable_from_value ask gs st (eval_rv ask gs st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in
+      let immediately_reachable = reachable_from_value value_domain_ask gs st (eval_rv ask gs st e) (Cilfacade.typeOf e) (CilType.Exp.show e) in
       reachable_vars ask [immediately_reachable] gs st
     in
     List.concat_map do_exp exps

src/analyses/startStateAnalysis.ml

@@ -16,16 +16,18 @@ struct
     let ask = Analyses.ask_of_ctx ctx in
     let cpa = ask.f Queries.BaseCPA in
     ctx.sideg f cpa;
+    if Messages.tracing then Messages.tracel "startstate" "For %a, side-effecting state %a \n" CilType.Fundec.pretty f G.pretty cpa;
     ()
 
   let name () = "startstate"
 
-  let is_modular () = true
+  let modular_support () = Modular
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | Queries.StartCPA f ->
       let r : G.t = ctx.global f in
+      if Messages.tracing then Messages.tracel "startstate" "For %a, startstate analysis answering: %a\n" CilType.Fundec.pretty f G.pretty r;
       r
     | _ -> Queries.Result.top q
 

src/analyses/written.ml

@@ -15,6 +15,11 @@ struct
   (* Value of entries not in mapping: bot, LiftTop such that there is a `Top map. *)
   module D = WrittenDomain.Written
   module C = Lattice.Unit
+  module V = struct
+    include CilType.Fundec
+    let is_write_only _ = false
+  end
+  module G = ValueDomain.ADGraph
 
   let context _ _ = C.bot ()
 
@@ -38,7 +43,20 @@ struct
   let body ctx (f:fundec) : D.t =
     ctx.local
 
+  let join_address_list (a : AD.t list) =
+    List.fold AD.join (AD.bot ()) a
+
   let return ctx (exp:exp option) (f:fundec) : D.t =
+    let ask = Analyses.ask_of_ctx ctx in
+    let start_state = ask.f (Queries.StartCPA f) in
+    let written = List.map Tuple2.first (D.bindings ctx.local) in
+    let written = join_address_list written in
+    let params = f.sformals in
+    let params = List.map (AD.of_var ~is_modular:true) params in
+    let params = join_address_list params in
+    let graph = ask.f (CollectGraph (start_state, params, written)) in (* TODO: Adapt start and end sets *)
+    M.tracel "startstate" "Looking for path from %a to %a in state %a\n" AD.pretty params AD.pretty written BaseDomain.CPA.pretty start_state;
+    ctx.sideg f graph;
     ctx.local
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
@@ -98,4 +116,5 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  let dep = ["startstate"] in
+  MCP.register_analysis ~dep (module Spec : MCPSpec)

src/cdomain/value/cdomains/valueDomain.ml

@@ -1477,3 +1477,5 @@ let invariant_global find g =
   in
   let module I = ValueInvariant (Arg) in
   I.key_invariant g (find g)
+
+module ADGraph = MapDomain.MapBot_LiftTop (Addr) (AD)

src/domains/queries.ml

@@ -135,6 +135,7 @@ type _ t =
   | IsModular: MustBool.t t
   | BaseCPA: BaseDomain.CPA.t t
   | StartCPA: CilType.Fundec.t -> BaseDomain.CPA.t t
+  | CollectGraph: BaseDomain.CPA.t * AD.t * AD.t -> ValueDomain.ADGraph.t t
 
 type 'a result = 'a
 
@@ -212,6 +213,7 @@ struct
     | TmpSpecial _ -> (module ML)
     | BaseCPA -> (module BaseDomain.CPA)
     | StartCPA _ -> (module BaseDomain.CPA)
+    | CollectGraph _ -> (module ValueDomain.ADGraph)
 
   (** Get bottom result for query. *)
   let bot (type a) (q: a t): a result =
@@ -288,6 +290,7 @@ struct
     | TmpSpecial _ -> ML.top ()
     | BaseCPA -> BaseDomain.CPA.top ()
     | StartCPA _ -> BaseDomain.CPA.top ()
+    | CollectGraph _ -> ValueDomain.ADGraph.top ()
 end
 
 (* The type any_query can't be directly defined in Any as t,
@@ -361,6 +364,7 @@ struct
     | Any Read -> 63
     | Any BaseCPA -> 64
     | Any (StartCPA _) -> 65
+    | Any (CollectGraph _) -> 66
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -417,6 +421,17 @@ struct
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
       | Any (StartCPA f1), Any (StartCPA f2) -> CilType.Fundec.compare f1 f2
+      | Any (CollectGraph (c, a1, b1)), Any (CollectGraph (c2, a2, b2)) ->
+        let r = BaseDomain.CPA.compare c c2 in
+        if r <> 0 then
+          r
+        else begin
+          let r = AD.compare a1 a2 in
+          if r <> 0 then
+            r
+          else
+            AD.compare b1 b2
+        end
       (* only argumentless queries should remain *)
       | _, _ -> Stdlib.compare (order a) (order b)
 
@@ -530,6 +545,7 @@ struct
     | Any IsModular -> Pretty.dprintf "IsModular"
     | Any BaseCPA -> Pretty.dprintf "BaseCPA"
     | Any (StartCPA f) -> Pretty.dprintf "StartCPA %a" CilType.Fundec.pretty f
+    | Any (CollectGraph (c, s, g)) -> Pretty.dprintf "CollectGraph (%a, %a, %a)" BaseDomain.CPA.pretty c AD.pretty s AD.pretty g
 end
 
 let to_value_domain_ask (ask: ask) =

tests/regression/79-modular/63-simple-int.c

@@ -0,0 +1,33 @@
+//PARAM: --enable modular --enable ana.modular.auto-funs --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'" --set ana.activated[+] "'used_globals'" --set ana.activated[+] "'startstate'"
+#include <stdlib.h>
+
+int foo(int *p){
+	*p = 23;
+	return 0;
+}
+
+struct node {
+	struct node* next;
+	int value;
+};
+
+int modify_node_ptr(struct node** n){
+	*n = NULL;
+	return 0;
+}
+
+int modify_node_ptr_indirect(struct node** n){
+	(*n)->next = NULL;
+	return 0;
+}
+
+
+int modify_node(struct node* n){
+	n->next = NULL;
+	return 0;
+}
+
+int modify_node_indirect(struct node* n){
+	n->next->next = NULL;
+	return 0;
+}