Merge pull request #167 from goblint/fix-locations

Location fixes for Goblint YAML witness generation/validation

Author: sim642

src/check.ml

@@ -760,8 +760,9 @@ and checkStmt (s: stmt) =
           currentLoc := l;
           let te = checkExp false e in
           typeMatch te voidPtrType
-      | Return (re,l) -> begin
+      | Return (re, l, el) -> begin
           currentLoc := l;
+          currentExpLoc := el;
           match re, !currentReturnType with
             None, TVoid _  -> ()
           | _, TVoid _ -> ignore (warn "Invalid return value")

src/cil.ml

@@ -767,8 +767,9 @@ and stmtkind =
   | Instr  of instr list               (** A group of instructions that do not
                                            contain control flow. Control
                                            implicitly falls through. *)
-  | Return of exp option * location     (** The return statement. This is a
-                                            leaf in the CFG. *)
+  | Return of exp option * location * location (** The return statement. This is a
+                                                   leaf in the CFG.
+                                                   Second location is just for expression. *)
 
   | Goto of stmt ref * location         (** A goto statement. Appears from
                                             actual goto's in the code. *)
@@ -1145,7 +1146,7 @@ let rec get_stmtLoc (statement : stmtkind) =
   match statement with
       Instr([]) -> lu
     | Instr(hd::tl) -> get_instrLoc(hd)
-    | Return(_, loc) -> loc
+    | Return(_, loc, _) -> loc
     | Goto(_, loc) -> loc
     | ComputedGoto(_, loc) -> loc
     | Break(loc) -> loc
@@ -3861,11 +3862,11 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           ++ self#pBlock () thenBlock)
 
   method private pStmtKind (next: stmt) () = function
-      Return(None, l) ->
+      Return(None, l, el) ->
         self#pLineDirective l
           ++ text "return;"
 
-    | Return(Some e, l) ->
+    | Return(Some e, l, el) ->
         self#pLineDirective l
           ++ text "return ("
           ++ self#pExp () e
@@ -5363,13 +5364,13 @@ and childrenStmt (toPrepend: instr list ref) : cilVisitor -> stmt -> stmt =
   (* Just change the statement kind *)
   let skind' =
     match s.skind with
-      Break _ | Continue _ | Goto _ | Return (None, _) -> s.skind
+      Break _ | Continue _ | Goto _ | Return (None, _, _) -> s.skind
     | ComputedGoto (e, l) ->
          let e' = fExp e in
          if e' != e then ComputedGoto (e', l) else s.skind
-    | Return (Some e, l) ->
+    | Return (Some e, l, el) ->
         let e' = fExp e in
-        if e' != e then Return (Some e', l) else s.skind
+        if e' != e then Return (Some e', l, el) else s.skind
     | Loop (b, l, el, s1, s2) ->
         let b' = fBlock b in
         if b' != b then Loop (b', l, el, s1, s2) else s.skind

src/cil.mli

@@ -964,8 +964,9 @@ and stmtkind =
   (** A group of instructions that do not contain control flow. Control
      implicitly falls through. *)
 
-  | Return of exp option * location
-   (** The return statement. This is a leaf in the CFG. *)
+  | Return of exp option * location * location
+   (** The return statement. This is a leaf in the CFG.
+       Second location is just for expression. *)
 
   | Goto of stmt ref * location
    (** A goto statement. Appears from actual goto's in the code or from

src/ext/dataslicing/dataslicing.ml

@@ -336,16 +336,16 @@ let sliceInstr (inst : instr) : instr list =
       instrs @ (Call (ret', sliceExp 1 fn, args', l, el) :: set)
   | _ -> E.s (unimp "inst %a" d_instr inst)
 
-let sliceReturnExp (eo : exp option) (l : location) : stmtkind =
+let sliceReturnExp (eo : exp option) (l : location) (el : location) : stmtkind =
   match eo with
   | Some e ->
       begin
       match sliceExpAll e l with
-      | [], e' -> Return (Some e', l)
+      | [], e' -> Return (Some e', l, el)
       | instrs, e' -> Block (mkBlock [mkStmt (Instr instrs);
-                                      mkStmt (Return (Some e', l))])
+                                      mkStmt (Return (Some e', l, el))])
       end
-  | None -> Return (None, l)
+  | None -> Return (None, l, el)
 
 let rec sliceStmtKind (sk : stmtkind) : stmtkind =
   match sk with
@@ -354,7 +354,7 @@ let rec sliceStmtKind (sk : stmtkind) : stmtkind =
   | If (e, b1, b2, l, el) -> If (sliceExp 1 e, sliceBlock b1, sliceBlock b2, l, el)
   | Break l -> Break l
   | Continue l -> Continue l
-  | Return (eo, l) -> sliceReturnExp eo l
+  | Return (eo, l, el) -> sliceReturnExp eo l el
   | Switch (e, b, sl, l, el) -> Switch (sliceExp 1 e, sliceBlock b,
                                     Util.list_map sliceStmt sl, l, el)
   | Loop (b, l, el, so1, so2) -> Loop (sliceBlock b, l, el,

src/ext/liveness/usedef.ml

@@ -190,8 +190,8 @@ let computeUseDefStmtKind ?(acc_used=VS.empty)
   let ve e = ignore (visitCilExpr useDefVisitor e) in
   let _ =
     match sk with
-      Return (None, _) -> ()
-    | Return (Some e, _) -> ve e
+      Return (None, _, _) -> ()
+    | Return (Some e, _, _) -> ve e
     | If (e, _, _, _, _) -> ve e
     | Break _ | Goto _ | Continue _ -> ()
     | ComputedGoto (e, _) -> ve e
@@ -218,8 +218,8 @@ let rec computeDeepUseDefStmtKind ?(acc_used=VS.empty)
   varDefs := acc_defs;
   let ve e = ignore (visitCilExpr useDefVisitor e) in
   match sk with
-    Return (None, _) -> !varUsed, !varDefs
-  | Return (Some e, _) ->
+    Return (None, _, _) -> !varUsed, !varDefs
+  | Return (Some e, _, _) ->
       let _ = ve e in
       !varUsed, !varDefs
   | If (e, tb, fb, _, _) ->

src/ext/pta/ptranal.ml

@@ -304,7 +304,7 @@ let analyze_instr (i : instr ) : unit =
 let rec analyze_stmt (s : stmt ) : unit =
   match s.skind with
       Instr il -> List.iter analyze_instr il
-    | Return (eo, l) ->
+    | Return (eo, l, el) ->
         begin
           match eo with
               Some e ->

src/ext/syntacticsearch/funcFunction.ml

@@ -32,7 +32,7 @@ class fun_find_returns funname funid result : nopCilVisitor =
 
     method! vstmt stmt =
       match stmt.skind with
-      | Return (Some exp, loc) ->
+      | Return (Some exp, loc, eloc) ->
           result :=
             !result
             @ [
@@ -42,7 +42,7 @@ class fun_find_returns funname funid result : nopCilVisitor =
                   -1 );
               ];
           DoChildren
-      | Return (None, loc) ->
+      | Return (None, loc, eloc) ->
           result := !result @ [ ("", loc, "void", -1) ];
           DoChildren
       | _ -> DoChildren
@@ -72,7 +72,7 @@ class fun_find_sig funname funid result : nopCilVisitor =
 
     method! vstmt stmt =
       match stmt.skind with
-      | Return (Some exp, loc) ->
+      | Return (Some exp, loc, eloc) ->
           result :=
             !result
             @ [
@@ -82,7 +82,7 @@ class fun_find_sig funname funid result : nopCilVisitor =
                   -1 );
               ];
           SkipChildren
-      | Return (None, loc) ->
+      | Return (None, loc, eloc) ->
           result := !result @ [ ("", loc, "void", -1) ];
           SkipChildren
       | _ -> DoChildren

src/ext/syntacticsearch/funcVar.ml

@@ -170,7 +170,7 @@ let rec search_stmt_list_for_var list name varid includeCallTmp =
       ( match x.skind with
       | Instr ins_list ->
           search_instr_list_for_var ins_list name varid includeCallTmp
-      | Return (Some exp, loc) ->
+      | Return (Some exp, loc, eloc) ->
           search_expression exp name loc varid includeCallTmp
       | ComputedGoto (exp, loc) ->
           search_expression exp name loc varid includeCallTmp

src/formatparse.mly

@@ -1334,7 +1334,7 @@ stmt:
                   }
 |   RETURN exp_opt SEMICOLON
                   { (fun mkTemp loc args ->
-                         mkStmt (Return((fst $2) args, loc)))
+                         mkStmt (Return((fst $2) args, loc, locUnknown))) (* TODO: better eloc *)
                   }
 |   BREAK SEMICOLON
                   { (fun mkTemp loc args ->

src/frontc/cabs.ml

@@ -223,7 +223,7 @@ and statement =
  | FOR of for_clause * expression * expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | BREAK of cabsloc
  | CONTINUE of cabsloc
- | RETURN of expression * cabsloc
+ | RETURN of expression * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | SWITCH of expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | CASE of expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | CASERANGE of expression * expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)