Refactor setjmp/longjmp analysis

.github/workflows/locked.yml

@@ -25,6 +25,9 @@ jobs:
 
     runs-on: ${{ matrix.os }}
 
+    env:
+      OCAMLRUNPARAM: b
+
     steps:
       - name: Checkout code
         uses: actions/checkout@v3
@@ -73,6 +76,12 @@ jobs:
       - name: Test incremental regression with cfg comparison
         run: ruby scripts/update_suite.rb -c
 
+      - uses: actions/upload-artifact@v3
+        if: always()
+        with:
+          name: suite_result
+          path: tests/suite_result/
+
   extraction:
     if: ${{ github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' }}
 

src/analyses/abortUnless.ml

@@ -46,7 +46,7 @@ struct
     in
     [false, candidate]
 
-  let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     if au && lval = None then (
       (* Assert happens after evaluation of call, so if variables in `arg` are assigned to, asserting might unsoundly yield bot *)
       (* See test 62/03 *)

src/analyses/accessAnalysis.ml

@@ -24,9 +24,12 @@ struct
   module G = AccessDomain.EventSet
 
   let collect_local = ref false
+  let emit_single_threaded = ref false
 
   let init _ =
-    collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed"
+    collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
+    let activated = get_string_list "ana.activated" in
+    emit_single_threaded := List.mem (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
@@ -40,7 +43,7 @@ struct
       + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
   let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp =
     if M.tracing then M.traceli "access" "access_one_top %a %b %a:\n" AccessKind.pretty kind reach d_exp exp;
-    if force || !collect_local || ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) then (
+    if force || !collect_local || !emit_single_threaded || ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) then (
       if deref then
         do_access ctx kind reach exp;
       Access.distribute_access_exp (do_access ctx Read false) exp
@@ -102,7 +105,7 @@ struct
   let enter ctx lv f args : (D.t * D.t) list =
     [(ctx.local,ctx.local)]
 
-  let combine ctx ?(longjmpthrough = false) lv fexp f args fc al f_ask =
+  let combine ctx lv fexp f args fc al f_ask =
     access_one_top ctx Read false fexp;
     begin match lv with
       | None      -> ()

src/analyses/activeLongjmp.ml

@@ -5,49 +5,29 @@ open Analyses
 
 module Spec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "activeLongjmp"
 
   (* The first component are the longjmp targets, the second are the longjmp callers *)
   module D = JmpBufDomain.ActiveLongjmps
   module C = Lattice.Unit
 
-  (* transfer functions *)
-  let assign ctx (lval:lval) (rval:exp) : D.t =
-    ctx.local
-
-  let branch ctx (exp:exp) (tv:bool) : D.t =
-    ctx.local
-
-  let body ctx (f:fundec) : D.t =
-    ctx.local
-
-  let return ctx (exp:exp option) (f:fundec) : D.t =
-    ctx.local
-
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [ctx.local, ctx.local]
-
-  let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
-    au
+  let context _ _ = ()
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special arglist, f.vname with
-    | Longjmp {env; value; sigrestore}, _ ->
+    | Longjmp {env; value}, _ ->
       (* Set target to current value of env *)
       let bufs = ctx.ask (EvalJumpBuf env) in
       bufs, JmpBufDomain.NodeSet.singleton(ctx.prev_node)
     | _ -> ctx.local
 
   let startstate v = D.bot ()
-  let threadenter ctx lval f args = [D.top ()]
-  let threadspawn ctx lval f args fctx = ctx.local
+  let threadenter ctx lval f args = [D.top ()] (* TODO: why other threads start with top? *)
   let exitstate  v = D.top ()
 
-  let context _ _ = ()
-
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | ActiveJumpBuf ->

src/analyses/activeSetjmp.ml

@@ -5,48 +5,29 @@ open Analyses
 
 module Spec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "activeSetjmp"
 
   module D = JmpBufDomain.JmpBufSet
   module C = JmpBufDomain.JmpBufSet
 
-  (* transfer functions *)
-  let assign ctx (lval:lval) (rval:exp) : D.t =
-    ctx.local
-
-  let branch ctx (exp:exp) (tv:bool) : D.t =
-    ctx.local
-
-  let body ctx (f:fundec) : D.t =
-    ctx.local
-
-  let return ctx (exp:exp option) (f:fundec) : D.t =
-    ctx.local
-
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [ctx.local, ctx.local]
+  let should_join a b = D.equal a b
 
-  let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =
-    ctx.local
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =
+    ctx.local (* keep local as opposed to IdentitySpec *)
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special arglist with
     | Setjmp _ ->
-      let controlctx = ControlSpecC.hash (ctx.control_context ()) in
-      let entry = (ctx.prev_node, IntDomain.Flattened.of_int (Int64.of_int controlctx)) in
+      let entry = (ctx.prev_node, ctx.control_context ()) in
       D.add (Target entry) ctx.local
-    | Longjmp {env; value; sigrestore} -> ctx.local
     | _ -> ctx.local
 
   let startstate v = D.bot ()
   let threadenter ctx lval f args = [D.bot ()]
-  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate v = D.top ()
-  let context fundec v = v
-  let should_join a b = D.equal a b
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with

src/analyses/apron/relationAnalysis.apron.ml

@@ -350,7 +350,7 @@ struct
         st'
     end
 
-  let combine ctx ?(longjmpthrough = false) r fe f args fc fun_st (f_ask : Queries.ask) =
+  let combine ctx r fe f args fc fun_st (f_ask : Queries.ask) =
     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

src/analyses/assert.ml

@@ -27,7 +27,7 @@ struct
   let enter ctx (lval: lval option) (fd:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, ctx.local]
 
-  let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (fd:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+  let combine ctx (lval:lval option) fexp (fd:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     au
 
   let assert_fn ctx e check refine =

src/analyses/base.ml

@@ -147,6 +147,8 @@ struct
   let return_var () = AD.from_var (return_varinfo ())
   let return_lval (): lval = (Var (return_varinfo ()), NoOffset)
 
+  let longjmp_return = ref dummyFunDec.svar
+
   let heap_var ctx =
     let info = match (ctx.ask Q.HeapVar) with
       | `Lifted vinfo -> vinfo
@@ -162,6 +164,7 @@ struct
       | None -> ()
     end;
     return_varstore := Goblintutil.create_var @@ makeVarinfo false "RETURN" voidType;
+    longjmp_return := Goblintutil.create_var @@ makeVarinfo false "LONGJMP_RETURN" intType;
     Priv.init ()
 
   let finalize () =
@@ -1250,14 +1253,19 @@ struct
         List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
       end
     | Q.EvalJumpBuf e ->
-      (match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
-       | `Address jmp_buf ->
-         if AD.mem Addr.UnknownPtr jmp_buf then M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
-         begin match get ~top:(VD.bot ()) (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with
-           | `JmpBuf (x, t) -> if t then M.warn "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;x
-           | y -> failwith (Printf.sprintf "problem?! is %s %s:\n state is %s" (CilType.Exp.show e) (VD.show y) (Pretty.sprint ~width:5000 (D.pretty () ctx.local)))
-         end
-       | _ -> failwith "problem?!");
+      begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+        | `Address jmp_buf ->
+          if AD.mem Addr.UnknownPtr jmp_buf then
+            M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
+          begin match get ~top:(VD.bot ()) (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with
+            | `JmpBuf (x, copied) ->
+              if copied then
+                M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
+              x
+            | y -> failwith (Pretty.sprint ~width:max_int (Pretty.dprintf "problem?! is %a %a:\n state is %a" CilType.Exp.pretty e VD.pretty y D.pretty ctx.local))
+          end
+        | _ -> failwith "problem?!"
+      end
     | Q.EvalInt e ->
       query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
     | Q.EvalLength e -> begin
@@ -2242,31 +2250,43 @@ struct
           st
       end
     | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
-    | Setjmp { env; savesigs}, _ ->
-      (let st' = (match (eval_rv (Analyses.ask_of_ctx ctx) gs st env) with
-           | `Address jmp_buf ->
-             let controlctx = ControlSpecC.hash (ctx.control_context ()) in
-             let value = `JmpBuf ((ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, IntDomain.Flattened.of_int (Int64.of_int controlctx)))),false) in
-             let r = set ~ctx (Analyses.ask_of_ctx ctx) gs st jmp_buf (Cilfacade.typeOf env) value in
-             M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env  D.pretty st  D.pretty r;
-             r
-           | _      -> failwith "problem?!")
-       in
-       match lv with
-       | Some lv ->
-         set ~ctx (Analyses.ask_of_ctx ctx) gs st' (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv) (Cilfacade.typeOfLval lv) (`Int (ID.of_int IInt BI.zero))
-       | None -> st')
-    | Longjmp {env; value; sigrestore}, _ ->
+    | Setjmp { env }, _ ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let st' = match eval_rv ask gs st env with
+        | `Address jmp_buf ->
+          let value = `JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
+          let r = set ~ctx ask gs st jmp_buf (Cilfacade.typeOf env) value in
+          if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
+          r
+        | _ -> failwith "problem?!"
+      in
+      begin match lv with
+        | Some lv ->
+          set ~ctx ask gs st' (eval_lv ask ctx.global st lv) (Cilfacade.typeOfLval lv) (`Int (ID.of_int IInt BI.zero))
+        | None -> st'
+      end
+    | Longjmp {env; value}, _ ->
+      let ask = Analyses.ask_of_ctx ctx in
       let ensure_not_zero rv = match rv with
-        | `Int i when ID.to_bool i = Some true -> rv
-        | `Int i when ID.to_bool i = Some false -> M.warn "Must: Longjmp with a value of 0 is silently changed to 1"; `Int (ID.of_int (ID.ikind i) Z.one)
-        | `Int i when ID.to_bool i = None -> M.warn "May: Longjmp with a value of 0 is silently changed to 1"; `Int (ID.meet i (ID.of_excl_list (ID.ikind i) [Z.one]))
-        | _ -> M.warn "Arguments to longjmp are strange!"; rv
+        | `Int i ->
+          begin match ID.to_bool i with
+            | Some true -> rv
+            | Some false ->
+              M.error "Must: Longjmp with a value of 0 is silently changed to 1";
+              `Int (ID.of_int (ID.ikind i) Z.one)
+            | None ->
+              M.warn "May: Longjmp with a value of 0 is silently changed to 1";
+              let ik = ID.ikind i in
+              `Int (ID.join (ID.meet i (ID.of_excl_list ik [Z.zero])) (ID.of_int ik Z.one))
+          end
+        | _ ->
+          M.warn ~category:Program "Arguments to longjmp are strange!";
+          rv
       in
-      let rv = ensure_not_zero @@ eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local value in
+      let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in
       let t = Cilfacade.typeOf value in
-      set ~ctx ~t_override:t (Analyses.ask_of_ctx ctx) ctx.global ctx.local (return_var ()) t rv
-      (* Not rasing Deadode here, deadcode is raised at a higher level! *)
+      set ~ctx ~t_override:t ask ctx.global ctx.local (AD.from_var !longjmp_return) t rv
+      (* Not rasing Deadcode here, deadcode is raised at a higher level! *)
     | _, _ ->
       let st =
         special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args
@@ -2311,7 +2331,7 @@ struct
             end
         else st) tainted_lvs local_st
 
-  let combine ctx ?(longjmpthrough = false) (lval: lval option) fexp (f: fundec) (args: exp list) fc (after: D.t) (f_ask: Q.ask) : D.t =
+  let combine ctx (lval: lval option) fexp (f: fundec) (args: exp list) fc (after: D.t) (f_ask: Q.ask) : D.t =
     let combine_one (st: D.t) (fun_st: D.t) =
       if M.tracing then M.tracel "combine" "%a\n%a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
       (* This function does miscellaneous things, but the main task was to give the
@@ -2321,29 +2341,25 @@ struct
        * variables of the called function from cpa_s. *)
       let add_globals (st: store) (fun_st: store) =
         (* Remove the return value as this is dealt with separately. *)
-        let cpa_noreturn =
-          if not longjmpthrough then
-            (* Remove the return value as this is dealt with separately. *)
-            CPA.remove (return_varinfo ()) fun_st.cpa
-          else
-            (* Keep the return value as this is not actually the return value but the thing supplied in longjmp *)
-            fun_st.cpa
-        in
+        let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
         let ask = (Analyses.ask_of_ctx ctx) in
         let tainted = f_ask.f Q.MayBeTainted in
         if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname Q.LS.pretty tainted;
         if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
-        if (Q.LS.is_top tainted) then
+        if Q.LS.is_top tainted then
           let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
           let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa';
           { fun_st with cpa = cpa' }
         else
           (* remove variables from caller cpa, that are global and not in the callee cpa *)
           let cpa_caller = CPA.filter (fun x _ -> (not (is_global ask x)) || CPA.mem x fun_st.cpa) st.cpa in
+          if M.tracing then M.trace "taintPC" "cpa_caller: %a\n" CPA.pretty cpa_caller;
           (* add variables from callee that are not in caller yet *)
           let cpa_new = CPA.filter (fun x _ -> not (CPA.mem x cpa_caller)) cpa_noreturn in
+          if M.tracing then M.trace "taintPC" "cpa_new: %a\n" CPA.pretty cpa_new;
           let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
+          if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller';
           (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
           let tainted = Q.LS.filter (fun (v, _) ->  not (CPA.mem v cpa_new)) tainted in
           let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in
@@ -2556,6 +2572,13 @@ struct
       assert_fn ctx exp true
     | Events.Unassume {exp; uuids} ->
       Timing.wrap "base unassume" (unassume ctx exp) uuids
+    | Events.Longjmped {lval} ->
+      begin match lval with
+        | Some lval ->
+          let st' = assign ctx lval (Lval (Cil.var !longjmp_return)) in
+          {st' with cpa = CPA.remove !longjmp_return st'.cpa}
+        | None -> ctx.local
+      end
     | _ ->
       ctx.local
 end

src/analyses/condVars.ml

@@ -139,7 +139,7 @@ struct
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, D.bot ()]
 
-  let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     (* combine caller's state with globals from callee *)
     (* TODO (precision): globals with only global vars are kept, the rest is lost -> collect which globals are assigned to *)
     (* D.merge (fun k s1 s2 -> match s2 with Some ss2 when (fst k).vglob && D.only_global_exprs ss2 -> s2 | _ when (fst k).vglob -> None | _ -> s1) ctx.local au *)

src/analyses/expRelation.ml

@@ -98,7 +98,7 @@ struct
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, ctx.local]
 
-  let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     au
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =