Apron: Track relational information for variables that have their address taken

.github/workflows/locked.yml

@@ -41,8 +41,9 @@ jobs:
         run: ./make.sh headers testci
 
       - name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
-        run:  ruby scripts/update_suite.rb group apron -s;
-
+        run: |
+          ruby scripts/update_suite.rb group apron -s
+          ruby scripts/update_suite.rb group apron2 -s
       - name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run:  ruby scripts/update_suite.rb group octagon -s
 

.github/workflows/unlocked.yml

@@ -58,7 +58,9 @@ jobs:
 
       - name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         if: ${{ matrix.apron }}
-        run: ruby scripts/update_suite.rb group apron -s
+        run: |
+          ruby scripts/update_suite.rb group apron -s
+          ruby scripts/update_suite.rb group apron2 -s
 
       - name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         if: ${{ matrix.apron }}

src/analyses/apron/apronAnalysis.apron.ml

@@ -52,12 +52,12 @@ struct
 
   module VH = BatHashtbl.Make (Basetype.Variables)
 
-  let read_globals_to_locals ask getg st e =
+  let read_globals_to_locals (ask:Queries.ask) getg st e =
     let v_ins = VH.create 10 in
     let visitor = object
       inherit nopCilVisitor
       method! vvrbl (v: varinfo) =
-        if v.vglob then (
+        if v.vglob || ThreadEscape.has_escaped ask v then (
           let v_in =
             if VH.mem v_ins v then
               VH.find v_ins v
@@ -104,14 +104,17 @@ struct
       {st with apr = apr'}
     )
 
-  let assign_to_global_wrapper ask getg sideg st lv f =
+  let rec assign_to_global_wrapper (ask:Queries.ask) getg sideg st lv f =
     match lv with
     (* Lvals which are numbers, have no offset and their address wasn't taken *)
     (* This means that variables of which multiple copies may be reachable via pointers are also also excluded (they have their address taken) *)
     (* and no special handling for them is required (https://github.com/goblint/analyzer/pull/310) *)
     | (Var v, NoOffset) when AD.varinfo_tracked v ->
-      if not v.vglob then
-        {st with apr = f st v}
+      if not v.vglob && not (ThreadEscape.has_escaped ask v) then
+        (if ask.f (Queries.IsMultiple v) then
+          {st with apr = AD.join (f st v) st.apr}
+         else
+          {st with apr = f st v})
       else (
         let v_out = Goblintutil.create_var @@ makeVarinfo false (v.vname ^ "#out") v.vtype in (* temporary local g#out for global g *)
         let st = {st with apr = AD.add_vars st.apr [V.local v_out]} in (* add temporary g#out *)
@@ -121,6 +124,16 @@ struct
         let apr'' = AD.remove_vars st'.apr [V.local v_out] in (* remove temporary g#out *)
         {st' with apr = apr''}
       )
+    | (Mem v, NoOffset) ->
+      (let r = ask.f (Queries.MayPointTo v) in
+       match r with
+       | `Top ->
+         st
+       | `Lifted s ->
+         let lvals = Queries.LS.elements r in
+         let ass' = List.map (fun lv -> assign_to_global_wrapper ask getg sideg st (Lval.CilLval.to_lval lv) f) lvals in
+         List.fold_right (fun {apr=apr1; priv=priv1} {apr=apr2; priv=priv2} -> {apr = AD.join apr1 apr2; priv = Priv.D.join priv1 priv2}) ass' {apr = AD.bot (); priv = Priv.D.bot ()}
+      )
     (* Ignoring all other assigns *)
     | _ ->
       st
@@ -139,17 +152,35 @@ struct
       apr
 
 
+  let replace_deref_exps ask e =
+    let rec inner e = match e with
+      | Const x -> e
+      | UnOp (unop, e, typ) -> UnOp(unop, inner e, typ)
+      | BinOp (binop, e1, e2, typ) -> BinOp (binop, inner e1, inner e2, typ)
+      | CastE (t,e) -> CastE (t, inner e)
+      | Lval (Var v, off) -> Lval (Var v, off)
+      | Lval (Mem e, NoOffset) ->
+        (match ask (Queries.MayPointTo e) with
+         | (`Lifted _) as r when (Queries.LS.cardinal r) = 1 ->
+           let lval = Lval.CilLval.to_lval (Queries.LS.choose r) in
+           Lval lval
+         | _ -> Lval (Mem e, NoOffset))
+      | e -> e
+    in
+    inner e
+
   (* Basic transfer functions. *)
 
   let assign ctx (lv:lval) e =
     let st = ctx.local in
     if !GU.global_initialization && e = MyCFG.unknown_exp then
       st (* ignore extern inits because there's no body before assign, so the apron env is empty... *)
     else (
-      if M.tracing then M.traceli "apron" "assign %a = %a\n" d_lval lv d_exp e;
+      let simplified_e = replace_deref_exps ctx.ask e in
+      if M.tracing then M.traceli "apron" "assign %a = %a (simplified to %a)\n" d_lval lv  d_exp e d_exp simplified_e;
       let ask = Analyses.ask_of_ctx ctx in
       let r = assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
-          assign_from_globals_wrapper ask ctx.global st e (fun apr' e' ->
+          assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' ->
               AD.assign_exp apr' (V.local v) e'
             )
         )
@@ -171,7 +202,14 @@ struct
 
   (* Function call transfer functions. *)
 
+  let pass_to_callee fundec reachable_from_args var =
+    let vname = Var.to_string var in
+    match List.find_opt (fun v -> v.vname = vname) (fundec.sformals @ fundec.slocals) with
+    | None -> true
+    | Some v -> Queries.LS.exists (fun (v',_) -> v'.vid = v.vid) reachable_from_args
+
   let enter ctx r f args =
+    let fundec = Node.find_fundec ctx.node in
     let st = ctx.local in
     if M.tracing then M.tracel "combine" "apron enter f: %a\n" d_varinfo f.svar;
     if M.tracing then M.tracel "combine" "apron enter formals: %a\n" (d_list "," d_varinfo) f.sformals;
@@ -181,6 +219,7 @@ struct
       |> List.filter (fun (x, _) -> AD.varinfo_tracked x)
       |> List.map (Tuple2.map1 V.arg)
     in
+    let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
     let arg_vars = List.map fst arg_assigns in
     let new_apr = AD.add_vars st.apr arg_vars in
     (* AD.assign_exp_parallel_with new_oct arg_assigns; (* doesn't need to be parallel since exps aren't arg vars directly *) *)
@@ -194,7 +233,7 @@ struct
     in
     AD.remove_filter_with new_apr (fun var ->
         match V.find_metadata var with
-        | Some Local -> true (* remove caller locals *)
+        | Some Local when not (pass_to_callee fundec reachable_from_args var) -> true (* remove caller locals provided they are unreachable *)
         | Some Arg when not (List.mem_cmp Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
@@ -249,13 +288,16 @@ struct
 
   let combine ctx r fe f args fc fun_st =
     let st = ctx.local in
+    let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
+    let fundec = Node.find_fundec ctx.node in
     if M.tracing then M.tracel "combine" "apron f: %a\n" d_varinfo f.svar;
     if M.tracing then M.tracel "combine" "apron formals: %a\n" (d_list "," d_varinfo) f.sformals;
     if M.tracing then M.tracel "combine" "apron args: %a\n" (d_list "," d_exp) args;
     let new_fun_apr = AD.add_vars fun_st.apr (AD.vars st.apr) in
     let arg_substitutes =
       GobList.combine_short f.sformals args (* TODO: is it right to ignore missing formals/args? *)
-      |> List.filter (fun (x, _) -> AD.varinfo_tracked x)
+      (* Do not do replacement for actuals whose value may be modified after the call *)
+      |> List.filter (fun (x, e) -> AD.varinfo_tracked x && List.for_all (fun v -> not (Queries.LS.exists (fun (v',_) -> v'.vid = v.vid) reachable_from_args)) (Basetype.CilExp.get_vars e))
       |> List.map (Tuple2.map1 V.arg)
     in
     (* AD.substitute_exp_parallel_with new_fun_oct arg_substitutes; (* doesn't need to be parallel since exps aren't arg vars directly *) *)
@@ -268,14 +310,14 @@ struct
           )
       ) new_fun_apr arg_substitutes
     in
-    let arg_vars = List.map fst arg_substitutes in
+    let arg_vars = f.sformals |> List.filter (AD.varinfo_tracked) |> List.map V.arg in
     if M.tracing then M.tracel "combine" "apron remove vars: %a\n" (docList (fun v -> Pretty.text (Var.to_string v))) arg_vars;
     AD.remove_vars_with new_fun_apr arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_apr adds them back with proper constraints *)
     let new_apr = AD.keep_filter st.apr (fun var ->
         match V.find_metadata var with
-        | Some Local -> true (* keep caller locals *)
+        | Some Local when not (pass_to_callee fundec reachable_from_args var) -> true (* keep caller locals, provided they were not passed to the function *)
         | Some Arg -> true (* keep caller args *)
-        | _ -> false (* remove everything else (globals, global privs) *)
+        | _ -> false (* remove everything else (globals, global privs, reachable things from the caller) *)
       )
     in
     let unify_apr = ApronDomain.A.unify Man.mgr new_apr new_fun_apr in (* TODO: unify_with *)
@@ -421,6 +463,8 @@ struct
     (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *)
     | Events.EnterMultiThreaded ->
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st
+    | Events.Escape escaped ->
+      Priv.escape ctx.node (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st escaped
     | _ ->
       st
 

src/analyses/apron/apronPriv.apron.ml

@@ -34,6 +34,7 @@ module type S =
 
     val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> apron_components_t -> [`Normal | `Join | `Return | `Init | `Thread] -> apron_components_t
 
+    val escape: Node.t -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> apron_components_t -> EscapeDomain.EscapedVars.t -> apron_components_t
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> apron_components_t -> apron_components_t
     val threadenter: Q.ask -> (V.t -> G.t) -> apron_components_t -> apron_components_t
 
@@ -50,6 +51,9 @@ struct
   module D = Lattice.Unit
   module G = Lattice.Unit
   module V = EmptyV
+  module AV = ApronDomain.V
+
+  type apron_components_t = ApronDomain.ApronComponents (AD) (D).t
 
   let name () = "Dummy"
   let startstate () = ()
@@ -65,6 +69,21 @@ struct
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg st reason = st
+  let escape node ask getg sideg (st:apron_components_t) escaped:apron_components_t =
+    let apr = st.apr in
+    let esc_vars = List.filter (fun var -> match AV.find_metadata var with
+        | Some (Global _) -> false
+        | Some Local ->
+          (let fundec = Node.find_fundec node in
+           let r = AV.to_cil_varinfo fundec var in
+           match r with
+           | Some r -> EscapeDomain.EscapedVars.mem r escaped
+           | _ -> false)
+        | _ -> false
+      ) (AD.vars apr)
+    in
+    let apr_local = AD.remove_vars apr esc_vars in
+    { st with apr = apr_local }
 
   let enter_multithreaded ask getg sideg st = st
   let threadenter ask getg st = st
@@ -315,6 +334,8 @@ struct
     | `Thread ->
       st
 
+  let escape node ask getg sideg st escaped = (* TODO: Implement *) st
+
   let enter_multithreaded ask getg sideg (st: apron_components_t): apron_components_t =
     let apr = st.apr in
     let (g_vars, gs) =
@@ -509,6 +530,23 @@ struct
     let apr_local = AD.remove_vars apr g_vars in (* TODO: side effect initial values to mutex_globals? *)
     {st with apr = apr_local}
 
+  let escape node ask getg sideg (st:apron_components_t) escaped : apron_components_t =
+    let apr = st.apr in
+    let esc_vars = List.filter (fun var -> match AV.find_metadata var with
+        | Some (Global _) -> false
+        | Some Local ->
+          (let fundec = Node.find_fundec node in
+           let r = AV.to_cil_varinfo fundec var in
+           match r with
+           | Some r -> EscapeDomain.EscapedVars.mem r escaped
+           | _ -> false)
+        | _ -> false
+      ) (AD.vars apr) in
+    let apr_side = AD.keep_vars apr esc_vars in
+    sideg V.mutex_inits apr_side;
+    let apr_local = AD.remove_vars apr esc_vars in
+    { st with apr = apr_local }
+
   let threadenter ask getg (st: apron_components_t): apron_components_t =
     {apr = AD.bot (); priv = startstate ()}
 
@@ -1025,6 +1063,26 @@ struct
     | `Thread ->
       st
 
+  let escape node ask getg sideg (st: apron_components_t) escaped: apron_components_t =
+    let apr = st.apr in
+    let esc_vars = List.filter (fun var -> match AV.find_metadata var with
+        | Some (Global _) -> false
+        | Some Local ->
+          (let fundec = Node.find_fundec node in
+           let r = AV.to_cil_varinfo fundec var in
+           match r with
+           | Some r -> EscapeDomain.EscapedVars.mem r escaped
+           | _ -> false)
+        | _ -> false
+      ) (AD.vars apr) in
+    let apr_side = AD.keep_vars apr esc_vars in
+    let apr_side = Cluster.unlock (W.top ()) apr_side in (* top W to avoid any filtering *)
+    let tid = ThreadId.get_current ask in
+    let sidev = GMutex.singleton tid apr_side in
+    sideg V.mutex_inits (G.create_mutex sidev);
+    let apr_local = AD.remove_vars apr esc_vars in
+    { st with apr = apr_local }
+
   let enter_multithreaded (ask:Q.ask) getg sideg (st: apron_components_t): apron_components_t =
     let apr = st.apr in
     (* Don't use keep_filter & remove_filter because it would duplicate find_metadata-s. *)

src/cdomains/apron/apronDomain.apron.ml

@@ -674,7 +674,7 @@ struct
 
     let varinfo_tracked vi =
       (* no vglob check here, because globals are allowed in apron, but just have to be handled separately *)
-      type_tracked vi.vtype && not vi.vaddrof
+      type_tracked vi.vtype
   end
 
   include AOps (Tracked) (Man)

tests/regression/24-octagon/17-address.c

@@ -0,0 +1,26 @@
+// SKIP PARAM: --set solver td3 --enable ana.int.interval  --set ana.base.arrays.domain partitioned  --set ana.activated "['base','threadid','threadflag','expRelation','apron','mallocWrapper']" --set ana.base.privatization none
+// Example from https://www-apr.lip6.fr/~mine/publi/article-mine-HOSC06.pdf
+void main(void) {
+  int X = 0;
+  int N = rand();
+  if(N < 0) { N = 0; }
+
+  while(X < N) {
+    X++;
+  }
+
+  int* ptr = &N;
+  *ptr = N;
+
+
+  assert(X-N == 0);
+  assert(X == N);
+
+  if(X == N) {
+    N = 8;
+  } else {
+    // is dead code but if that is detected or not depends on what we do in branch
+    // currenlty we can't detect this
+    N = 42;
+  }
+}

tests/regression/36-apron/07-problem-pointer.c

@@ -1,19 +1,21 @@
-// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron']" --set ana.base.privatization none --set ana.apron.privatization dummy
+// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.base.privatization none --set ana.apron.privatization dummy
 extern int __VERIFIER_nondet_int();
 
 void change(int *p) {
     (*p)++;
+    int* ptr = &p;
 }
 
 int g;
 int main() {
     int c = __VERIFIER_nondet_int();
-    g = 3; // Globals are not tracked by apron for now
+    g = 3;
     assert(g != 3); // FAIL
     assert(g == 3);
     int a = 5;
     int *p = &a; // after this apron should put a to top because pointers are not tracked
     change(p);
+    assert(a == 5); //FAIL
     assert(a - 6 == 0);
     return 0;
 }

tests/regression/45-escape/01-local-in-pthread.c

@@ -1,7 +1,5 @@
 #include <pthread.h>
 #include <assert.h>
-
-#include <pthread.h>
 #include <stdio.h>
 #include <unistd.h>
 

tests/regression/46-apron2/05-pointer-multilevel.c

@@ -0,0 +1,27 @@
+// SKIP PARAM: --set solver td3 --set ana.activated "['base','threadid','threadflag','mallocWrapper','apron','escape']" --set ana.base.privatization none --set ana.apron.privatization dummy
+extern int __VERIFIER_nondet_int();
+
+void otherchange(int* ptr) {
+    (*ptr)++;
+}
+
+void change(int *p) {
+    (*p)++;
+    otherchange(p);
+    int* ptr = &p;
+    assert(*p ==7);
+}
+
+int g;
+int main() {
+    int c = __VERIFIER_nondet_int();
+    g = 3;
+    assert(g != 3); // FAIL
+    assert(g == 3);
+    int a = 5;
+    int *p = &a;
+    change(p);
+    assert(a == 5); //FAIL
+    assert(a - 7 == 0);
+    return 0;
+}