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 D.join ass' (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' ->
               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
@@ -175,7 +206,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;
@@ -185,6 +223,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 *) *)
@@ -198,7 +237,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) *)
       );
@@ -253,13 +292,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 *) *)
@@ -272,14 +314,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 *)
@@ -300,14 +342,41 @@ struct
     else
       unify_st
 
+
+  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
+    match reachables ask es with
+    | None -> D.top ()
+    | Some rs ->
+      Queries.LS.fold (fun lval st ->
+          invalidate_one ask ctx st (Lval.CilLval.to_lval lval)
+        ) rs st
+
+
   let special ctx r f args =
     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 *)
-        )
-    in
     let st = ctx.local in
     match LibraryFunctions.classify f.vname args with
     (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
@@ -316,26 +385,20 @@ struct
     | `Unknown "__goblint_commit" -> st
     | `Unknown "__goblint_assert" -> st
     | `ThreadJoin (id,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 *)
-          )
-      in
       let st' = match LibraryFunctions.get_invalidate_action f.vname with
-        | Some fnc -> st (* nothing to do because only AddrOf arguments may be invalidated *)
+        | Some fnc -> forget_reachable ctx st (fnc `Write args)
         | None ->
-          (* nothing to do for args because only AddrOf arguments may be invalidated *)
-          if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then (
+          let st' = if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then (
             let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
                 match global with
                 | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
@@ -344,14 +407,18 @@ struct
                 | _ -> acc
               ) []
             in
-            List.fold_left invalidate_one st globals
-          )
+            List.fold_left (invalidate_one ask ctx) st globals)
           else
             st
+          in
+          if GobConfig.get_bool "sem.unknown_function.invalidate.args" then
+            forget_reachable ctx st' args
+          else
+            st'
       in
       (* invalidate lval if present *)
       match r with
-      | Some lv -> invalidate_one st' lv
+      | Some lv -> invalidate_one ask ctx st' lv
       | None -> st'
 
 
@@ -425,6 +492,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