Merge pull request #1063 from goblint/evalfun-ptranal

Add CIL's ptranal for `EvalFunvar` queries

Author: sim642

src/analyses/ptranalAnalysis.ml

@@ -0,0 +1,31 @@
+(** CIL's {!GoblintCil.Ptranal} for function pointer evaluation ([ptranal]).
+
+    Useful for sound analysis of function pointers without base. *)
+
+(* TODO: fix unsoundness on some bench repo examples: https://github.com/goblint/analyzer/pull/1063 *)
+
+open GoblintCil
+open Analyses
+
+module Spec =
+struct
+  include UnitAnalysis.Spec
+
+  let name () = "ptranal"
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | Queries.EvalFunvar (Lval (Mem e, _)) ->
+      let funs = Ptranal.resolve_exp e in
+      (* TODO: filter compatible function pointers by type? *)
+      List.fold_left (fun xs f -> Queries.AD.add (Queries.AD.Addr.of_var f) xs) (Queries.AD.empty ()) funs
+    | _ -> Queries.Result.top q
+
+  let init _: unit =
+    Ptranal.analyze_file !Cilfacade.current_file;
+    Ptranal.compute_results false
+
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/goblint_lib.ml

@@ -164,6 +164,7 @@ module TaintPartialContexts = TaintPartialContexts
 module UnassumeAnalysis = UnassumeAnalysis
 module ExpRelation = ExpRelation
 module AbortUnless = AbortUnless
+module PtranalAnalysis = PtranalAnalysis
 
 
 (** {1 Domains}

tests/regression/33-constants/05-fun_ptranal.c

@@ -0,0 +1,14 @@
+//PARAM: --set ana.activated '["constants", "ptranal"]'
+// intentional explicit ana.activated to do tutorial in isolation
+int f(int a, int b){
+    int d = 3;
+    int z = a + d;
+    return z;
+}
+
+int main(){
+    int d = 0;
+    int (*fp)(int,int) = &f;
+    d = fp(2, 3);
+    return 0;
+}