diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 685fdc0afd..343882ebd5 100644
--- a/.github/workflows/locked.yml
+++ b/.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' }}
diff --git a/src/analyses/abortUnless.ml b/src/analyses/abortUnless.ml
index e53d4dfa3d..b548519583 100644
--- a/src/analyses/abortUnless.ml
+++ b/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 *)
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 1b616869cf..cf363d9b06 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/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 -> ()
diff --git a/src/analyses/activeLongjmp.ml b/src/analyses/activeLongjmp.ml
index f8f76e4748..185cdfca0e 100644
--- a/src/analyses/activeLongjmp.ml
+++ b/src/analyses/activeLongjmp.ml
@@ -5,7 +5,7 @@ open Analyses
module Spec =
struct
- include Analyses.DefaultSpec
+ include Analyses.IdentitySpec
let name () = "activeLongjmp"
@@ -13,41 +13,22 @@ struct
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
+ (* Initial values don't really matter: overwritten at longjmp call. *)
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.bot ()]
let exitstate v = D.top ()
- let context _ _ = ()
-
let query ctx (type a) (q: a Queries.t): a Queries.result =
match q with
| ActiveJumpBuf ->
diff --git a/src/analyses/activeSetjmp.ml b/src/analyses/activeSetjmp.ml
index 3eb7dce3c1..904ad12ae7 100644
--- a/src/analyses/activeSetjmp.ml
+++ b/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
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 3fa80a39d3..f30cbeb278 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/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
diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml
index 9cc605e64a..40cf00df2b 100644
--- a/src/analyses/assert.ml
+++ b/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 =
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 0088bb3ff6..9726bc72db 100644
--- a/src/analyses/base.ml
+++ b/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,19 +2341,12 @@ 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';
@@ -2341,9 +2354,12 @@ struct
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
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 5e557b319f..ad2910bc7c 100644
--- a/src/analyses/condVars.ml
+++ b/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 *)
diff --git a/src/analyses/expRelation.ml b/src/analyses/expRelation.ml
index 3835d5cc04..393121b616 100644
--- a/src/analyses/expRelation.ml
+++ b/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 =
diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml
index 0e0b9c0bd3..32c2f40744 100644
--- a/src/analyses/expsplit.ml
+++ b/src/analyses/expsplit.ml
@@ -46,7 +46,7 @@ struct
let return ctx (exp:exp option) (f:fundec) =
emit_splits_ctx ctx
- let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
let d = D.join ctx.local au in
emit_splits ctx d
@@ -60,18 +60,17 @@ struct
| _, "__goblint_split_end" ->
let exp = List.hd arglist in
D.remove exp ctx.local
- | Setjmp { env; savesigs}, _ ->
+ | Setjmp { env }, _ ->
Option.map_default (fun lval ->
match GobConfig.get_string "ana.setjmp.split" with
| "none" -> ctx.local
| "precise" ->
- let e = Lval lval in
- let ik = Cilfacade.get_ikind_exp e in
- D.add e (ID.top_of ik) ctx.local
- | "coarse" ->
let e = Lval lval in
let ik = Cilfacade.get_ikind_exp e in
- let e = BinOp(Eq, e, integer 0, intType) in
+ D.add e (ID.top_of ik) ctx.local
+ | "coarse" ->
+ let e = Lval lval in
+ let e = BinOp (Eq, e, integer 0, intType) in
D.add e (ID.top_of IInt) ctx.local
| _ -> failwith "Invalid value for ana.setjmp.split"
) ctx.local lval
@@ -90,6 +89,8 @@ struct
| UpdateExpSplit exp ->
let value = ctx.ask (EvalInt exp) in
D.add exp value ctx.local
+ | Longjmped _ ->
+ emit_splits_ctx ctx
| _ ->
ctx.local
end
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index 71e5c02161..efec236ede 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -1057,7 +1057,7 @@ module Spec : Analyses.MCPSpec = struct
[ (d_caller, d_callee) ]
- 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 D.any_is_bot ctx.local || D.any_is_bot au
then ctx.local
else
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index 40b1edd9f6..4260f2d479 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -163,7 +163,7 @@ struct
D.extend_value unclosed_var (mustOpen, mayOpen) m
) else m
- 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 =
let m = ctx.local in
(* pop the last location off the stack *)
let m = D.edit_callstack List.tl m in (* TODO could it be problematic to keep this in the caller instead of callee domain? if we only add the stack for the callee in enter, then there would be no need to pop a location anymore... *)
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index d44215e027..a477fc1809 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -62,8 +62,8 @@ type special =
| Strcpy of { dest: Cil.exp; src: Cil.exp } (* TODO: add count for strncpy when actually used *)
| Abort
| Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
- | Setjmp of {env: Cil.exp; savesigs: Cil.exp; }
- | Longjmp of {env: Cil.exp; value: Cil.exp; sigrestore: bool}
+ | Setjmp of { env: Cil.exp; }
+ | Longjmp of { env: Cil.exp; value: Cil.exp; }
| Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 6c502e1098..e38079f4dd 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -50,12 +50,12 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("abs", unknown [drop "j" []]);
("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
- ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env; savesigs = Cil.zero }); (* only has one underscore *)
- ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env; savesigs = Cil.zero });
- ("__sigsetjmp", special [__ "env" [w]; __ "savesigs" []] @@ fun env savesigs -> Setjmp { env; savesigs }); (* has two underscores *)
- ("sigsetjmp", special [__ "env" [w]; __ "savesigs" []] @@ fun env savesigs -> Setjmp { env; savesigs });
- ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value; sigrestore = false });
- ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value; sigrestore = true });
+ ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
+ ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
+ ("__sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env }); (* has two underscores *)
+ ("sigsetjmp", special [__ "env" [w]; drop "savesigs" []] @@ fun env -> Setjmp { env });
+ ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
+ ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
]
(** C POSIX library functions.
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index a585ee7a58..f4640f8ea2 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -519,7 +519,7 @@ struct
do_spawns ctx !spawns;
map (fun xs -> (topo_sort_an @@ map fst xs, topo_sort_an @@ map snd xs)) @@ n_cartesian_product css
- let combine (ctx:(D.t, G.t, C.t, V.t) ctx) ?(longjmpthrough= false) r fe f a fc fd f_ask =
+ let combine (ctx:(D.t, G.t, C.t, V.t) ctx) r fe f a fc fd f_ask =
let spawns = ref [] in
let sides = ref [] in
let emits = ref [] in
@@ -540,7 +540,7 @@ struct
in
let f post_all (n,(module S:MCPSpec),(d,fc,fd)) =
let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "combine" ~post_all ctx'' n d in
- n, repr @@ S.combine ~longjmpthrough ctx' r fe f a (Option.map obj fc) (obj fd) f_ask
+ n, repr @@ S.combine ctx' r fe f a (Option.map obj fc) (obj fd) f_ask
in
let d, q = map_deadcode f @@ List.rev @@ spec_list3_rev_acc [] ctx.local fc fd in
do_sideg ctx !sides;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index 01ed816955..94b9d1893d 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -27,7 +27,7 @@ struct
let assign ctx lval rval =
assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
- let combine ctx ?(longjmpthrough = false) lval f fd args context f_local (f_ask: Queries.ask) =
+ let combine ctx lval f fd args context f_local (f_ask: Queries.ask) =
match lval with
| None -> f_local
| Some lval -> assign_lval (Analyses.ask_of_ctx ctx) lval f_local
diff --git a/src/analyses/mallocWrapperAnalysis.ml b/src/analyses/mallocWrapperAnalysis.ml
index f46f46d5e2..4890646aa8 100644
--- a/src/analyses/mallocWrapperAnalysis.ml
+++ b/src/analyses/mallocWrapperAnalysis.ml
@@ -87,7 +87,7 @@ struct
let callee = (counter, new_wrapper_node) in
[(ctx.local, callee)]
- let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) (f_ask: Queries.ask) : D.t =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc ((counter, _):D.t) (f_ask: Queries.ask) : D.t =
(* Keep (potentially higher) counter from callee and keep wrapper node from caller *)
let _, lnode = ctx.local in
(counter, lnode)
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 7550c00d6f..0a5261a381 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -200,7 +200,7 @@ struct
List.iter (warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local) args;
[ctx.local,nst]
- 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 =
let cal_st = remove_unreachable (Analyses.ask_of_ctx ctx) args ctx.local in
let ret_st = D.union au (D.diff ctx.local cal_st) in
let new_u =
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index acbe86feb6..62af3451a5 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -5,13 +5,15 @@ open Analyses
module Spec =
struct
- include Analyses.DefaultSpec
+ include Analyses.IdentitySpec
let name () = "modifiedSinceLongjmp"
module D = JmpBufDomain.LocallyModifiedMap
module VS = D.VarSet
module C = Lattice.Unit
+ let context _ _ = ()
+
let add_to_all_defined vs d =
D.map (fun vs' -> VS.union vs vs') d
@@ -25,64 +27,40 @@ struct
else
Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())
- let relevants_from_lval_opt ctx lval = match lval with
- | Some (Var v, _) -> if is_relevant v then VS.singleton v else VS.empty ()
- | Some (Mem e, _) -> relevants_from_ls (ctx.ask (Queries.MayPointTo e))
- | None -> VS.empty ()
-
(* transfer functions *)
- let assign ctx (lval:lval) (rval:exp) : D.t =
- add_to_all_defined (relevants_from_lval_opt ctx (Some lval)) 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, D.bot ()]
+ [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
- 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 fromlv = if not longjmpthrough then relevants_from_lval_opt ctx lval else VS.empty () in
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
- add_to_all_defined (VS.union taintedcallee fromlv) ctx.local
+ add_to_all_defined taintedcallee ctx.local
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
let v = D.find entry ctx.local in (* Will make bot binding explicit here *)
(* LHS of setjmp not marked as tainted on purpose *)
D.add entry v ctx.local
| _ ->
- (* perform shallow and deep invalidate according to Library descriptors *)
- let vs = relevants_from_lval_opt ctx lval in
- let desc = LibraryFunctions.find f in
- let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in
- let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in
- let vs = List.fold_left (fun acc addr -> VS.union acc (relevants_from_ls (ctx.ask (Queries.MayPointTo addr)))) vs shallow_addrs in
- let vs = List.fold_left (fun acc addr -> VS.union acc (relevants_from_ls (ctx.ask (Queries.ReachableFrom addr)))) vs deep_addrs in
- add_to_all_defined vs ctx.local
+ ctx.local
let startstate v = D.bot ()
let threadenter ctx lval f args = [D.bot ()]
- let threadspawn ctx lval f args fctx =
- add_to_all_defined (relevants_from_lval_opt ctx lval) ctx.local
-
let exitstate v = D.top ()
- let context _ _ = ()
-
let query ctx (type a) (q: a Queries.t): a Queries.result =
match q with
| Queries.MayBeModifiedSinceSetjmp entry -> D.find entry ctx.local
| _ -> Queries.Result.top q
+
+ let event ctx (e: Events.t) octx =
+ match e with
+ | Access {lvals; kind = Write; _} ->
+ add_to_all_defined (relevants_from_ls lvals) ctx.local
+ | _ ->
+ ctx.local
end
let _ =
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index 2573d88672..42529dd9c3 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -3,113 +3,99 @@ open Analyses
module Spec =
struct
- include Analyses.DefaultSpec
+ include Analyses.IdentitySpec
module VS = SetDomain.ToppedSet(CilType.Varinfo) (struct let topname = "All vars" end)
let name () = "poisonVariables"
module D = VS
module C = Lattice.Unit
- let rec check_exp ask tainted e = match e with
- (* Recurse over the structure in the expression, returning true if any varinfo appearing in the expression is tainted *)
- | AddrOf v
- | StartOf v -> check_lval ~ignore_var:true ask tainted v
- | Lval v -> check_lval ask tainted v
- | BinOp (_,e1,e2,_) -> check_exp ask tainted e1; check_exp ask tainted e2
- | Real e
- | Imag e
- | SizeOfE e
- | AlignOfE e
- | CastE (_,e)
- | UnOp (_,e,_) -> check_exp ask tainted e
- | SizeOf _ | SizeOfStr _ | Const _ | AlignOf _ | AddrOfLabel _ -> ()
- | Question (b, t, f, _) -> check_exp ask tainted b; check_exp ask tainted t; check_exp ask tainted f
- and check_lval ask ?(ignore_var = false) tainted lval = match lval with
- | (Var v, offset) ->
- if not ignore_var && not v.vglob && VS.mem v tainted then M.warn "accessing poisonous variable %a" d_varinfo v;
- check_offset ask tainted offset
- | (Mem e, offset) ->
- (try
- Queries.LS.iter (fun lv -> check_lval ~ignore_var ask tainted @@ Lval.CilLval.to_lval lv) (ask (Queries.MayPointTo e))
- with
- SetDomain.Unsupported _ -> if not @@ VS.is_empty tainted then M.warn "accessing unknown memory location, may be tainted!");
- check_exp ask tainted e;
+ let context _ _ = ()
- check_offset ask tainted offset;
- ()
- and check_offset ask tainted offset = match offset with
- | NoOffset -> ()
- | Field (_, o) -> check_offset ask tainted o
- | Index (e, o) -> check_exp ask tainted e; check_offset ask tainted o
+ let check_lval tainted ((v, offset): Queries.LS.elt) =
+ if not v.vglob && VS.mem v tainted then
+ M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" d_varinfo v
- let rec rem_lval ask tainted lval = match lval with
- | (Var v, NoOffset) -> VS.remove v tainted (* TODO: If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
- | (Mem e, NoOffset) ->
- (try
- let r = Queries.LS.elements (ask (Queries.MayPointTo e)) in
- match r with
- | [x] -> rem_lval ask tainted @@ Lval.CilLval.to_lval x
- | _ -> tainted
- with
- SetDomain.Unsupported _ -> tainted)
+ let rem_lval tainted ((v, offset): Queries.LS.elt) = match offset with
+ | `NoOffset -> VS.remove v tainted
| _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
(* transfer functions *)
- let assign ctx (lval:lval) (rval:exp) : D.t =
- check_lval ctx.ask ~ignore_var:true ctx.local lval;
- check_exp ctx.ask ctx.local rval;
- rem_lval ctx.ask ctx.local lval
-
- let branch ctx (exp:exp) (tv:bool) : D.t =
- check_exp ctx.ask ctx.local exp;
- ctx.local
-
- let body ctx (f:fundec) : D.t =
- ctx.local
-
let return ctx (exp:exp option) (f:fundec) : D.t =
- Option.may (check_exp ctx.ask ctx.local) exp;
(* remove locals, except ones which need to be weakly updated*)
if D.is_top ctx.local then
ctx.local
- else
- let locals = (f.sformals @ f.slocals) in
- let locals_noweak = List.filter (fun v_info -> not (ctx.ask (Queries.IsMultiple v_info))) locals in
- D.filter (fun v -> not (List.mem v locals_noweak)) ctx.local
+ else (
+ let locals = f.sformals @ f.slocals in
+ D.filter (fun v ->
+ not (List.exists (fun local ->
+ CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
+ ) locals)
+ ) ctx.local
+ )
let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
if VS.is_empty ctx.local then
[ctx.local,ctx.local]
- else
- (Option.may (check_lval ctx.ask ~ignore_var:true ctx.local) lval;
- List.iter (check_exp ctx.ask ctx.local) args;
- let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
- if Queries.LS.is_top reachable_from_args || VS.is_top ctx.local then
- [ctx.local, ctx.local]
- else
- let reachable_vars = Queries.LS.elements reachable_from_args |> List.map fst |> VS.of_list in
- [VS.diff ctx.local reachable_vars, VS.inter reachable_vars 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 =
- (* Actually, this ask would have to be on the post state?! *)
- Option.map_default (rem_lval ctx.ask au) (VS.join au ctx.local) lval
-
- let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
- Option.may (check_lval ctx.ask ~ignore_var:true ctx.local) lval;
- List.iter (check_exp ctx.ask ctx.local) arglist;
- Option.map_default (rem_lval ctx.ask ctx.local) ctx.local lval
+ else (
+ let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in
+ if Queries.LS.is_top reachable_from_args || VS.is_top ctx.local then
+ [ctx.local, ctx.local]
+ else
+ let reachable_vars =
+ Queries.LS.elements reachable_from_args
+ |> List.map fst
+ |> VS.of_list
+ in
+ [VS.diff ctx.local reachable_vars, VS.inter reachable_vars ctx.local]
+ )
+
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+ VS.join au 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 _ _ = ()
-
let event ctx e octx =
match e with
- | Events.Poison poisoned -> D.join poisoned ctx.local
+ | Events.Longjmped {lval} ->
+ let modified_locals = ctx.ask (MayBeModifiedSinceSetjmp (ctx.prev_node, ctx.control_context ())) in
+ let modified_locals = match lval with
+ | Some (Var v, NoOffset) -> Queries.VS.remove v modified_locals
+ | _ -> modified_locals (* Does usually not really occur, if it does, this is sound *)
+ in
+ let (_, longjmp_nodes) = ctx.ask ActiveJumpBuf in
+ JmpBufDomain.NodeSet.iter (fun longjmp_node ->
+ if Queries.VS.is_top modified_locals then
+ M.info ~category:(Behavior (Undefined Other)) ~loc:(Node longjmp_node) "Since setjmp at %a, potentially all locals were modified! Reading them will yield Undefined Behavior." Node.pretty ctx.prev_node
+ else if not (Queries.VS.is_empty modified_locals) then
+ M.info ~category:(Behavior (Undefined Other)) ~loc:(Node longjmp_node) "Since setjmp at %a, locals %a were modified! Reading them will yield Undefined Behavior." Node.pretty ctx.prev_node Queries.VS.pretty modified_locals
+ else
+ ()
+ ) longjmp_nodes;
+ D.join modified_locals ctx.local
+ | Access {lvals; kind = Read; _} ->
+ if Queries.LS.is_top lvals then (
+ if not (VS.is_empty octx.local) then
+ M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
+ )
+ else (
+ Queries.LS.iter (fun lv ->
+ (* Use original access state instead of current with removed written vars. *)
+ check_lval octx.local lv
+ ) lvals
+ );
+ ctx.local
+ | Access {lvals; kind = Write; _} ->
+ if Queries.LS.is_top lvals then
+ ctx.local
+ else (
+ Queries.LS.fold (fun lv acc ->
+ rem_lval acc lv
+ ) lvals ctx.local
+ )
| _ -> ctx.local
end
diff --git a/src/analyses/pthreadSignals.ml b/src/analyses/pthreadSignals.ml
index 001e3a7584..95dc25f9e7 100644
--- a/src/analyses/pthreadSignals.ml
+++ b/src/analyses/pthreadSignals.ml
@@ -50,7 +50,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 =
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index fb1938772f..b7730ad3e3 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -137,7 +137,7 @@ struct
[ctx.local, `Lifted reg]
| x -> [x,x]
- 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 =
match au with
| `Lifted reg -> begin
let old_regpart = ctx.global () in
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index e38a14a90f..1b2cce115e 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -414,7 +414,7 @@ struct
D.edit_callstack (BatList.cons (Option.get !Node.current_node)) ctx.local
else ctx.local in [m, m]
- 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 =
(* M.debug ~category:Analyzer @@ "leaving function "^f.vname^D.string_of_callstack au; *)
let au = D.edit_callstack List.tl au in
let return_val = D.find_option return_var au in
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index 1ad105231f..6adf367b2d 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -28,7 +28,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 =
ctx.local
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
@@ -64,7 +64,7 @@ struct
let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
[ctx.local, D.push !Tracing.current_loc 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 =
ctx.local
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 98bf4d7bd2..26038205fd 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -46,7 +46,7 @@ struct
List.fold_right D.remove_var (fundec.sformals@fundec.slocals) ctx.local
let enter ctx lval f args = [(ctx.local,ctx.local)]
- let combine ctx ?(longjmpthrough = false) lval fexp f args fc st2 f_ask = st2
+ let combine ctx lval fexp f args fc st2 f_ask = st2
let get_locks e st =
let add_perel x xs =
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 35508dacb6..f7eb266900 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -36,9 +36,18 @@ struct
let return ctx (exp:exp option) (f:fundec) : D.t =
(* remove locals, except ones which need to be weakly updated*)
let d = ctx.local in
- let locals = (f.sformals @ f.slocals) in
- let locals_noweak = List.filter (fun v_info -> not (ctx.ask (Queries.IsMultiple v_info))) locals in
- let d_return = if D.is_top d then d else D.filter (fun (v, _) -> not (List.mem v locals_noweak)) d in
+ let d_return =
+ if D.is_top d then
+ d
+ else (
+ let locals = f.sformals @ f.slocals in
+ D.filter (fun (v, _) ->
+ not (List.exists (fun local ->
+ CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
+ ) locals)
+ ) d
+ )
+ in
if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return;
d_return
@@ -47,7 +56,7 @@ struct
(* Entering a function, all globals count as untainted *)
[ctx.local, (D.bot ())]
- let combine ctx ?(longjmpthrough = false) (lvalOpt:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+ let combine ctx (lvalOpt:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
if M.tracing then M.trace "taintPC" "combine for %s in TaintPC: tainted: in function: %a before call: %a\n" f.svar.vname D.pretty au D.pretty ctx.local;
let d =
match lvalOpt with
diff --git a/src/analyses/termination.ml b/src/analyses/termination.ml
index 0fb344008d..4dc7ee74c7 100644
--- a/src/analyses/termination.ml
+++ b/src/analyses/termination.ml
@@ -226,7 +226,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 =
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index 28396dc7ca..54e28d7a80 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -34,7 +34,7 @@ struct
end;
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 combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = au
let rec is_not_unique ctx tid =
let (rep, parents, _) = ctx.global tid in
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index cff9071dfb..604413e653 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -87,7 +87,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) (args:exp list) : D.t =
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 747397194a..71ab0f1f98 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -49,7 +49,7 @@ struct
let enter ctx lval f args =
[ctx.local,ctx.local]
- let combine ctx ?(longjmpthrough = false) lval fexp f args fc st2 f_ask = st2
+ let combine ctx lval fexp f args fc st2 f_ask = st2
let special ctx lval f args =
ctx.local
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 32c7e431d2..970e4a0cd7 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -63,7 +63,7 @@ struct
let enter ctx lval f args =
[ctx.local,ctx.local]
- let combine ctx ?(longjmpthrough = false) lval fexp f args fc st2 f_ask = st2
+ let combine ctx lval fexp f args fc st2 f_ask = st2
let special ctx lval f args =
ctx.local
diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml
index 823fa93862..8c78ba84a8 100644
--- a/src/analyses/threadJoins.ml
+++ b/src/analyses/threadJoins.ml
@@ -87,7 +87,7 @@ struct
| Queries.MustJoinedThreads -> (ctx.local:ConcDomain.MustThreadSet.t) (* type annotation needed to avoid "would escape the scope of its equation" *)
| _ -> Queries.Result.top q
- let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
D.union ctx.local au
let startstate v = D.top ()
diff --git a/src/analyses/threadReturn.ml b/src/analyses/threadReturn.ml
index aa6c9cccff..bc1fc9da30 100644
--- a/src/analyses/threadReturn.ml
+++ b/src/analyses/threadReturn.ml
@@ -29,13 +29,13 @@ struct
ctx.local
let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
- if ctx.edge = MyCFG.Skip && ctx.node = MyCFG.dummy_node then
+ if !Goblintutil.global_initialization then
(* We are inside enter_with inside a startfun, and thus the current function retruning is the main function *)
[ctx.local, true]
else
[ctx.local, false]
- 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 =
ctx.local
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml
index f3a4d0ee94..8908545ce4 100644
--- a/src/analyses/tutorials/constants.ml
+++ b/src/analyses/tutorials/constants.ml
@@ -83,7 +83,7 @@ struct
)
|_ -> state
- 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 we have a function call with assignment
x = f (e1, ... , ek)
with a local int variable x on the left, we set it to top *)
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 64da50a469..023305b9d2 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -104,7 +104,7 @@ struct
(** For a function call "lval = f(args)" or "f(args)",
computes the state of the caller after the call.
Argument [callee_local] is the state of [f] at its return node. *)
- let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
let caller_state = ctx.local in
(* TODO: Record whether lval was tainted. *)
caller_state
diff --git a/src/analyses/tutorials/unitAnalysis.ml b/src/analyses/tutorials/unitAnalysis.ml
index 13385d71a8..af5c4f0d30 100644
--- a/src/analyses/tutorials/unitAnalysis.ml
+++ b/src/analyses/tutorials/unitAnalysis.ml
@@ -29,7 +29,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 =
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index eb5da6dfb8..4729258295 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -274,7 +274,7 @@ struct
let enter ctx lv f args =
[(ctx.local, D.empty ())]
- let combine ctx ?(longjmpthrough = false) lv fe f args fc fd f_ask =
+ let combine ctx lv fe f args fc fd f_ask =
emit_unassume ctx
(* not in sync, query, entry, threadenter because they aren't final transfer function on edge *)
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index 2cff4f58b4..22195985bd 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -261,7 +261,7 @@ struct
let nst = remove_unreachable (Analyses.ask_of_ctx ctx) args ctx.local in
[ctx.local, nst]
- let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : trans_out =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : trans_out =
ignore (List.map (fun x -> is_expr_initd (Analyses.ask_of_ctx ctx) x ctx.local) args);
let cal_st = remove_unreachable (Analyses.ask_of_ctx ctx) args ctx.local in
let ret_st = D.union au (D.diff ctx.local cal_st) in
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 5ef4b7412a..383ff69f2f 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -429,7 +429,7 @@ struct
| true -> raise Analyses.Deadcode
| false -> [ctx.local,nst]
- let combine ctx ?(longjmpthrough = false) lval fexp f args fc st2 (f_ask : Queries.ask) =
+ let combine ctx lval fexp f args fc st2 (f_ask : Queries.ask) =
let tainted = f_ask.f Queries.MayBeTainted in
let d_local =
(* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
diff --git a/src/analyses/vla.ml b/src/analyses/vla.ml
index a159cf4209..1cc67dc282 100644
--- a/src/analyses/vla.ml
+++ b/src/analyses/vla.ml
@@ -5,46 +5,36 @@ open Analyses
module Spec =
struct
- include Analyses.DefaultSpec
+ include Analyses.IdentitySpec
let name () = "vla"
module D = BoolDomain.MayBool
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 context _ _ = ()
let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
[ctx.local, false]
- 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 =
ctx.local
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
- ctx.local
-
- let vdecl ctx (v:varinfo) : D.t = true
+ match (LibraryFunctions.find f).special arglist with
+ | Setjmp _ ->
+ (* Checking if this within the scope of an identifier of variably modified type *)
+ if ctx.local then
+ M.warn ~category:(Behavior (Undefined Other)) "setjmp called within the scope of a variably modified type. If a call to longjmp is made after this scope is left, the behavior is undefined.";
+ ctx.local
+ | _ ->
+ ctx.local
+
+ let vdecl ctx (v:varinfo) : D.t =
+ ctx.local || Cilfacade.isVLAType v.vtype
let startstate v = D.bot ()
let threadenter ctx lval f args = [D.top ()]
- let threadspawn ctx lval f args fctx = ctx.local
let exitstate v = D.top ()
- let context _ _ = ()
-
- let query ctx (type a) (q: a Queries.t): a Queries.result =
- match q with
- | MayBeInVLAScope -> (ctx.local:bool) (* Will not compile without annotation *)
- | _ -> Queries.Result.top q
end
let _ =
diff --git a/src/cdomains/jmpBufDomain.ml b/src/cdomains/jmpBufDomain.ml
index f0b22ad525..e5c3c96e74 100644
--- a/src/cdomains/jmpBufDomain.ml
+++ b/src/cdomains/jmpBufDomain.ml
@@ -1,4 +1,4 @@
-module BufferEntry = Printable.ProdSimple(Node)(IntDomain.Flattened)
+module BufferEntry = Printable.ProdSimple(Node)(ControlSpecC)
module BufferEntryOrTop = struct
include Printable.Std
diff --git a/src/domains/events.ml b/src/domains/events.ml
index ece1f96bce..4b96e1c1b0 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -12,7 +12,7 @@ type t =
| UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
| Assert of exp
| Unassume of {exp: CilType.Exp.t; uuids: string list}
- | Poison of Queries.VS.t
+ | Longjmped of {lval: CilType.Lval.t option}
(** Should event be emitted after transfer function raises [Deadcode]? *)
let emit_on_deadcode = function
@@ -28,7 +28,7 @@ let emit_on_deadcode = function
| UpdateExpSplit _ (* Pointless to split on dead. *)
| Unassume _ (* Avoid spurious writes. *)
| Assert _ (* Pointless to refine dead. *)
- | Poison _ -> (* TODO: correct? *)
+ | Longjmped _ ->
false
let pretty () = function
@@ -43,4 +43,4 @@ let pretty () = function
| UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
| Assert exp -> dprintf "Assert %a" d_exp exp
| Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
- | Poison vars -> dprintf "Poison %a" Queries.VS.pretty vars
+ | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 69943dade5..f6632610ea 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -130,7 +130,6 @@ type _ t =
| MayAccessed: AccessDomain.EventSet.t t
| MayBeTainted: LS.t t
| MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t
- | MayBeInVLAScope: MayBool.t t
type 'a result = 'a
@@ -191,7 +190,6 @@ struct
| MayAccessed -> (module AccessDomain.EventSet)
| MayBeTainted -> (module LS)
| MayBeModifiedSinceSetjmp _ -> (module VS)
- | MayBeInVLAScope -> (module MayBool)
(** Get bottom result for query. *)
let bot (type a) (q: a t): a result =
@@ -251,7 +249,6 @@ struct
| MayAccessed -> AccessDomain.EventSet.top ()
| MayBeTainted -> LS.top ()
| MayBeModifiedSinceSetjmp _ -> VS.top ()
- | MayBeInVLAScope -> MayBool.top ()
end
(* The type any_query can't be directly defined in Any as t,
@@ -308,7 +305,6 @@ struct
| Any ActiveJumpBuf -> 46
| Any ValidLongJmp -> 47
| Any (MayBeModifiedSinceSetjmp _) -> 48
- | Any MayBeInVLAScope -> 49
let rec compare a b =
let r = Stdlib.compare (order a) (order b) in
@@ -439,7 +435,6 @@ struct
| Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
| Any DYojson -> Pretty.dprintf "DYojson"
| Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf
- | Any MayBeInVLAScope -> Pretty.dprintf "MayBeInVLAScope"
end
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 9a6ead3616..9eead26aa4 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -394,7 +394,7 @@ sig
val special : (D.t, G.t, C.t, V.t) ctx -> lval option -> varinfo -> exp list -> D.t
val enter : (D.t, G.t, C.t, V.t) ctx -> lval option -> fundec -> exp list -> (D.t * D.t) list
- val combine : (D.t, G.t, C.t, V.t) ctx -> ?longjmpthrough:bool -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
+ val combine : (D.t, G.t, C.t, V.t) ctx -> lval option -> exp -> fundec -> exp list -> C.t option -> D.t -> Queries.ask -> D.t
(* Paths as sets: I know this is ugly! *)
val paths_as_set : (D.t, G.t, C.t, V.t) ctx -> D.t list
@@ -635,7 +635,7 @@ struct
let enter ctx (lval: lval option) (f:fundec) (args:exp list) =
[ctx.local, ctx.local]
- let combine ctx ?(longjmpthrough = false) (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
+ let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc au (f_ask: Queries.ask) =
au
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) =
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
index 7b717bd18d..2792d1b92e 100644
--- a/src/framework/cfgTools.ml
+++ b/src/framework/cfgTools.ml
@@ -525,10 +525,8 @@ struct
in
let shape = match n with
| Statement {skind=If (_,_,_,_,_); _} -> ["shape=diamond"]
- | Statement _
- | LongjmpTo _ -> [] (* use default shape *)
+ | Statement _ -> [] (* use default shape *)
| Function _
- | LongjmpFromFunction _
| FunctionEntry _ -> ["shape=box"]
in
let styles = String.concat "," (label @ shape @ extraNodeStyles n) in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 3dd98e1f3b..602a5ddf5e 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -73,8 +73,8 @@ struct
let special ctx r f args =
D.lift @@ S.special (conv ctx) r f args
- let combine ctx ?(longjmpthrough = false) r fe f args fc es f_ask =
- D.lift @@ S.combine (conv ctx) ~longjmpthrough r fe f args fc (D.unlift es) f_ask
+ let combine ctx r fe f args fc es f_ask =
+ D.lift @@ S.combine (conv ctx) r fe f args fc (D.unlift es) f_ask
let threadenter ctx lval f args =
List.map D.lift @@ S.threadenter (conv ctx) lval f args
@@ -155,8 +155,8 @@ struct
let special ctx r f args =
S.special (conv ctx) r f args
- let combine ctx ?(longjmpthrough = false) r fe f args fc es f_ask =
- S.combine (conv ctx) ~longjmpthrough r fe f args (Option.map C.unlift fc) es f_ask
+ let combine ctx r fe f args fc es f_ask =
+ S.combine (conv ctx) r fe f args (Option.map C.unlift fc) es f_ask
let threadenter ctx lval f args =
S.threadenter (conv ctx) lval f args
@@ -234,7 +234,7 @@ struct
let asm ctx = lift_fun ctx (lift ctx) S.asm identity
let skip ctx = lift_fun ctx (lift ctx) S.skip identity
let special ctx r f args = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
- let combine' ctx ?(longjmpthrough = false) r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine (fun p -> p ~longjmpthrough r fe f args fc (fst es) f_ask)
+ let combine' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine (fun p -> p r fe f args fc (fst es) f_ask)
let threadenter ctx lval f args = lift_fun ctx (List.map lift_start_level) S.threadenter ((|>) args % (|>) f % (|>) lval)
let threadspawn ctx lval f args fctx = lift_fun ctx (lift ctx) S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
@@ -266,13 +266,13 @@ struct
else
enter' {ctx with local=(d, sub1 l)} r f args
- let combine ctx ?(longjmpthrough = false) r fe f args fc es f_ask =
+ let combine ctx r fe f args fc es f_ask =
let (d,l) = ctx.local in
let l = add1 l in
if leq0 l then
(d, l)
else
- let d',_ = combine' ctx ~longjmpthrough r fe f args fc es f_ask in
+ let d',_ = combine' ctx r fe f args fc es f_ask in
(d', l)
let query ctx (type a) (q: a Queries.t): a Queries.result =
@@ -391,7 +391,7 @@ struct
let m = snd ctx.local in
S.paths_as_set (conv ctx) |> List.map (fun v -> (v,m))
- let combine ctx ?(longjmpthrough = false) r fe f args fc es f_ask = lift_fun ctx S.combine (fun p -> p ~longjmpthrough r fe f args fc (fst es) f_ask)
+ let combine ctx r fe f args fc es f_ask = lift_fun ctx S.combine (fun p -> p r fe f args fc (fst es) f_ask)
end
@@ -453,7 +453,7 @@ struct
let asm ctx = lift_fun ctx D.lift S.asm identity `Bot
let skip ctx = lift_fun ctx D.lift S.skip identity `Bot
let special ctx r f args = lift_fun ctx D.lift S.special ((|>) args % (|>) f % (|>) r) `Bot
- let combine ctx ?(longjmpthrough = false) r fe f args fc es f_ask = lift_fun ctx D.lift S.combine (fun p -> p ~longjmpthrough r fe f args fc (D.unlift es) f_ask) `Bot
+ let combine ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot
let threadenter ctx lval f args = lift_fun ctx (List.map D.lift) S.threadenter ((|>) args % (|>) f % (|>) lval) []
let threadspawn ctx lval f args fctx = lift_fun ctx D.lift S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval) `Bot
@@ -645,211 +645,56 @@ struct
common_join ctx (S.branch ctx e tv) !r !spawns
let tf_normal_call ctx lv e (f:fundec) args getl sidel getg sideg =
- let jmptarget = function
- | Statement s -> LongjmpTo s
- | _ -> failwith "should not happen"
- in
- let current_fundec = Node.find_fundec ctx.node in
let combine (cd, fc, fd) =
if M.tracing then M.traceli "combine" "local: %a\n" S.D.pretty cd;
- (* Extra sync in case function has multiple returns.
- Each `Return sync is done before joining, so joined value may be unsound.
- Since sync is normally done before tf (in common_ctx), simulate it here for fd. *)
- (* TODO: don't do this extra sync here *)
- let rec sync_ctx = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
- local = fd;
- prev_node = Function f
- }
+ let rec cd_ctx =
+ { ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query cd_ctx q);
+ local = cd;
+ }
+ in
+ let fd_ctx =
+ (* Inner scope to prevent unsynced fd_ctx from being used. *)
+ (* Extra sync in case function has multiple returns.
+ Each `Return sync is done before joining, so joined value may be unsound.
+ Since sync is normally done before tf (in common_ctx), simulate it here for fd. *)
+ (* TODO: don't do this extra sync here *)
+ let rec sync_ctx =
+ { ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
+ local = fd;
+ prev_node = Function f;
+ }
+ in
+ (* TODO: more accurate ctx? *)
+ let synced = sync sync_ctx in
+ let rec fd_ctx =
+ { sync_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query fd_ctx q);
+ local = synced;
+ }
+ in
+ fd_ctx
in
- (* TODO: more accurate ctx? *)
- let fd = sync sync_ctx in
if M.tracing then M.trace "combine" "function: %a\n" S.D.pretty fd;
- let r = S.combine {ctx with local = cd} lv e f args fc fd (Analyses.ask_of_ctx sync_ctx) in
+ let r = S.combine cd_ctx lv e f args fc fd_ctx.local (Analyses.ask_of_ctx fd_ctx) in
if M.tracing then M.traceu "combine" "combined local: %a\n" S.D.pretty r;
r
in
- let handlelongjmp (cd,fc,fd) =
- let rec ctx_fd = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query ctx_fd q);
- local = fd;
- prev_node = Function f
- }
- in
- let rec ctx_cd = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query ctx_cd q);
- local = cd}
- in
- (* Set of jumptargets with which the callee may return here *)
- let targets = fst @@ ctx_fd.ask ActiveJumpBuf in
- (* Handle a longjmp to targetnode in targetcontext *)
- let handle_longjmp = function
- | JmpBufDomain.BufferEntryOrTop.AllTargets -> () (* The warning is already emitted at the point where the longjmp happens *)
- | Target (targetnode, targetcontext) ->
- let target_in_caller () = CilType.Fundec.equal (Node.find_fundec targetnode) current_fundec in
- let targetcontext_matches () =
- let controlctx = ControlSpecC.hash (ctx.control_context ()) in
- targetcontext = IntDomain.Flattened.of_int (Int64.of_int controlctx)
- in
- (* Check if corresponding setjmp call was in current function & in current context *)
- if targetcontext_matches () && target_in_caller () then
- (if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %s\n" (Node.show targetnode);
- match targetnode with
- | Statement { skind = Instr [Call (setjmplval, _, setjmpargs,_, _)] ;_ } ->
- let fd' = S.return ctx_fd None f in
- let rec ctx_fd' = { ctx_fd with
- ask = (fun (type a) (q: a Queries.t) -> S.query ctx_fd' q);
- local = fd';
- prev_node = Function f
- }
- in
- (* Using f from called function on purpose here! Needed? *)
- let value = S.combine ctx_cd setjmplval (Cil.one) f setjmpargs fc fd' (Analyses.ask_of_ctx ctx_fd') in
- let rec res_ctx = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query res_ctx q);
- local = value
- }
- in
- let setjmpvar = match setjmplval with
- | Some (Var v, NoOffset) -> Queries.VS.singleton v
- | _ -> Queries.VS.empty () (* Does usually not really occur, if it does, this is sound *)
- in
- let modified_vars = Queries.VS.diff (res_ctx.ask (MayBeModifiedSinceSetjmp (targetnode, targetcontext))) setjmpvar in
- (if Queries.VS.is_top modified_vars then
- M.warn "Information: Since setjmp at %s, potentially all locals were modified! Acessing them will yield Undefined Behavior." (Node.show targetnode)
- else if not (Queries.VS.is_empty modified_vars) then
- M.warn "Information: Since setjmp at %s, locals %s were modified! Acessing them will yield Undefined Behavior." (Node.show targetnode) (Queries.VS.show modified_vars)
- else
- ()
- );
- let value' = S.event res_ctx (Events.Poison modified_vars) res_ctx in
- sidel (jmptarget targetnode, ctx.context ()) value'
- (* No need to propagate this outwards here, the set of valid longjumps is part of the context, we can never have the same context setting the longjmp multiple times *)
- | _ -> failwith "target of longjmp is node that is not a call to setjmp!")
- else
- (* Appropriate setjmp is not in current function & current context *)
- let validBuffers = ctx_cd.ask ValidLongJmp in
- if not (JmpBufDomain.JmpBufSet.mem (Target (targetnode,targetcontext)) validBuffers) then
- (* It actually is not handled here but was propagated her spuriously, we already warned at the location where this issue is caused *)
- (* As the validlongjumps inside the callee is a a superset of the ones inside the caller*)
- ()
- else
- (if M.tracing then Messages.tracel "longjmp" "Fun: Longjmp to somewhere else\n";
- (* Globals are non-problematic here, as they are always carried around without any issues! *)
- (* A combine call is mostly needed to ensure locals have appropriate values. *)
- let fd' = S.return ctx_fd None f in
- let rec ctx_fd' = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query ctx_fd' q);
- local = fd';
- prev_node = Function f
- }
- in
- let value = S.combine ctx_cd ~longjmpthrough:true None (Cil.one) f [] None fd' (Analyses.ask_of_ctx ctx_fd') in
- sidel (LongjmpFromFunction current_fundec, ctx.context ()) value)
- in
- JmpBufDomain.JmpBufSet.iter handle_longjmp targets
- in
- (* Handle normal calls to function *)
let paths = S.enter ctx lv f args in
- let ld_fc_fd_list = List.map (fun (c,v) -> (c, S.context f v, v)) paths in
- List.iter (fun (c,fc,v) -> if not (S.D.is_bot v) then sidel (FunctionEntry f, fc) v) ld_fc_fd_list;
- let paths = List.map (fun (c,fc,v) -> (c, fc, if S.D.is_bot v then v else getl (Function f, fc))) ld_fc_fd_list in
- let paths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) paths in
+ let paths = List.map (fun (c,v) -> (c, S.context f v, v)) paths in
+ List.iter (fun (c,fc,v) -> if not (S.D.is_bot v) then sidel (FunctionEntry f, fc) v) paths;
+ let paths = List.map (fun (c,fc,v) -> (c, fc, if S.D.is_bot v then v else getl (Function f, fc))) paths in
+ (* Don't filter bot paths, otherwise LongjmpLifter is not called. *)
+ (* let paths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) paths in *)
let paths = List.map (Tuple3.map2 Option.some) paths in
if M.tracing then M.traceli "combine" "combining\n";
let paths = List.map combine paths in
- let result = List.fold_left D.join (D.bot ()) paths in
- if M.tracing then M.traceu "combine" "combined: %a\n" S.D.pretty result;
- (* Handle "longjumpy" ;p returns from this function by producing appropriate side-effects *)
- let longjmpv fc v = if S.D.is_bot v then v else (if Messages.tracing then Messages.tracel "longjmp" "asking for side-effect to %i\n" (S.C.hash fc); getl (LongjmpFromFunction f, fc)) in
- let longjmppaths = List.map (fun (c,fc,v) -> (c, fc, longjmpv fc v)) ld_fc_fd_list in
- let longjmppaths = List.filter (fun (c,fc,v) -> not (D.is_bot v)) longjmppaths in
- let longjmppaths = List.map (Tuple3.map2 Option.some) longjmppaths in
- let _ = List.iter handlelongjmp longjmppaths in
- (* Return result of normal call, longjmp om;y happens via side-effect *)
- result
-
- let tf_special_call ctx (getl: lv -> ld) (sidel: lv -> ld -> unit) lv f args =
- let jmptarget = function
- | Statement s -> LongjmpTo s
- | _ -> failwith "should not happen"
- in
- match (LibraryFunctions.find f).special args with
- | Setjmp { env; savesigs} ->
- (* Checking if this within the scope of an identifier of variably modified type *)
- if ctx.ask Queries.MayBeInVLAScope then (
- M.warn "setjmp called within the scope of a variably modified type. If a call to longjmp is made after this scope is left, the behavior is undefined.";
- );
- (* Handling of returning for the first time *)
- let first_return = S.special ctx lv f args in
- if M.tracing then Messages.tracel "longjmp" "reading from %s\n" (Node.show (jmptarget ctx.prev_node));
- let later_return = getl (jmptarget ctx.prev_node, ctx.context ()) in
- if not @@ S.D.is_bot later_return then
- S.D.join first_return later_return
- else
- first_return
- | Longjmp {env; value; sigrestore} ->
- let res = S.special ctx lv f args in
- let current_fundec = Node.find_fundec ctx.node in
- let one_path s = (
- let rec path_ctx = { ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query path_ctx q);
- local = s;
- }
- in
- (* Eval `env` again to avoid having to construct bespoke ctx to ask *)
- let targets = path_ctx.ask (EvalJumpBuf env) in
- if M.tracing then Messages.tracel "longjmp" "Jumping to %a\n" JmpBufDomain.JmpBufSet.pretty targets;
- let handle_longjmp = function
- | JmpBufDomain.BufferEntryOrTop.AllTargets ->
- M.warn "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env
- | JmpBufDomain.BufferEntryOrTop.Target (node, c) ->
- let validBuffers = path_ctx.ask ValidLongJmp in
- if not (JmpBufDomain.JmpBufSet.mem (Target (node,c)) validBuffers) then
- M.warn "Longjmp to potentially invalid target! (Target %s in Function %s which may have already returned or is in a different thread)" (Node.show node) (Node.find_fundec node).svar.vname
- else
- (let controlctx = ControlSpecC.hash (ctx.control_context ()) in
- if c = IntDomain.Flattened.of_int (Int64.of_int controlctx) && (Node.find_fundec node).svar.vname = current_fundec.svar.vname then
- (if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %s\n" (Node.show node);
- match node with
- | Statement { skind = Instr [Call (lval, exp, args,_, _)] ;_ } ->
- (* TODO: this assign is wrong: if value is definitely 0, then it is changed and should assign 1 instead *)
- (* non-local longjmp does this in base special, but base assign does not *)
- let res' = Option.map_default (fun lv -> S.assign path_ctx lv value) s lval in
- let setjmpvar = match lval with
- | Some (Var v, NoOffset) -> Queries.VS.singleton v
- | _ -> Queries.VS.empty () (* Does usually not really occur, if it does, this is sound *)
- in
- let modified_vars = Queries.VS.diff (path_ctx.ask (MayBeModifiedSinceSetjmp (node, c))) setjmpvar in
- (if Queries.VS.is_top modified_vars then
- M.warn "Information: Since setjmp at %s, potentially all locals were modified! Acessing them will yield Undefined Behavior." (Node.show node)
- else if not (Queries.VS.is_empty modified_vars) then
- M.warn "Information: Since setjmp at %s, locals %s were modified! Acessing them will yield Undefined Behavior." (Node.show node) (Queries.VS.show modified_vars)
- else
- ()
- );
- let rec res_ctx = { path_ctx with
- ask = (fun (type a) (q: a Queries.t) -> S.query res_ctx q);
- local = res';
- }
- in
- let r = S.event res_ctx (Events.Poison modified_vars) res_ctx in
- sidel (jmptarget node, ctx.context ()) r
- | _ -> failwith (Printf.sprintf "strange: %s" (Node.show node))
- )
- else
- (if M.tracing then Messages.tracel "longjmp" "Longjmp to somewhere else, side-effect to %i\n" (S.C.hash (ctx.context ()));
- sidel (LongjmpFromFunction current_fundec, ctx.context ()) res))
- in
- if JmpBufDomain.JmpBufSet.is_empty targets then
- M.warn "Longjmp to potentially invalid target (%a is bot?!)" d_exp env
- else
- JmpBufDomain.JmpBufSet.iter handle_longjmp targets
- )
- in
- List.iter one_path (S.paths_as_set ctx);
- S.D.bot ()
- | _ -> S.special ctx lv f args
+ let r = List.fold_left D.join (D.bot ()) paths in
+ if M.tracing then M.traceu "combine" "combined: %a\n" S.D.pretty r;
+ r
+
+ let tf_special_call ctx lv f args = S.special ctx lv f args
let tf_proc var edge prev_node lv e args getl sidel getg sideg d =
let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
@@ -875,11 +720,11 @@ struct
begin Some (match Cilfacade.find_varinfo_fundec f with
| fd when LibraryFunctions.use_special f.vname ->
M.info ~category:Analyzer "Using special for defined function %s" f.vname;
- tf_special_call ctx getl sidel lv f args
+ tf_special_call ctx lv f args
| fd ->
tf_normal_call ctx lv e fd args getl sidel getg sideg
| exception Not_found ->
- tf_special_call ctx getl sidel lv f args)
+ tf_special_call ctx lv f args)
end
else begin
let geq = if var_arg then ">=" else "" in
@@ -966,10 +811,6 @@ struct
match v with
| FunctionEntry _ ->
None
- | LongjmpTo _ ->
- None
- | LongjmpFromFunction _ ->
- None
| _ ->
let tf getl sidel getg sideg =
let tf' eu = tf (v,c) eu getl sidel getg sideg in
@@ -1396,13 +1237,13 @@ struct
let elems = D.elements ctx.local in
List.map (D.singleton) elems
- let combine ctx ?(longjmpthrough = false) l fe f a fc d f_ask =
+ let combine ctx l fe f a fc d f_ask =
assert (D.cardinal ctx.local = 1);
let cd = D.choose ctx.local in
let k x y =
if M.tracing then M.traceli "combine" "function: %a\n" Spec.D.pretty x;
try
- let r = Spec.combine (conv ctx cd) ~longjmpthrough l fe f a fc x f_ask in
+ let r = Spec.combine (conv ctx cd) l fe f a fc x f_ask in
if M.tracing then M.traceu "combine" "combined function: %a\n" Spec.D.pretty r;
D.add r y
with Deadcode ->
@@ -1534,7 +1375,7 @@ struct
let paths_as_set ctx = S.paths_as_set (conv ctx)
let body ctx = S.body (conv ctx)
let return ctx = S.return (conv ctx)
- let combine ctx ?(longjmpthrough = false) = S.combine (conv ctx) ~longjmpthrough
+ let combine ctx = S.combine (conv ctx)
let special ctx = S.special (conv ctx)
let threadenter ctx = S.threadenter (conv ctx)
let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
@@ -1544,6 +1385,239 @@ struct
let event ctx e octx = S.event (conv ctx) e (conv octx)
end
+module LongjmpLifter (S: Spec): Spec =
+struct
+ include S
+
+ let name () = "Longjmp (" ^ S.name () ^ ")"
+
+ module V =
+ struct
+ include Printable.Either (S.V) (Printable.Either (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C)))
+ let s x = `Left x
+ let longjmpto x = `Right (`Left x)
+ let longjmpret x = `Right (`Right x)
+ let is_write_only = function
+ | `Left x -> S.V.is_write_only x
+ | `Right _ -> false
+ end
+
+ module G =
+ struct
+ include Lattice.Lift2 (S.G) (S.D) (Printable.DefaultNames)
+
+ let s = function
+ | `Bot -> S.G.bot ()
+ | `Lifted1 x -> x
+ | _ -> failwith "LongjmpLifter.s"
+ let local = function
+ | `Bot -> S.D.bot ()
+ | `Lifted2 x -> x
+ | _ -> failwith "LongjmpLifter.local"
+ let create_s s = `Lifted1 s
+ let create_local local = `Lifted2 local
+
+ let printXml f = function
+ | `Lifted1 x -> S.G.printXml f x
+ | `Lifted2 x -> BatPrintf.fprintf f "%a" S.D.printXml x
+ | x -> BatPrintf.fprintf f "%a" printXml x
+ end
+
+ let conv (ctx: (_, G.t, _, V.t) ctx): (_, S.G.t, _, S.V.t) ctx =
+ { ctx with
+ global = (fun v -> G.s (ctx.global (V.s v)));
+ sideg = (fun v g -> ctx.sideg (V.s v) (G.create_s g));
+ }
+
+ let query ctx (type a) (q: a Queries.t): a Queries.result =
+ match q with
+ | WarnGlobal g ->
+ let g: V.t = Obj.obj g in
+ begin match g with
+ | `Left g ->
+ S.query (conv ctx) (WarnGlobal (Obj.repr g))
+ | `Right g ->
+ Queries.Result.top q
+ end
+ | InvariantGlobal g ->
+ let g: V.t = Obj.obj g in
+ begin match g with
+ | `Left g ->
+ S.query (conv ctx) (InvariantGlobal (Obj.repr g))
+ | `Right g ->
+ Queries.Result.top q
+ end
+ | IterSysVars (vq, vf) ->
+ (* vars for S *)
+ let vf' x = vf (Obj.repr (V.s (Obj.obj x))) in
+ S.query (conv ctx) (IterSysVars (vq, vf'));
+ (* TODO: vars? *)
+ | _ ->
+ S.query (conv ctx) q
+
+
+ let branch ctx = S.branch (conv ctx)
+ let assign ctx = S.assign (conv ctx)
+ let vdecl ctx = S.vdecl (conv ctx)
+ let enter ctx = S.enter (conv ctx)
+ let paths_as_set ctx = S.paths_as_set (conv ctx)
+ let body ctx = S.body (conv ctx)
+ let return ctx = S.return (conv ctx)
+
+ let combine ctx lv e f args fc fd f_ask =
+ let conv_ctx = conv ctx in
+ let current_fundec = Node.find_fundec ctx.node in
+ let handle_longjmp (cd, fc, longfd) =
+ (* This is called per-path. *)
+ let rec cd_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query cd_ctx q);
+ local = cd;
+ }
+ in
+ let longfd_ctx =
+ (* Inner scope to prevent unsynced longfd_ctx from being used. *)
+ (* Extra sync like with normal combine. *)
+ let rec sync_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);
+ local = longfd;
+ prev_node = Function f;
+ }
+ in
+ let synced = S.sync sync_ctx `Join in
+ let rec longfd_ctx =
+ { sync_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query longfd_ctx q);
+ local = synced;
+ }
+ in
+ longfd_ctx
+ in
+ let combined = lazy ( (* does not depend on target, do at most once *)
+ (* Globals are non-problematic here, as they are always carried around without any issues! *)
+ (* A combine call is mostly needed to ensure locals have appropriate values. *)
+ (* Using f from called function on purpose here! Needed? *)
+ S.combine cd_ctx None e f args fc longfd_ctx.local (Analyses.ask_of_ctx longfd_ctx) (* no lval because longjmp return skips return value assignment *)
+ )
+ in
+ let returned = lazy ( (* does not depend on target, do at most once *)
+ let rec combined_ctx =
+ { cd_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query combined_ctx q);
+ local = Lazy.force combined;
+ }
+ in
+ S.return combined_ctx None current_fundec
+ )
+ in
+ let (active_targets, _) = longfd_ctx.ask ActiveJumpBuf in
+ let valid_targets = cd_ctx.ask ValidLongJmp in
+ let handle_target target = match target with
+ | JmpBufDomain.BufferEntryOrTop.AllTargets -> () (* The warning is already emitted at the point where the longjmp happens *)
+ | Target (target_node, target_context) ->
+ let target_fundec = Node.find_fundec target_node in
+ if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (
+ if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %a\n" Node.pretty target_node;
+ ctx.sideg (V.longjmpto (target_node, ctx.context ())) (G.create_local (Lazy.force combined))
+ (* No need to propagate this outwards here, the set of valid longjumps is part of the context, we can never have the same context setting the longjmp multiple times *)
+ )
+ (* Appropriate setjmp is not in current function & current context *)
+ else if JmpBufDomain.JmpBufSet.mem target valid_targets then
+ ctx.sideg (V.longjmpret (current_fundec, ctx.context ())) (G.create_local (Lazy.force returned))
+ else
+ (* It actually is not handled here but was propagated here spuriously, we already warned at the location where this issue is caused *)
+ (* As the validlongjumps inside the callee is a a superset of the ones inside the caller *)
+ ()
+ in
+ JmpBufDomain.JmpBufSet.iter handle_target active_targets
+ in
+ if M.tracing then M.tracel "longjmp" "longfd getg %a\n" CilType.Fundec.pretty f;
+ let longfd = G.local (ctx.global (V.longjmpret (f, Option.get fc))) in
+ if M.tracing then M.tracel "longjmp" "longfd %a\n" D.pretty longfd;
+ if not (D.is_bot longfd) then
+ handle_longjmp (ctx.local, fc, longfd);
+ S.combine (conv_ctx) lv e f args fc fd f_ask
+
+ let special ctx lv f args =
+ let conv_ctx = conv ctx in
+ match (LibraryFunctions.find f).special args with
+ | Setjmp {env} ->
+ (* Handling of returning for the first time *)
+ let normal_return = S.special conv_ctx lv f args in
+ let jmp_return = G.local (ctx.global (V.longjmpto (ctx.prev_node, ctx.context ()))) in
+ if S.D.is_bot jmp_return then
+ normal_return
+ else (
+ let rec jmp_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query jmp_ctx q);
+ local = jmp_return;
+ }
+ in
+ let longjmped = S.event jmp_ctx (Events.Longjmped {lval=lv}) jmp_ctx in
+ S.D.join normal_return longjmped
+ )
+ | Longjmp {env; value} ->
+ let current_fundec = Node.find_fundec ctx.node in
+ let handle_path path = (
+ let rec path_ctx =
+ { conv_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query path_ctx q);
+ local = path;
+ }
+ in
+ let specialed = lazy ( (* does not depend on target, do at most once *)
+ S.special path_ctx lv f args
+ )
+ in
+ let returned = lazy ( (* does not depend on target, do at most once *)
+ let rec specialed_ctx =
+ { path_ctx with
+ ask = (fun (type a) (q: a Queries.t) -> S.query specialed_ctx q);
+ local = Lazy.force specialed;
+ }
+ in
+ S.return specialed_ctx None current_fundec
+ )
+ in
+ (* Eval `env` again to avoid having to construct bespoke ctx to ask *)
+ let targets = path_ctx.ask (EvalJumpBuf env) in
+ let valid_targets = path_ctx.ask ValidLongJmp in
+ if M.tracing then Messages.tracel "longjmp" "Jumping to %a\n" JmpBufDomain.JmpBufSet.pretty targets;
+ let handle_target target = match target with
+ | JmpBufDomain.BufferEntryOrTop.AllTargets ->
+ M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env
+ | Target (target_node, target_context) ->
+ let target_fundec = Node.find_fundec target_node in
+ if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (ctx.control_context ()) then (
+ if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %a\n" Node.pretty target_node;
+ ctx.sideg (V.longjmpto (target_node, ctx.context ())) (G.create_local (Lazy.force specialed))
+ )
+ else if JmpBufDomain.JmpBufSet.mem target valid_targets then (
+ if M.tracing then Messages.tracel "longjmp" "Longjmp to somewhere else, side-effect to %i\n" (S.C.hash (ctx.context ()));
+ ctx.sideg (V.longjmpret (current_fundec, ctx.context ())) (G.create_local (Lazy.force returned))
+ )
+ else
+ M.warn ~category:(Behavior (Undefined Other)) "Longjmp to potentially invalid target! (Target %a in Function %a which may have already returned or is in a different thread)" Node.pretty target_node CilType.Fundec.pretty target_fundec
+ in
+ if JmpBufDomain.JmpBufSet.is_empty targets then
+ M.warn ~category:(Behavior (Undefined Other)) "Longjmp to potentially invalid target (%a is bot?!)" d_exp env
+ else
+ JmpBufDomain.JmpBufSet.iter handle_target targets
+ )
+ in
+ List.iter handle_path (S.paths_as_set conv_ctx);
+ S.D.bot ()
+ | _ -> S.special conv_ctx lv f args
+ let threadenter ctx = S.threadenter (conv ctx)
+ let threadspawn ctx lv f args fctx = S.threadspawn (conv ctx) lv f args (conv fctx)
+ let sync ctx = S.sync (conv ctx)
+ let skip ctx = S.skip (conv ctx)
+ let asm ctx = S.asm (conv ctx)
+ let event ctx e octx = S.event (conv ctx) e (conv octx)
+end
+
module CompareGlobSys (SpecSys: SpecSys) =
struct
open SpecSys
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 2d18814ad2..656f8883bb 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -33,6 +33,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
(* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
|> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
+ |> lift true (module LongjmpLifter)
) in
GobConfig.building_spec := false;
ControlSpecC.control_spec_c := (module S1.C);
diff --git a/src/framework/myCFG.ml b/src/framework/myCFG.ml
index e3fa6c5c52..ad8ce433a3 100644
--- a/src/framework/myCFG.ml
+++ b/src/framework/myCFG.ml
@@ -5,10 +5,8 @@ open GoblintCil
(** Re-exported [Node.t] with constructors. See [Node.t] for documentation. *)
type node = Node.t =
| Statement of CilType.Stmt.t
- | LongjmpTo of CilType.Stmt.t
| FunctionEntry of CilType.Fundec.t
| Function of CilType.Fundec.t
- | LongjmpFromFunction of CilType.Fundec.t
(** Re-exported [Edge.t] with constructors. See [Edge.t] for documentation. *)
type edge = Edge.t =
diff --git a/src/framework/node.ml b/src/framework/node.ml
index f01f6eed48..451c2d6db3 100644
--- a/src/framework/node.ml
+++ b/src/framework/node.ml
@@ -11,26 +11,20 @@ let name () = "node"
(** Pretty node plainly with entire stmt. *)
let pretty_plain () = function
| Statement s -> text "Statement " ++ dn_stmt () s
- | LongjmpTo s -> text "LongjmpTo Statement" ++ dn_stmt () s
| Function f -> text "Function " ++ text f.svar.vname
- | LongjmpFromFunction f -> text "Longjmp from Function " ++ text f.svar.vname
| FunctionEntry f -> text "FunctionEntry " ++ text f.svar.vname
(* TODO: remove this? *)
(** Pretty node plainly with stmt location. *)
let pretty_plain_short () = function
| Statement s -> text "Statement @ " ++ CilType.Location.pretty () (Cilfacade.get_stmtLoc s)
- | LongjmpTo s -> text "LongjmpTo Statement @ " ++ CilType.Location.pretty () (Cilfacade.get_stmtLoc s)
| Function f -> text "Function " ++ text f.svar.vname
- | LongjmpFromFunction f -> text "Longjmp from Function " ++ text f.svar.vname
| FunctionEntry f -> text "FunctionEntry " ++ text f.svar.vname
(** Pretty node for solver variable tracing with short stmt. *)
let pretty_trace () = function
| Statement stmt -> dprintf "node %d \"%a\"" stmt.sid Cilfacade.stmt_pretty_short stmt
- | LongjmpTo stmt -> dprintf "LongjmpTo node %d \"%a\"" stmt.sid Cilfacade.stmt_pretty_short stmt
| Function fd -> dprintf "call of %s (%d)" fd.svar.vname fd.svar.vid
- | LongjmpFromFunction fd -> dprintf "Longjmp from call of %s (%d)" fd.svar.vname fd.svar.vid
| FunctionEntry fd -> dprintf "entry state of %s (%d)" fd.svar.vname fd.svar.vid
(** Output functions for Printable interface *)
@@ -46,27 +40,21 @@ include Printable.SimplePretty (
(** Show node ID for CFG and results output. *)
let show_id = function
| Statement stmt -> string_of_int stmt.sid
- | LongjmpTo stmt -> "longjmpto" ^ string_of_int stmt.sid
| Function fd -> "ret" ^ string_of_int fd.svar.vid
- | LongjmpFromFunction fd -> "longjmpfrom" ^ string_of_int fd.svar.vid
| FunctionEntry fd -> "fun" ^ string_of_int fd.svar.vid
(** Show node label for CFG. *)
let show_cfg = function
| Statement stmt -> string_of_int stmt.sid (* doesn't use this but defaults to no label and uses ID from show_id instead *)
- | LongjmpTo stmt -> "longjmpto" ^ string_of_int stmt.sid
| Function fd -> "return of " ^ fd.svar.vname ^ "()"
- | LongjmpFromFunction fd -> "longjmp from " ^ fd.svar.vname ^ "()"
| FunctionEntry fd -> fd.svar.vname ^ "()"
(** Find [fundec] which the node is in. In an incremental run this might yield old fundecs for pseudo-return nodes from the old file. *)
let find_fundec (node: t) =
match node with
- | Statement stmt
- | LongjmpTo stmt -> Cilfacade.find_stmt_fundec stmt
+ | Statement stmt -> Cilfacade.find_stmt_fundec stmt
| Function fd
- | LongjmpFromFunction fd
| FunctionEntry fd -> fd
(** @raise Not_found *)
@@ -82,4 +70,3 @@ let of_id s =
| "ret" -> Function fundec
| "fun" -> FunctionEntry fundec
| _ -> raise Not_found
-(* TODO: longjmpTo, LongjmpFromFunction? *)
diff --git a/src/framework/node0.ml b/src/framework/node0.ml
index 547e0de9aa..0bcfa13510 100644
--- a/src/framework/node0.ml
+++ b/src/framework/node0.ml
@@ -7,22 +7,16 @@ type t =
| Statement of CilType.Stmt.t
(** The statements as identified by CIL *)
(* The stmt in a Statement node is misleading because nodes are program points between transfer functions (edges), which actually correspond to statement execution. *)
- | LongjmpTo of CilType.Stmt.t
- (** The statement as the target of a longjmp *)
| FunctionEntry of CilType.Fundec.t
(** *)
| Function of CilType.Fundec.t
(** The variable information associated with the function declaration. *)
- | LongjmpFromFunction of CilType.Fundec.t
- (** Handles longjumps out of the concerned function *)
[@@deriving eq, ord, hash, to_yojson]
let location (node: t) =
match node with
| Statement stmt -> Cilfacade0.get_stmtLoc stmt
- | LongjmpTo stmt -> Cilfacade0.get_stmtLoc stmt
| Function fd -> fd.svar.vdecl
- | LongjmpFromFunction fd -> fd.svar.vdecl
| FunctionEntry fd -> fd.svar.vdecl
let current_node: t option ref = ref None
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 5387c11b57..3f0c7dd779 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -18,6 +18,13 @@ let isFloatType t =
| TFloat _ -> true
| _ -> false
+let rec isVLAType t =
+ match Cil.unrollType t with
+ | TArray (et, len, _) ->
+ let variable_len = GobOption.exists (Fun.negate Cil.isConstant) len in
+ variable_len || isVLAType et
+ | _ -> false
+
let init_options () =
Mergecil.merge_inlines := get_bool "cil.merge.inlines";
Cil.cstd := Cil.cstd_of_string (get_string "cil.cstd");
diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml
index af12ddc9c9..04b1af62f6 100644
--- a/src/util/wideningTokens.ml
+++ b/src/util/wideningTokens.ml
@@ -172,7 +172,7 @@ struct
let asm ctx = lift_fun ctx lift' S.asm identity
let skip ctx = lift_fun ctx lift' S.skip identity
let special ctx r f args = lift_fun ctx lift' S.special ((|>) args % (|>) f % (|>) r)
- let combine ctx ?(longjmpthrough = false) r fe f args fc es f_ask = lift_fun ctx lift' S.combine (fun p -> p ~longjmpthrough r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
+ let combine ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *)
let threadenter ctx lval f args = lift_fun ctx (fun l ts -> List.map (Fun.flip lift' ts) l) S.threadenter ((|>) args % (|>) f % (|>) lval)
let threadspawn ctx lval f args fctx = lift_fun ctx lift' S.threadspawn ((|>) (conv fctx) % (|>) args % (|>) f % (|>) lval)
diff --git a/src/witness/argTools.ml b/src/witness/argTools.ml
index 41aae0cb7f..b5d87cde9b 100644
--- a/src/witness/argTools.ml
+++ b/src/witness/argTools.ml
@@ -21,10 +21,8 @@ struct
let dot_node ppf node =
let shape = match Arg.Node.cfgnode node with
| Statement {skind=If (_,_,_,_,_); _} -> "diamond"
- | Statement _
- | LongjmpTo _ -> "oval"
+ | Statement _ -> "oval"
| Function _
- | LongjmpFromFunction _
| FunctionEntry _ -> "box"
in
Format.fprintf ppf "@,%a [shape=%s];" dot_node_name node shape;
@@ -84,9 +82,7 @@ struct
let i_str = string_of_int i in
match n with
| Statement stmt -> Printf.sprintf "s%d(%d)[%s]" stmt.sid c_tag i_str
- | LongjmpTo stmt -> "" (* TODO: Correct? *)
| Function f -> Printf.sprintf "ret%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
- | LongjmpFromFunction f -> "" (* TODO: Correct? *)
| FunctionEntry f -> Printf.sprintf "fun%d%s(%d)[%s]" f.svar.vid f.svar.vname c_tag i_str
(* TODO: less hacky way (without ask_indices) to move node *)
diff --git a/src/witness/observerAnalysis.ml b/src/witness/observerAnalysis.ml
index d073e709db..a5180e3642 100644
--- a/src/witness/observerAnalysis.ml
+++ b/src/witness/observerAnalysis.ml
@@ -65,7 +65,7 @@ struct
(* ctx.local doesn't matter here? *)
[ctx.local, step ctx.local ctx.prev_node (FunctionEntry f)]
- 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 =
step au (Function f) ctx.node
let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml
index 0a8f9506ca..2e2e146659 100644
--- a/src/witness/witnessConstraints.ml
+++ b/src/witness/witnessConstraints.ml
@@ -278,7 +278,7 @@ struct
in
fold' ctx Spec.enter (fun h -> h l f a) g []
- let combine ctx ?(longjmpthrough = false) l fe f a fc d f_ask =
+ let combine ctx l fe f a fc d f_ask =
assert (Dom.cardinal (fst ctx.local) = 1);
let cd = Dom.choose_key (fst ctx.local) in
let k x (y, sync) =
diff --git a/tests/incremental/11-restart/12-mutex-simple-access.c b/tests/incremental/11-restart/12-mutex-simple-access.c
index 37a81c9a61..8a1c25768b 100644
--- a/tests/incremental/11-restart/12-mutex-simple-access.c
+++ b/tests/incremental/11-restart/12-mutex-simple-access.c
@@ -1,4 +1,3 @@
-// SKIP!
// Same as 13-restart-write/01-mutex-simple
#include
#include
diff --git a/tests/incremental/11-restart/17-mutex-simple-fuel.c b/tests/incremental/11-restart/17-mutex-simple-fuel.c
index eedc05d69c..82c1642a93 100644
--- a/tests/incremental/11-restart/17-mutex-simple-fuel.c
+++ b/tests/incremental/11-restart/17-mutex-simple-fuel.c
@@ -1,4 +1,3 @@
-// SKIP!
#include
#include
diff --git a/tests/incremental/13-restart-write/01-mutex-simple.c b/tests/incremental/13-restart-write/01-mutex-simple.c
index eedc05d69c..82c1642a93 100644
--- a/tests/incremental/13-restart-write/01-mutex-simple.c
+++ b/tests/incremental/13-restart-write/01-mutex-simple.c
@@ -1,4 +1,3 @@
-// SKIP!
#include
#include
diff --git a/tests/incremental/13-restart-write/05-race-call-remove.c b/tests/incremental/13-restart-write/05-race-call-remove.c
index f0207d3051..c07962ad78 100644
--- a/tests/incremental/13-restart-write/05-race-call-remove.c
+++ b/tests/incremental/13-restart-write/05-race-call-remove.c
@@ -1,4 +1,3 @@
-// SKIP!
#include
int g;
diff --git a/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c
index eedc05d69c..82c1642a93 100644
--- a/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c
+++ b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c
@@ -1,4 +1,3 @@
-// SKIP!
#include
#include
diff --git a/tests/regression/68-longjmp/21-multifun.c b/tests/regression/68-longjmp/21-multifun.c
index 0115aecf0b..3d593c2a8f 100644
--- a/tests/regression/68-longjmp/21-multifun.c
+++ b/tests/regression/68-longjmp/21-multifun.c
@@ -26,7 +26,7 @@ int main () {
if(0 == setjmp( env_buffer )) {
fun();
} else {
- __goblint_check(global == 42); //TODO
+ __goblint_check(global == 42);
}
return(0);
diff --git a/tests/regression/68-longjmp/31-mixedjmpbufs.c b/tests/regression/68-longjmp/31-mixedjmpbufs.c
index 1ae2ce011c..470526fe19 100644
--- a/tests/regression/68-longjmp/31-mixedjmpbufs.c
+++ b/tests/regression/68-longjmp/31-mixedjmpbufs.c
@@ -9,7 +9,7 @@ jmp_buf error1;
int blorg(int x) {
if(x > 8) {
- longjmp(error1, 1); //NOWARN
+ longjmp(error1, 1); // WARN (modified since setjmp)
}
return x;
@@ -17,7 +17,7 @@ int blorg(int x) {
int blub(int x,int y) {
if(x == 0) {
- longjmp(error0, 1); //NOWARN
+ longjmp(error0, 1); // WARN (modified since setjmp)
}
return blorg(x-27+3);
@@ -40,7 +40,7 @@ int main(void) {
int x, y;
scanf("%d", &x);
scanf("%d", &y);
- int x = blub(x, y);
+ int x = blub(x, y); // NOWARN
printf("%d", x);
return 0;
diff --git a/tests/regression/68-longjmp/50-arguments-non-top.c b/tests/regression/68-longjmp/50-arguments-non-top.c
index ed4ba930e6..fd5f30a166 100644
--- a/tests/regression/68-longjmp/50-arguments-non-top.c
+++ b/tests/regression/68-longjmp/50-arguments-non-top.c
@@ -19,7 +19,7 @@ int main () {
if (val = setjmp( env_buffer )) {
__goblint_check(val == 1); // UNKNOWN!
__goblint_check(val != 1); // UNKNOWN!
- __goblint_check(1 <= val);
+ __goblint_check(1 <= val); // TODO (better interval exclude)
__goblint_check(val <= 10);
return 8;
}
diff --git a/tests/regression/68-longjmp/51-worries.c b/tests/regression/68-longjmp/51-worries.c
new file mode 100644
index 0000000000..d25df25712
--- /dev/null
+++ b/tests/regression/68-longjmp/51-worries.c
@@ -0,0 +1,26 @@
+// PARAM: --enable ana.int.interval
+#include
+#include
+#include
+#include
+
+jmp_buf env_buffer;
+int global = 0;
+
+int bar() {
+ longjmp(env_buffer, 2);
+ return 8;
+}
+
+void foo() {
+ global = bar();
+}
+
+int main() {
+ if(setjmp( env_buffer )) {
+ assert(global == 0);
+ return 0;
+ }
+
+ foo();
+}