diff --git a/.semgrep/cil.yml b/.semgrep/cil.yml index 7cc2e78f40..5c12ae5a71 100644 --- a/.semgrep/cil.yml +++ b/.semgrep/cil.yml @@ -6,6 +6,7 @@ rules: - pattern: Cil.typeOfInit - pattern: Cil.typeOffset - pattern: Cil.get_stmtLoc + - pattern: Cil.get_instrLoc paths: exclude: - cilfacade0.ml diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml index f2e5a66ce2..51c7df6380 100644 --- a/src/transform/evalAssert.ml +++ b/src/transform/evalAssert.ml @@ -106,16 +106,16 @@ module EvalAssert = struct let rec instrument_instructions = function | i1 :: ((i2 :: _) as is) -> (* List contains successor statement, use location of successor for values *) - let loc = get_instrLoc i2 in + let loc = get_instrLoc i2 in (* TODO: why not using Cilfacade.get_instrLoc? *) i1 :: ((instrument i1 loc) @ instrument_instructions is) | [i] when unique_succ -> (* Last statement in list *) (* Successor of it has only one predecessor, we can query for the value there *) - let loc = get_stmtLoc (List.hd s.succs).skind in + let loc = get_stmtLoc (List.hd s.succs).skind in (* TODO: why not using Cilfacade.get_stmtLoc? *) i :: (instrument i loc) | [i] when s.succs <> [] -> (* Successor has multiple predecessors, results may be imprecise but remain correct *) - let loc = get_stmtLoc (List.hd s.succs).skind in + let loc = get_stmtLoc (List.hd s.succs).skind in (* TODO: why not using Cilfacade.get_stmtLoc? *) i :: (instrument i loc) | x -> x in @@ -134,7 +134,7 @@ module EvalAssert = struct match s.preds with | [p1; p2] when not only_at_locks -> (* exactly two predecessors -> join point, assert locals if they changed *) - let join_loc = get_stmtLoc s.skind in + let join_loc = get_stmtLoc s.skind in (* TODO: why not using Cilfacade.get_stmtLoc? *) (* Possible enhancement: It would be nice to only assert locals here that were modified in either branch if trans.assert.full is false *) let asserts = make_assert join_loc None in self#queueInstr asserts; () @@ -153,7 +153,7 @@ module EvalAssert = struct let add_asserts block = if block.bstmts <> [] then let with_asserts = - let b_loc = get_stmtLoc (List.hd block.bstmts).skind in + let b_loc = get_stmtLoc (List.hd block.bstmts).skind in (* TODO: why not using Cilfacade.get_stmtLoc? *) let b_assert_instr = asserts b_loc vars in [cStmt "{ %I:asserts %S:b }" (fun n t -> makeVarinfo true "unknown" (TVoid [])) b_loc [("asserts", FI b_assert_instr); ("b", FS block.bstmts)]] in diff --git a/src/util/cilfacade0.ml b/src/util/cilfacade0.ml index dfe6dd031b..4d3e56f48a 100644 --- a/src/util/cilfacade0.ml +++ b/src/util/cilfacade0.ml @@ -16,12 +16,32 @@ let rec get_labelsLoc = function else loc -let get_stmtkindLoc = Cil.get_stmtLoc (* CIL has a confusing name for this function *) +(** Following functions are similar to [Cil] versions, but return expression location instead of entire statement location, where possible. *) +(* Ideally we would have both copies of the functions available, but UpdateCil would have to be adapted per-stmtkind/instr to store and update either one or two locations. *) -let get_stmtLoc stmt = +(** Get expression location for [Cil.instr]. *) +let get_instrLoc = function + | Set (_, _, _loc, eloc) -> eloc + | Call (_, _, _, _loc, eloc) -> eloc + | Asm (_, _, _, _, _, loc) -> loc + | VarDecl (_, loc) -> loc + +(** Get expression location for [Cil.stmt]. *) +(* confusingly CIL.get_stmtLoc works on stmtkind instead *) +let rec get_stmtLoc stmt = match stmt.skind with - (* Cil.get_stmtLoc returns Cil.locUnknown in these cases, so try labels instead *) + (* no stmtkind/instr location in these cases, so try labels instead *) | Instr [] | Block {bstmts = []; _} -> get_labelsLoc stmt.labels - | _ -> get_stmtkindLoc stmt.skind + + | Instr (hd :: _) -> get_instrLoc hd + | Return (_, loc) -> loc + | Goto (_, loc) -> loc + | ComputedGoto (_, loc) -> loc + | Break loc -> loc + | Continue loc -> loc + | If (_, _, _, _loc, eloc) -> eloc + | Switch (_, _, _, _loc, eloc) -> eloc + | Loop (_, _loc, eloc, _, _) -> eloc + | Block {bstmts = hd :: _; _} -> get_stmtLoc hd diff --git a/tests/regression/04-mutex/81-if-cond-race-loc.c b/tests/regression/04-mutex/81-if-cond-race-loc.c new file mode 100644 index 0000000000..b5228f6e70 --- /dev/null +++ b/tests/regression/04-mutex/81-if-cond-race-loc.c @@ -0,0 +1,26 @@ +#include +#include + +int myglobal; + +void *t_fun(void *arg) { + // awkward formatting to check that warning is just on condition expression, not entire if + if // NORACE + (myglobal > 0) { // RACE! + printf("Stupid!"); + printf("Stupid!"); + printf("Stupid!"); + printf("Stupid!"); + printf("Stupid!"); + printf("Stupid!"); + } + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + myglobal=myglobal+1; // RACE! + pthread_join (id, NULL); + return 0; +}