Linear Two-Variable Equalities Analysis

conf/svcomp2var.json

@@ -0,0 +1,146 @@
+{
+  "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",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins" ,
+      "lin2vareq"
+    ],
+    "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",
+        "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/apron/linearTwoVarEqualityAnalysis.apron.ml

@@ -0,0 +1,31 @@
+(** {{!RelationAnalysis} Relational integer value analysis} using an OCaml implementation of the linear two-variable equalities domain ([lin2vareq]).
+
+    @see <http://doi.acm.org/10.1145/2049706.2049710> A. Flexeder, M. Petter, and H. Seidl Fast Interprocedural Linear Two-Variable Equalities. *)
+
+open Analyses
+include RelationAnalysis
+
+let spec_module: (module MCPSpec) Lazy.t =
+  lazy (
+    let module AD = LinearTwoVarEqualityDomain.D2
+    in
+    let module Priv = (val RelationPriv.get_priv ()) in
+    let module Spec =
+    struct
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
+      let name () = "lin2vareq"
+    end
+    in
+    (module Spec)
+  )
+
+let get_spec (): (module MCPSpec) =
+  Lazy.force spec_module
+
+let after_config () =
+  let module Spec = (val get_spec ()) in
+  MCP.register_analysis (module Spec : MCPSpec);
+  GobConfig.set_string "ana.path_sens[+]"  (Spec.name ())
+
+let _ =
+  AfterConfig.register after_config

src/analyses/apron/linearTwoVarEqualityAnalysis.no-apron.ml

@@ -0,0 +1,3 @@
+(* This analysis is empty on purpose. It serves only as an alternative dependency
+   in cases where the actual domain can't be used because of a missing library.
+   It was added because we don't want to fully depend on Apron. *)

src/analyses/apron/relationAnalysis.apron.ml

@@ -177,23 +177,22 @@ struct
 
   let no_overflow (ask: Queries.ask) exp =
     match Cilfacade.get_ikind_exp exp with
-    | exception Invalid_argument _ -> false (* TODO: why this? *)
+    | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
     | exception Cilfacade.TypeOfError _ -> false
     | ik ->
       if IntDomain.should_wrap ik then
         false
       else if IntDomain.should_ignore_overflow ik then
         true
       else
-        not (Queries.ID.is_top_of ik (ask.f (EvalInt exp)))
+        not (ask.f (MaySignedOverflow exp))
 
   let no_overflow ctx exp = lazy (
     let res = no_overflow ctx exp in
     if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a\n" res d_exp exp;
     res
   )
 
-
   let assert_type_bounds ask rel x =
     assert (RD.Tracked.varinfo_tracked x);
     match Cilfacade.get_ikind x.vtype with
@@ -202,8 +201,9 @@ struct
       (* TODO: don't go through CIL exp? *)
       let e1 = BinOp (Le, Lval (Cil.var x), (Cil.kintegerCilint ik type_max), intType) in
       let e2 = BinOp (Ge, Lval (Cil.var x), (Cil.kintegerCilint ik type_min), intType) in
-      let rel = RD.assert_inv rel e1 false (no_overflow ask e1) in (* TODO: how can be overflow when asserting type bounds? *)
-      let rel = RD.assert_inv rel e2 false (no_overflow ask e2) in
+      (* TODO: do not duplicate no_overflow defined via ask: https://github.com/goblint/analyzer/pull/1297#discussion_r1477281950 *)
+      let rel = RD.assert_inv ask rel e1 false (no_overflow ask e1) in (* TODO: how can be overflow when asserting type bounds? *)
+      let rel = RD.assert_inv ask rel e2 false (no_overflow ask e2) in
       rel
     | exception Invalid_argument _ ->
       rel
@@ -243,7 +243,6 @@ struct
     inner e
 
   (* Basic transfer functions. *)
-
   let assign ctx (lv:lval) e =
     let st = ctx.local in
     if !AnalysisState.global_initialization && e = MyCFG.unknown_exp then
@@ -256,7 +255,7 @@ struct
           assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' ->
               if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)\n" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
               if M.tracing then M.trace "relation" "st: %a\n" RD.pretty apr';
-              let r = RD.assign_exp apr' (RV.local v) e' (no_overflow ask simplified_e) in
+              let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
               if M.tracing then M.traceu "relation" "-> %a\n" RD.pretty r;
               r
             )
@@ -271,7 +270,7 @@ struct
     let ask = Analyses.ask_of_ctx ctx in
     let res = assign_from_globals_wrapper ask ctx.global st e (fun rel' e' ->
         (* not an assign, but must remove g#in-s still *)
-        RD.assert_inv rel' e' (not b) (no_overflow ask e)
+        RD.assert_inv ask rel' e' (not b) (no_overflow ask e)
       )
     in
     if RD.is_bot_env res then raise Deadcode;
@@ -322,7 +321,7 @@ struct
         let ask = Analyses.ask_of_ctx ctx in
         List.fold_left (fun new_rel (var, e) ->
             assign_from_globals_wrapper ask ctx.global {st with rel = new_rel} e (fun rel' e' ->
-                RD.assign_exp rel' var e' (no_overflow ask e)
+                RD.assign_exp ask rel' var e' (no_overflow ask e)
               )
           ) new_rel arg_assigns
     in
@@ -365,7 +364,7 @@ struct
         match e with
         | Some e ->
           assign_from_globals_wrapper ask ctx.global {st with rel = rel'} e (fun rel' e' ->
-              RD.assign_exp rel' RV.return e' (no_overflow ask e)
+              RD.assign_exp ask rel' RV.return e' (no_overflow ask e)
             )
         | None ->
           rel' (* leaves V.return unconstrained *)
@@ -413,7 +412,9 @@ struct
     let new_fun_rel = List.fold_left (fun new_fun_rel (var, e) ->
         assign_from_globals_wrapper ask ctx.global {st with rel = new_fun_rel} e (fun rel' e' ->
             (* not an assign, but still works? *)
-            RD.substitute_exp rel' var e' (no_overflow ask e)
+            (* substitute is the backwards semantics of assignment *)
+            (* https://antoinemine.github.io/Apron/doc/papers/expose_CEA_2007.pdf *)
+            RD.substitute_exp ask rel' var e' (no_overflow ask e)
           )
       ) new_fun_rel arg_substitutes
     in
@@ -506,7 +507,7 @@ struct
       let ask = Analyses.ask_of_ctx ctx in
       let res = assign_from_globals_wrapper ask ctx.global st e (fun apr' e' ->
           (* not an assign, but must remove g#in-s still *)
-          RD.assert_inv apr' e' false (no_overflow ask e)
+          RD.assert_inv ask apr' e' false (no_overflow ask e)
         )
       in
       if RD.is_bot_env res then raise Deadcode;
@@ -634,22 +635,20 @@ struct
     |> Enum.fold (fun acc x -> Invariant.(acc && of_exp x)) Invariant.none
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
-    let no_overflow ctx' exp' =
-      IntDomain.should_ignore_overflow (Cilfacade.get_ikind_exp exp') in (* TODO: separate no_overflow? *)
     let open Queries in
     let st = ctx.local in
     let eval_int e no_ov =
       let esimple = replace_deref_exps ctx.ask e in
       read_from_globals_wrapper
         (Analyses.ask_of_ctx ctx)
         ctx.global st esimple
-        (fun rel' e' -> RD.eval_int rel' e' no_ov)
+        (fun rel' e' -> RD.eval_int (Analyses.ask_of_ctx ctx) rel' e' no_ov)
     in
     match q with
     | EvalInt e ->
       if M.tracing then M.traceli "evalint" "relation query %a (%a)\n" d_exp e d_plainexp e;
       if M.tracing then M.trace "evalint" "relation st: %a\n" D.pretty ctx.local;
-      let r = eval_int e (lazy(no_overflow ctx e)) in
+      let r = eval_int e (no_overflow (Analyses.ask_of_ctx ctx) e) in
       if M.tracing then M.traceu "evalint" "relation query %a -> %a\n" d_exp e ID.pretty r;
       r
     | Queries.IterSysVars (vq, vf) ->
@@ -708,7 +707,29 @@ struct
       let vars = Basetype.CilExp.get_vars e |> List.unique ~eq:CilType.Varinfo.equal |> List.filter RD.Tracked.varinfo_tracked in
       let rel = RD.forget_vars rel (List.map RV.local vars) in (* havoc *)
       let rel = List.fold_left (assert_type_bounds ask) rel vars in (* add type bounds to avoid overflow in top state *)
-      let rel = RD.assert_inv rel e false (no_overflow ask e_orig) in (* assume *)
+      let rec dummyask =
+        (* assert_inv calls texpr1_expr_of_cil_exp, which simplifies the constraint based on the pre-state of the transition;
+           this does not reflect the state after RD.forget_vars rel .... has been performed; to prevent this aggressive
+           simplification, we restrict read_int queries to a local dummy ask, that only dispatches to rel instead of the
+           full state *)
+        let f (type a) (q : a Queries.t) : a =
+          let eval_int e no_ov =
+            let esimple = replace_deref_exps dummyask.f e in
+            read_from_globals_wrapper
+              (dummyask)
+              ctx.global { st with rel } esimple
+              (fun rel' e' -> RD.eval_int (dummyask) rel' e' no_ov)
+          in
+          match q with
+          | EvalInt e ->
+            if M.tracing then M.traceli "relation" "evalint query %a (%a), ctx %a\n" d_exp e d_plainexp e D.pretty ctx.local;
+            let r = eval_int e (no_overflow (dummyask) e) in
+            if M.tracing then M.trace "relation" "evalint response %a -> %a\n" d_exp e ValueDomainQueries.ID.pretty r;
+            r
+          |_ -> Queries.Result.top q
+        in
+        ({ f } : Queries.ask) in
+      let rel = RD.assert_inv dummyask rel e false (no_overflow ask e_orig) in (* assume *)
       let rel = RD.keep_vars rel (List.map RV.local vars) in (* restrict *)
 
       (* TODO: parallel write_global? *)