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

@@ -58,12 +58,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
@@ -110,14 +110,14 @@ 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 *)
@@ -127,6 +127,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 D.join ass' (D.bot ())
+      )
     (* Ignoring all other assigns *)
     | _ ->
       st
@@ -145,17 +155,37 @@ 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
+         | a when not (Queries.LS.is_top a || Queries.LS.mem (dummyFunDec.svar, `NoOffset) a) && (Queries.LS.cardinal a) = 1 ->
+           let lval = Lval.CilLval.to_lval (Queries.LS.choose a) in
+           Lval lval
+         (* It would be possible to do better here, exploiting e.g. that the things pointed to are known to be equal *)
+         (* see: https://github.com/goblint/analyzer/pull/742#discussion_r879099745 *)
+         | _ -> Lval (Mem e, NoOffset))
+      | e -> e (* TODO: Potentially recurse further? *)
+    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' ->
               if M.tracing then M.traceli "apron" "assign inner %a = %a (%a)\n" d_varinfo v d_exp e' d_plainexp e';
               if M.tracing then M.trace "apron" "st: %a\n" AD.pretty apr';
               let r = AD.assign_exp apr' (V.local v) e' in
@@ -181,7 +211,23 @@ struct
 
   (* Function call transfer functions. *)
 
+  let any_local_reachable fundec reachable_from_args =
+    let locals = fundec.sformals @ fundec.slocals in
+    let locals_id = List.map (fun v -> v.vid) locals in
+    Queries.LS.exists (fun (v',_) -> List.mem v'.vid locals_id && AD.varinfo_tracked v') reachable_from_args
+
+  let pass_to_callee fundec any_local_reachable var =
+    (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachbale to preserve relationality *)
+    (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
+    (* Also, a local *)
+    let vname = Var.to_string var in
+    let locals = fundec.sformals @ fundec.slocals in
+    match List.find_opt (fun v -> V.local_name v = vname) locals with
+    | None -> true
+    | Some v -> any_local_reachable
+
   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;
@@ -191,6 +237,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 *) *)
@@ -202,9 +249,10 @@ struct
           )
       ) new_apr arg_assigns
     in
+    let any_local_reachable = any_local_reachable fundec reachable_from_args 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 any_local_reachable 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) *)
       );
@@ -259,13 +307,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 *) *)
@@ -278,14 +329,15 @@ struct
           )
       ) new_fun_apr arg_substitutes
     in
-    let arg_vars = List.map fst arg_substitutes in
+    let any_local_reachable = any_local_reachable fundec reachable_from_args 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 any_local_reachable 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 = AD.unify new_apr new_fun_apr in (* TODO: unify_with *)
@@ -306,14 +358,49 @@ struct
     else
       unify_st
 
-  let special ctx r f args =
+
+  let invalidate_one ask ctx st lv =
+    assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
+        let apr' = AD.forget_vars st.apr [V.local v] in
+        assert_type_bounds apr' v (* re-establish type bounds after forget *)
+      )
+
+
+  (* Give the set of reachables from argument. *)
+  let reachables (ask: Queries.ask) es =
+    let reachable e st =
+      match st with
+      | None -> None
+      | Some st ->
+        let vs = ask.f (Queries.ReachableFrom e) in
+        if Queries.LS.is_top vs then
+          None
+        else
+          Some (Queries.LS.join vs st)
+    in
+    List.fold_right reachable es (Some (Queries.LS.empty ()))
+
+
+  let forget_reachable ctx st es =
     let ask = Analyses.ask_of_ctx ctx in
-    let invalidate_one st lv =
-      assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
-          let apr' = AD.forget_vars st.apr [V.local v] in
-          assert_type_bounds apr' v (* re-establish type bounds after forget *)
-        )
+    let rs =
+      match reachables ask es with
+      | None ->
+        (* top reachable, so try to invalidate everything *)
+        let fd = Node.find_fundec ctx.node in
+        AD.vars st.apr
+        |> List.filter_map (V.to_cil_varinfo fd)
+        |> List.map Cil.var
+      | Some rs ->
+        Queries.LS.elements rs
+        |> List.map Lval.CilLval.to_lval
     in
+    List.fold_left (fun st lval ->
+        invalidate_one ask ctx st lval
+      ) st rs
+
+  let special ctx r f args =
+    let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname with
@@ -323,40 +410,42 @@ struct
     | Unknown, "__goblint_commit" -> st
     | Unknown, "__goblint_assert" -> st
     | ThreadJoin { thread = id; ret_var = retvar }, _ ->
-      (* nothing to invalidate as only arguments that have their AddrOf taken may be invalidated *)
       (
-        let st' = Priv.thread_join ask ctx.global id st in
+        (* Forget value that thread return is assigned to *)
+        let st' = forget_reachable ctx st [retvar] in
+        let st' = Priv.thread_join ask ctx.global id st' in
         match r with
-        | Some lv -> invalidate_one st' lv
+        | Some lv -> invalidate_one ask ctx st' lv
         | None -> st'
       )
     | _, _ ->
-      let ask = Analyses.ask_of_ctx ctx in
-      let invalidate_one st lv =
-        assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
-            let apr' = AD.forget_vars st.apr [V.local v] in
-            assert_type_bounds apr' v (* re-establish type bounds after forget *)
-          )
+      let lvallist e =
+        let s = ask.f (Queries.MayPointTo e) in
+        match s with
+        | `Top -> []
+        | `Lifted _ -> List.map (Lval.CilLval.to_lval) (Queries.LS.elements s)
       in
-      (* nothing to do for args because only AddrOf arguments may be invalidated *)
-      let st' =
+      let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
+      let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
+      let deep_addrs =
         if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
-          let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
+          foldGlobals !Cilfacade.current_file (fun acc global ->
               match global with
               | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-                (Var vi, NoOffset) :: acc
+                mkAddrOf (Var vi, NoOffset) :: acc
               (* TODO: what about GVarDecl? *)
               | _ -> acc
-            ) []
-          in
-          List.fold_left invalidate_one st globals
+            ) deep_addrs
         )
         else
-          st
+          deep_addrs
       in
+      let st' = forget_reachable ctx st deep_addrs in
+      let shallow_lvals = List.concat_map lvallist shallow_addrs in
+      let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in
       (* invalidate lval if present *)
       match r with
-      | Some lv -> invalidate_one st' lv
+      | Some lv -> invalidate_one ask ctx st' lv
       | None -> st'
 
 
@@ -392,9 +481,10 @@ struct
     let open Queries in
     let st = ctx.local in
     let eval_int e =
+      let esimple = replace_deref_exps ctx.ask e in
       read_from_globals_wrapper
         (Analyses.ask_of_ctx ctx)
-        ctx.global st e
+        ctx.global st esimple
         (fun apr' e' -> AD.eval_int apr' e')
     in
     match q with
@@ -461,6 +551,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