Merge pull request #717 from goblint/issue-689

Interactive: fix expression locations

Author: sim642

.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

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

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

tests/regression/04-mutex/81-if-cond-race-loc.c

@@ -0,0 +1,26 @@
+#include <pthread.h>
+#include <stdio.h>
+
+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;
+}