Add option ana.modular.auto-funs to automatically detect which functi…

…ons should be analyzed modularly.

src/analyses/base.ml

@@ -3071,7 +3071,7 @@ let after_config () =
   (* add ~dep:["expRelation"] after modifying test cases accordingly *)
   let dep =
     let base_dependencies = ["mallocWrapper"] in
-    let modular_dependencies = if is_any_modular () then ["modular_queries"; "is_modular"; "written"; "used_globals"] else [] in
+    let modular_dependencies = if get_bool "modular" then ["modular_queries"; "is_modular"; "written"; "used_globals"] else [] in
     base_dependencies @ modular_dependencies
   in
   MCP.register_analysis ~dep (module Main : MCPSpec)

src/common/util/cilfacade.ml

@@ -155,12 +155,40 @@ let is_exit = in_section (fun s -> s = ".exit.text")
 
 type startfuns = fundec list * fundec list * fundec list
 
+module VarinfoH = Hashtbl.Make (CilType.Varinfo)
+
+let varinfo_fundecs: fundec VarinfoH.t ResettableLazy.t =
+  ResettableLazy.from_fun (fun () ->
+      let h = VarinfoH.create 111 in
+      iterGlobals !current_file (function
+          | GFun (fd, _) ->
+            VarinfoH.replace h fd.svar fd
+          | _ -> ()
+        );
+      h
+    )
+
+(** Find [fundec] by the function's [varinfo] (has the function name and type). *)
+let find_varinfo_fundec vi = VarinfoH.find (ResettableLazy.force varinfo_fundecs) vi (* vi argument must be explicit, otherwise force happens immediately *)
+
+let find_varinfo_fundec_option f =
+  match find_varinfo_fundec f with
+  | v -> Some v
+  | exception Not_found -> None
+
+
+module StringSet = BatSet.Make (String)
 let getFuns fileAST : startfuns =
   let add_main f (m,e,o) = (f::m,e,o) in
   let add_exit f (m,e,o) = (m,f::e,o) in
   let add_other f (m,e,o) = (m,e,f::o) in
-  let modular_funs = get_string_list "ana.modular.funs" in
-  let only_modular_funs = get_bool "modular" && not (modular_funs = []) in
+
+  let modular_funs = StringSet.of_list (get_string_list "ana.modular.funs") in
+  ModularHeuristics.compute_auto_modular_funs find_varinfo_fundec_option fileAST;
+  let auto_modular_functions = ModularHeuristics.auto_modular_funs () in
+  let modular_funs = StringSet.union modular_funs auto_modular_functions in
+  let only_modular_funs = get_bool "ana.modular.only" in
+
   let f acc glob =
     match glob with
     | GFun({svar={vname=mn; _}; _} as def,_) when List.mem mn (get_string_list "mainfun") && not only_modular_funs -> add_main def acc
@@ -172,7 +200,7 @@ let getFuns fileAST : startfuns =
       Printf.printf "Cleanup function: %s\n" mn; set_string "exitfun[+]" mn; add_exit def acc
     | GFun ({svar={vstorage=NoStorage; vattr; _}; _} as def, _) when get_bool "nonstatic" && not (Cil.hasAttribute "goblint_stub" vattr) -> add_other def acc
     | GFun ({svar={vattr; _}; _} as def, _) when get_bool "allfuns" && not (Cil.hasAttribute "goblint_stub" vattr) ->  add_other def  acc
-    | GFun ({svar={vattr; vname; _}; _} as def, _) when (get_bool "modular" && (not only_modular_funs || List.mem vname modular_funs))  && not (Cil.hasAttribute "goblint_stub" vattr) ->  add_main def  acc
+    | GFun ({svar={vattr; vname; _}; _} as def, _) when (get_bool "modular" && StringSet.mem vname modular_funs)  && not (Cil.hasAttribute "goblint_stub" vattr) -> add_main def acc
     | _ -> acc
   in
   foldGlobals fileAST f ([],[],[])
@@ -542,22 +570,6 @@ let find_stmt_fundec stmt =
   with Not_found -> StmtH.find (ResettableLazy.force stmt_fundecs) stmt (* stmt argument must be explicit, otherwise force happens immediately *)
 
 
-module VarinfoH = Hashtbl.Make (CilType.Varinfo)
-
-let varinfo_fundecs: fundec VarinfoH.t ResettableLazy.t =
-  ResettableLazy.from_fun (fun () ->
-      let h = VarinfoH.create 111 in
-      iterGlobals !current_file (function
-          | GFun (fd, _) ->
-            VarinfoH.replace h fd.svar fd
-          | _ -> ()
-        );
-      h
-    )
-
-(** Find [fundec] by the function's [varinfo] (has the function name and type). *)
-let find_varinfo_fundec vi = VarinfoH.find (ResettableLazy.force varinfo_fundecs) vi (* vi argument must be explicit, otherwise force happens immediately *)
-
 
 module StringH = Hashtbl.Make (Printable.Strings)
 

src/common/util/modularHeuristics.ml

@@ -0,0 +1,98 @@
+open GoblintCil
+
+let contains_function_call_through_pointer (f : fundec) : bool =
+  let contains_call = ref false in
+  let visitor = object
+    inherit nopCilVisitor
+
+    method! vinst (i : instr) : instr list visitAction =
+      match i with
+      | Call (_, Lval (Mem _, _), _, _, _)  ->
+        (* TODO: Does this detect all calls via function pointer? *)
+        contains_call := true;
+        SkipChildren
+      (* Detect static call of pthread_create: *)
+      | Call (_, Lval (Var fptr, _), _, _, _) when fptr.vname = "pthread_create" ->
+        contains_call := true;
+        SkipChildren
+      | _ -> DoChildren
+  end in
+  ignore (visitCilFunction visitor f);
+  let result = !contains_call in
+  Printf.printf "contains_function_call_through_pointer: %s -> %b\n" f.svar.vname result;
+  result
+
+let collect_functions_without_call_through_pointers (file : file) : fundec list =
+  let functions_without_call_through_pointers = ref [] in
+  let visitor = object
+    inherit nopCilVisitor
+
+    method! vfunc (f : fundec) : fundec visitAction =
+      if not (contains_function_call_through_pointer f) then
+        functions_without_call_through_pointers := f :: !functions_without_call_through_pointers;
+      SkipChildren
+  end in
+  visitCilFile visitor file;
+  !functions_without_call_through_pointers
+
+let get_called_functions (f : Cil.fundec) : Cil.varinfo list =
+  let called_functions = ref [] in
+  let visitor = object
+    inherit nopCilVisitor
+
+    method! vinst (i : Cil.instr) : Cil.instr list visitAction =
+      match i with
+      | Call (_, Lval (Var fptr, _), _, _, _) when isFunctionType fptr.vtype ->
+        called_functions := fptr :: !called_functions;
+        SkipChildren
+      | _ -> DoChildren
+  end in
+  ignore (visitCilFunction visitor f);
+  !called_functions
+
+
+(* TODO: Mark function that are passed to pthread_create as non-modular, or automatically analyze them non-modularly if they are created as threads *)
+let collect_functions_without_function_pointers (find_varinfo_fundec) (file : Cil.file) : Cil.fundec list =
+  let functions_without_call_through_pointers = collect_functions_without_call_through_pointers file in
+  Printf.printf "functions_without_call_through_pointers: %s\n" (String.concat ", " (List.map (fun f -> f.svar.vname) functions_without_call_through_pointers));
+  let only_good_callees (f: fundec) : bool =
+    let callees = get_called_functions f in
+    let callees = (List.map find_varinfo_fundec) callees in
+    Printf.printf "callees: %s\n" (String.concat ", " (List.map (fun f -> BatOption.map_default  (fun f -> f.svar.vname) "None" f) callees));
+    let is_good g = match g with
+      | None ->
+        (* Assume unknown functions do not spawn / execute function pointers *)
+        true
+      | Some g ->
+        List.mem g functions_without_call_through_pointers
+    in
+    let result = List.for_all is_good callees in
+    Printf.printf "only_good_callees: %s -> %b\n" f.svar.vname result;
+    result
+  in
+  let result = List.filter only_good_callees functions_without_call_through_pointers in
+  Printf.printf "functions_without_function_pointers: %s\n" (String.concat ", " (List.map (fun f -> f.svar.vname) result));
+  result
+
+module StringSet = BatSet.Make(String)
+
+let auto_modular_funs = ref None
+
+let compute_auto_modular_funs (find_varinfo_fundec) (file : Cil.file) : unit =
+  let compute_and_set () =
+    let functions_without_function_pointers = collect_functions_without_function_pointers find_varinfo_fundec file in
+    let funs = List.map (fun f -> f.svar.vname) functions_without_function_pointers in
+    let funs = StringSet.of_list funs in
+    auto_modular_funs := Some funs
+  in
+  let set_to_empty () =
+    auto_modular_funs := Some StringSet.empty
+  in
+  if GobConfig.get_bool "ana.modular.auto-funs" then
+    compute_and_set ()
+  else
+    set_to_empty ()
+
+let auto_modular_funs () = match !auto_modular_funs with
+  | None -> failwith "auto_modular_functions not initialized"
+  | Some f -> f

src/common/util/options.schema.json

@@ -373,6 +373,20 @@
                 "type": "string"
               },
               "default": []
+            },
+            "auto-funs": {
+              "title": "ana.modular.auto-funs",
+              "description":
+                "Automatically detect functions that are to be analayzed modularly.",
+              "type": "boolean",
+              "default": false
+            },
+            "only": {
+              "title": "ana.modular.only",
+              "description":
+                "Only analyze functions that are to be analayzed modularly.",
+              "type": "boolean",
+              "default": false
             }
           },
           "additionalProperties": false

src/util/modularUtil0.ml

@@ -23,6 +23,9 @@ let modular_funs () = match !modular_funs with
   | None ->
     let funs = get_string_list "ana.modular.funs" in
     let funs = StringSet.of_list funs in
+    let auto_funs = ModularHeuristics.auto_modular_funs () in
+
+    let funs = StringSet.union funs auto_funs in
     modular_funs := Some funs;
     funs
   | Some funs ->
@@ -32,10 +35,10 @@ let is_modular_fun f =
   let is_modular_fun f =
     StringSet.mem f (modular_funs ())
   in
-  is_modular () || is_modular_fun f.vname
+  is_modular_fun f.vname
 
 let is_any_modular () =
-  is_modular () || not (StringSet.is_empty (modular_funs ()))
+  not (StringSet.is_empty (modular_funs ()))
 
 (** If [x] is global (but not a heap variable) and we are in ["modular"] mode, retrieves the varinfo_to_canonical for [x], else returns [x] itself *)
 let varinfo_or_canonical ~is_modular x =

tests/regression/79-modular/01-modular.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 
 #include <goblint.h>
 

tests/regression/79-modular/02-start-state.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include <goblint.h>
 
 typedef struct node {

tests/regression/79-modular/03-heap-blocks-non-unique.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include <goblint.h>
 #include <stdlib.h>
 

tests/regression/79-modular/04-heap-pointers_maybe_null.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include <goblint.h>
 #include <stdlib.h>
 

tests/regression/79-modular/06-global_values.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include<goblint.h>
 #include<stdlib.h>
 

tests/regression/79-modular/07-global_addresses.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include<goblint.h>
 
 typedef struct node {

tests/regression/79-modular/08-global_addresses_and_values.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include<goblint.h>
 #include<stdlib.h>
 

tests/regression/79-modular/09-function-calls.c

@@ -1,4 +1,4 @@
-//PARAM: --set ana.modular.funs "['modify_x', 'modify_y']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//PARAM: --enable modular --set ana.modular.funs "['modify_x', 'modify_y']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
 #include<goblint.h>
 
 #define X_VALUE 12

tests/regression/79-modular/10-shared-block-vals-top.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 
 typedef struct {
     int x;

tests/regression/79-modular/13-lists.c

@@ -1,4 +1,4 @@
-//PARAM: --set ana.modular.funs "['prepend', 'prepend2']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//PARAM: --enable modular --set ana.modular.funs "['prepend', 'prepend2']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
 #include<goblint.h>
 #include<stdlib.h>
 

tests/regression/79-modular/14-recursion.c

@@ -1,4 +1,4 @@
-//PARAM: --set ana.modular.funs "['fib']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//PARAM: --enable modular --set ana.modular.funs "['fib']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
 
 #include<goblint.h>
 

tests/regression/79-modular/15-return.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'" --enable ana.int.interval
+//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'" --enable ana.int.interval
 
 #include<goblint.h>
 #include<stdlib.h>

tests/regression/79-modular/16-return-local-pointer.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 
 int *identity(int *p){
 	return p;

tests/regression/79-modular/17-call-modifying-function.c

@@ -1,4 +1,4 @@
-//PARAM: --set ana.modular.funs "['change_param', 'call_change_param']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//PARAM: --enable modular --set ana.modular.funs "['change_param', 'call_change_param']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
 #include<stdlib.h>
 
 void change_param(int* p){

tests/regression/79-modular/18-non-pointers.c

@@ -1,4 +1,4 @@
-//PARAM: --set ana.modular.funs "['write_into_array']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//PARAM: --enable modular --set ana.modular.funs "['write_into_array']" --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
 
 void write_into_array(int *a, int value){
 	*a = value;

tests/regression/79-modular/19-arrays.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 
 void write_into_array(int *a, int size){
 	a[size - 1] = 123;

tests/regression/79-modular/20-arrays-top.c

@@ -1,4 +1,4 @@
-//SKIP PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//SKIP 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'"
 #include <stdlib.h>
 #include <goblint.h>
 

tests/regression/79-modular/21-call-global-modifying-function.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include<stdlib.h>
 #include<goblint.h>
 

tests/regression/79-modular/22-call-global-modifying-function-with-ptr.c

@@ -1,4 +1,4 @@
-//PARAM: --enable modular --set ana.activated[+] "'modular_queries'" --set ana.activated[+] "'is_modular'" --set ana.activated[+] "'written'" --set ana.activated[+] "'read'"  --set ana.activated[+] "'used_globals'"
+//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'"
 #include<stdlib.h>
 #include<goblint.h>