C-2PO: Thesis About a Weakly-Relational Pointer Analysis

conf/svcomp-no-var-eq.json

@@ -0,0 +1,145 @@
+{
+    "ana": {
+      "sv-comp": {
+        "enabled": true,
+        "functions": true
+      },
+      "int": {
+        "def_exc": true,
+        "enums": false,
+        "interval": true
+      },
+      "float": {
+        "interval": true
+      },
+      "activated": [
+        "base",
+        "threadid",
+        "threadflag",
+        "threadreturn",
+        "mallocWrapper",
+        "mutexEvents",
+        "mutex",
+        "access",
+        "race",
+        "escape",
+        "expRelation",
+        "mhp",
+        "assert",
+        "symb_locks",
+        "region",
+        "thread",
+        "threadJoins"
+      ],
+      "path_sens": [
+        "mutex",
+        "malloc_null",
+        "uninit",
+        "expsplit",
+        "activeSetjmp",
+        "memLeak",
+        "threadflag"
+      ],
+      "context": {
+        "widen": false
+      },
+      "malloc": {
+        "wrappers": [
+          "kmalloc",
+          "__kmalloc",
+          "usb_alloc_urb",
+          "__builtin_alloca",
+          "kzalloc",
+
+          "ldv_malloc",
+
+          "kzalloc_node",
+          "ldv_zalloc",
+          "kmalloc_array",
+          "kcalloc",
+
+          "ldv_xmalloc",
+          "ldv_xzalloc",
+          "ldv_calloc",
+          "ldv_kzalloc"
+        ]
+      },
+      "base": {
+        "arrays": {
+          "domain": "partitioned"
+        }
+      },
+      "race": {
+        "free": false,
+        "call": false
+      },
+      "autotune": {
+        "enabled": true,
+        "activated": [
+          "singleThreaded",
+          "mallocWrappers",
+          "noRecursiveIntervals",
+          "enums",
+          "congruence",
+          "octagon",
+          "wideningThresholds",
+          "loopUnrollHeuristic",
+          "memsafetySpecification",
+          "termination",
+          "tmpSpecialAnalysis"
+        ]
+      }
+    },
+    "exp": {
+      "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+      "unknown_function": {
+        "spawn": false
+      },
+      "int": {
+        "signed_overflow": "assume_none"
+      },
+      "null-pointer": {
+        "dereference": "assume_none"
+      }
+    },
+    "witness": {
+      "graphml": {
+        "enabled": true,
+        "id": "enumerate",
+        "unknown": false
+      },
+      "yaml": {
+        "enabled": true,
+        "format-version": "2.0",
+        "entry-types": [
+          "invariant_set"
+        ],
+        "invariant-types": [
+          "loop_invariant"
+        ]
+      },
+      "invariant": {
+        "loop-head": true,
+        "after-lock": false,
+        "other": false,
+        "accessed": false,
+        "exact": true,
+        "exclude-vars": [
+          "tmp\\(___[0-9]+\\)?",
+          "cond",
+          "RETURN",
+          "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+          ".*____CPAchecker_TMP_[0-9]+",
+          "__VERIFIER_assert__cond",
+          "__ksymtab_.*",
+          "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+        ]
+      }
+    },
+    "pre": {
+      "enabled": false
+    }
+  }

conf/svcomp-wrpointer.json

@@ -0,0 +1,148 @@
+{
+    "ana": {
+      "sv-comp": {
+        "enabled": true,
+        "functions": true
+      },
+      "int": {
+        "def_exc": true,
+        "enums": false,
+        "interval": true
+      },
+      "float": {
+        "interval": true
+      },
+      "activated": [
+        "base",
+        "threadid",
+        "threadflag",
+        "threadreturn",
+        "mallocWrapper",
+        "mutexEvents",
+        "mutex",
+        "access",
+        "race",
+        "escape",
+        "expRelation",
+        "mhp",
+        "assert",
+        "symb_locks",
+        "region",
+        "thread",
+        "threadJoins",
+        "wrpointer",
+        "startState",
+        "taintPartialContexts"
+      ],
+      "path_sens": [
+        "mutex",
+        "malloc_null",
+        "uninit",
+        "expsplit",
+        "activeSetjmp",
+        "memLeak",
+        "threadflag"
+      ],
+      "context": {
+        "widen": false
+      },
+      "malloc": {
+        "wrappers": [
+          "kmalloc",
+          "__kmalloc",
+          "usb_alloc_urb",
+          "__builtin_alloca",
+          "kzalloc",
+
+          "ldv_malloc",
+
+          "kzalloc_node",
+          "ldv_zalloc",
+          "kmalloc_array",
+          "kcalloc",
+
+          "ldv_xmalloc",
+          "ldv_xzalloc",
+          "ldv_calloc",
+          "ldv_kzalloc"
+        ]
+      },
+      "base": {
+        "arrays": {
+          "domain": "partitioned"
+        }
+      },
+      "race": {
+        "free": false,
+        "call": false
+      },
+      "autotune": {
+        "enabled": true,
+        "activated": [
+          "singleThreaded",
+          "mallocWrappers",
+          "noRecursiveIntervals",
+          "enums",
+          "congruence",
+          "octagon",
+          "wideningThresholds",
+          "loopUnrollHeuristic",
+          "memsafetySpecification",
+          "termination",
+          "tmpSpecialAnalysis"
+        ]
+      }
+    },
+    "exp": {
+      "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+      "unknown_function": {
+        "spawn": false
+      },
+      "int": {
+        "signed_overflow": "assume_none"
+      },
+      "null-pointer": {
+        "dereference": "assume_none"
+      }
+    },
+    "witness": {
+      "graphml": {
+        "enabled": true,
+        "id": "enumerate",
+        "unknown": false
+      },
+      "yaml": {
+        "enabled": true,
+        "format-version": "2.0",
+        "entry-types": [
+          "invariant_set"
+        ],
+        "invariant-types": [
+          "loop_invariant"
+        ]
+      },
+      "invariant": {
+        "loop-head": true,
+        "after-lock": false,
+        "other": false,
+        "accessed": false,
+        "exact": true,
+        "exclude-vars": [
+          "tmp\\(___[0-9]+\\)?",
+          "cond",
+          "RETURN",
+          "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+          ".*____CPAchecker_TMP_[0-9]+",
+          "__VERIFIER_assert__cond",
+          "__ksymtab_.*",
+          "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+        ]
+      }
+    },
+    "pre": {
+      "enabled": false
+    }
+  }

src/analyses/startStateAnalysis.ml

@@ -0,0 +1,85 @@
+(** Remembers the abstract address value of each parameter at the beginning of each function by adding a ghost variable for each parameter.
+    Used by the wrpointer anaylysis. *)
+
+open GoblintCil
+open Batteries
+open Analyses
+
+
+(*First all parameters (=formals) of the function are duplicated (by negating their ID),
+    then we remember the value of each local variable at the beginning of the function
+  in this new duplicated variable. *)
+module Spec : Analyses.MCPSpec =
+struct
+  let name () = "startState"
+  module VD = BaseDomain.VD
+  module AD = ValueDomain.AD
+  module Value = AD
+  module D = MapDomain.MapBot (Basetype.Variables) (Value)
+  module C = D
+
+  include Analyses.IdentitySpec
+
+
+  let duplicated_variable var = { var with vid = - var.vid - 4; vname = "wrpointer__" ^ var.vname ^ "'" }
+  let original_variable var = { var with vid = - (var.vid + 4); vname = String.lchop ~n:11 @@ String.rchop var.vname }
+  let return_varinfo = {dummyFunDec.svar with vid=(-2);vname="wrpointer__@return"}
+  let is_wrpointer_ghost_variable x = x.vid < 0 && String.starts_with x.vname "wrpointer__"
+
+
+  let get_value (ask: Queries.ask) exp = ask.f (MayPointTo exp)
+
+  (** If e is a known variable, then it returns the value for this variable.
+      If e is &x' for a duplicated variable x' of x, then it returns MayPointTo of &x.
+      If e is an unknown variable or an expression that is not simply a variable, then it returns top. *)
+  let eval (ask: Queries.ask) (d: D.t) (exp: exp): Value.t = match exp with
+    | Lval (Var x, NoOffset) -> begin match D.find_opt x d with
+        | Some v -> if M.tracing then M.trace "wrpointer-tainted" "QUERY %a : res = %a\n" d_exp exp AD.pretty v;v
+        | None -> Value.top()
+      end
+    | AddrOf (Var x, NoOffset) -> if is_wrpointer_ghost_variable x then (let res = get_value ask (AddrOf (Var (original_variable x), NoOffset)) in if M.tracing then M.trace "wrpointer-tainted" "QUERY %a, id: %d : res = %a\n" d_exp exp x.vid AD.pretty res;res) else Value.top()
+    | _ -> Value.top ()
+
+  let startcontext () = D.empty ()
+  let startstate v = D.bot ()
+  let exitstate = startstate
+
+  (* TODO: there should be a better way to do this, this should be removed here. *)
+  let return ctx exp_opt f =
+    (* remember all values of local vars *)
+    let st = List.fold_left (fun st var -> let value = get_value (ask_of_ctx ctx) (Lval (Var var, NoOffset)) in
+                              if M.tracing then M.trace "startState" "return: added value: var: %a; value: %a" d_lval (Var var, NoOffset) Value.pretty value;
+                              D.add (var) value st) (D.empty()) (f.sformals @ f.slocals) in
+    (* remember value of tainted vars in the return variable *)
+    let tainted = ctx.ask (MayBeTainted) in
+    let st = D.add return_varinfo tainted st
+    in if M.tracing then M.tracel "wrpointer-tainted" "startState: %a; state: %a\n" AD.pretty tainted D.pretty st;st
+
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    let open Queries in
+    match q with
+    | MayPointTo e -> eval (ask_of_ctx ctx) ctx.local e
+    | EvalValue e -> Address (eval (ask_of_ctx ctx) ctx.local e)
+    | _ -> Result.top q
+
+  let enter ctx var_opt f args =
+    [ctx.local, ctx.local]
+
+  let body ctx (f:fundec) =
+    (* assign function parameters *)
+    List.fold_left (fun st var -> let value = get_value (ask_of_ctx ctx) (Lval (Var var, NoOffset)) in
+                     if M.tracing then M.trace "startState" "added value: var: %a; value: %a" d_lval (Var (duplicated_variable var), NoOffset) Value.pretty value;
+                     D.add (duplicated_variable var) value st) (D.empty()) f.sformals
+
+  let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+    ctx.local
+
+  let combine_assign ctx var_opt expr f exprs t_context_opt t ask =
+    (* remove duplicated vars and local vars *)
+    ctx.local
+
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)