Skip to content

Commit 1f7424f

Browse files
committed
Don't use hash for longjmp
1 parent 6d0e55d commit 1f7424f

File tree

5 files changed

+6
-11
lines changed

5 files changed

+6
-11
lines changed

src/analyses/activeSetjmp.ml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,7 @@ struct
3535
let desc = LibraryFunctions.find f in
3636
match desc.special arglist with
3737
| Setjmp _ ->
38-
let controlctx = ControlSpecC.hash (ctx.control_context ()) in
39-
let entry = (ctx.prev_node, IntDomain.Flattened.of_int (Int64.of_int controlctx)) in
38+
let entry = (ctx.prev_node, ctx.control_context ()) in
4039
D.add (Target entry) ctx.local
4140
| Longjmp {env; value; sigrestore} -> ctx.local
4241
| _ -> ctx.local

src/analyses/base.ml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2239,8 +2239,7 @@ struct
22392239
| Setjmp { env; savesigs}, _ ->
22402240
(let st' = (match (eval_rv (Analyses.ask_of_ctx ctx) gs st env) with
22412241
| `Address jmp_buf ->
2242-
let controlctx = ControlSpecC.hash (ctx.control_context ()) in
2243-
let value = `JmpBuf ((ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, IntDomain.Flattened.of_int (Int64.of_int controlctx)))),false) in
2242+
let value = `JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())),false) in
22442243
let r = set ~ctx (Analyses.ask_of_ctx ctx) gs st jmp_buf (Cilfacade.typeOf env) value in
22452244
M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
22462245
r

src/analyses/modifiedSinceLongjmp.ml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,7 @@ struct
5555
let desc = LibraryFunctions.find f in
5656
match desc.special arglist with
5757
| Setjmp _ ->
58-
let controlctx = ControlSpecC.hash (ctx.control_context ()) in
59-
let entry = (ctx.prev_node, IntDomain.Flattened.of_int (Int64.of_int controlctx)) in
58+
let entry = (ctx.prev_node, ctx.control_context ()) in
6059
let v = D.find entry ctx.local in (* Will make bot binding explicit here *)
6160
(* LHS of setjmp not marked as tainted on purpose *)
6261
D.add entry v ctx.local

src/cdomains/jmpBufDomain.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
module BufferEntry = Printable.ProdSimple(Node)(IntDomain.Flattened)
1+
module BufferEntry = Printable.ProdSimple(Node)(ControlSpecC)
22

33
module BufferEntryOrTop = struct
44
include Printable.Std

src/framework/constraints.ml

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -684,8 +684,7 @@ struct
684684
| Target (targetnode, targetcontext) ->
685685
let target_in_caller () = CilType.Fundec.equal (Node.find_fundec targetnode) current_fundec in
686686
let targetcontext_matches () =
687-
let controlctx = ControlSpecC.hash (ctx.control_context ()) in
688-
targetcontext = IntDomain.Flattened.of_int (Int64.of_int controlctx)
687+
ControlSpecC.equal targetcontext (ctx.control_context ())
689688
in
690689
(* Check if corresponding setjmp call was in current function & in current context *)
691690
if targetcontext_matches () && target_in_caller () then
@@ -799,8 +798,7 @@ struct
799798
if not (JmpBufDomain.JmpBufSet.mem (Target (node,c)) validBuffers) then
800799
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
801800
else
802-
(let controlctx = ControlSpecC.hash (ctx.control_context ()) in
803-
if c = IntDomain.Flattened.of_int (Int64.of_int controlctx) && (Node.find_fundec node).svar.vname = current_fundec.svar.vname then
801+
(if ControlSpecC.equal c (ctx.control_context ()) && (Node.find_fundec node).svar.vname = current_fundec.svar.vname then
804802
(if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %s\n" (Node.show node);
805803
match node with
806804
| Statement { skind = Instr [Call (lval, exp, args,_, _)] ;_ } ->

0 commit comments

Comments
 (0)