Merge pull request #211 from goblint/issue-183

Fix location tracking for for loop expressions

Author: sim642

src/frontc/cabs.ml

@@ -221,7 +221,8 @@ and statement =
  | IF of expression * statement * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | WHILE of expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
  | DOWHILE of expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
- | FOR of for_clause * expression * expression * statement * cabsloc * cabsloc (* second cabsloc is just for expression *)
+ | FOR of for_clause * cabsloc * expression * cabsloc * expression * cabsloc * statement * cabsloc * cabsloc
+   (* for_clause, for_clause_loc, condition, condition_loc, increment, increment_loc, body, loop_loc, expr_loc *)
  | BREAK of cabsloc
  | CONTINUE of cabsloc
  | RETURN of expression * cabsloc * cabsloc (* second cabsloc is just for expression *)

src/frontc/cabs2cil.ml

@@ -6853,24 +6853,31 @@ and doStatement (s : A.statement) : chunk =
         exitLoop ();
         loopChunk (s' @@ s'')
 
-    | A.FOR(fc1,e2,e3,s,loc,eloc) -> begin
+    | A.FOR(fc1,fc_loc,e2,e2_loc,e3,e3_loc,s,loc,eloc) -> begin
         let loc' = convLoc loc in
         let eloc' = convLoc eloc in
-        currentLoc := loc'; (* For loop statement location is not synthetic. *)
-        currentExpLoc := SynthetizeLoc.doLoc eloc';
+        let fc_loc' = convLoc fc_loc in
+        let e2_loc' = convLoc e2_loc in
+        let e3_loc' = convLoc e3_loc in
+        currentLoc := loc'; (* For loop statement location is not synthetic (see se1 comment below). *)
+        currentExpLoc := SynthetizeLoc.doLoc fc_loc';
         enterScope (); (* Just in case we have a declaration *)
         let (se1, _, _) =
           match fc1 with
             FC_EXP e1 -> doExp false e1 ADrop
-          | FC_DECL d1 -> (doDecl false false d1, zero, voidType)
+          | FC_DECL d1 -> (doDecl false false d1, zero, voidType) (* doDecl may modify currentLoc and currentExpLoc! *)
         in
         (* First instruction (assignment) in for loop initializer has non-synthetic statement location before for loop.
            Its expression location inside for loop parentheses is synthetic.
            All other instructions are fully synthetic. *)
         let se1 = SynthetizeLoc.eDoChunkHead (SynthetizeLoc.doChunkTail se1) in
-        let (se3, _, _) = doExp false e3 ADrop in
-        let se3 = SynthetizeLoc.doChunkHead se3 in
+        (* Reset both locations due to doDecl (see above). *)
+        currentLoc := loc'; (* TODO: Why is statement location not synthetic here? Not needed? *)
+        currentExpLoc := SynthetizeLoc.doLoc e3_loc';
+        let (se3, _, _) = doExp false e3 ADrop in (* doExp does doChunkTail *)
+        let se3 = SynthetizeLoc.doChunkHead se3 in (* So just doChunkHead is enough *)
         startLoop false;
+        (* TODO: Are these locations ever used in doStatement? Why not synthetic? *)
         currentLoc := loc';
         currentExpLoc := eloc';
         let s' = doStatement s in
@@ -6880,6 +6887,8 @@ and doStatement (s : A.statement) : chunk =
         let break_cond = breakChunk loc' in (* TODO: use eloc'? *)
         exitLoop ();
         let res =
+          currentLoc := SynthetizeLoc.doLoc loc';
+          currentExpLoc := SynthetizeLoc.doLoc e2_loc';
           match e2 with
             A.NOTHING -> (* This means true *)
               se1 @@ loopChunk (consLabLoopCondition s' @@ s'')

src/frontc/cabshelper.ml

@@ -90,7 +90,7 @@ begin
   | IF(_,_,_,loc,_) -> loc
   | WHILE(_,_,loc,_) -> loc
   | DOWHILE(_,_,loc,_) -> loc
-  | FOR(_,_,_,_,loc,_) -> loc
+  | FOR(_,_,_,_,_,_,_,loc,_) -> loc
   | BREAK(loc) -> loc
   | CONTINUE(loc) -> loc
   | RETURN(_,loc,_) -> loc

src/frontc/cabsvisit.ml

@@ -372,7 +372,7 @@ and childrenStatement vis s =
       let e' = ve e in
       let s1' = vs l s1 in
       if e' != e || s1' != s1 then DOWHILE (e', s1', l, el) else s
-  | FOR (fc1, e2, e3, s4, l, el) ->
+  | FOR (fc1, fc_loc, e2, e2_loc, e3, e3_loc, s4, l, el) ->
       let _ = vis#vEnterScope () in
       let fc1' =
         match fc1 with
@@ -392,7 +392,7 @@ and childrenStatement vis s =
       let s4' = vs l s4 in
       let _ = vis#vExitScope () in
       if fc1' != fc1 || e2' != e2 || e3' != e3 || s4' != s4
-      then FOR (fc1', e2', e3', s4', l, el) else s
+      then FOR (fc1', fc_loc, e2', e2_loc, e3', e3_loc, s4', l, el) else s
   | BREAK _ | CONTINUE _ | GOTO _ -> s
   | RETURN (e, l, el) ->
       let e' = ve e in

src/frontc/cparser.mly

@@ -384,6 +384,7 @@ let transformOffsetOf (speclist, dtype) member =
 %type <Cabs.statement list> block_element_list
 %type <string list> local_labels local_label_names
 %type <string list> old_parameter_list_ne
+%type <Cabs.for_clause * cabsloc> for_clause
 
 %type <Cabs.init_name> init_declarator
 %type <Cabs.init_name list> init_declarator_list
@@ -952,9 +953,9 @@ statement_no_null:
 	        	{WHILE (smooth_expression (fst $2), $4, joinLoc $1 $5, joinLoc (snd $2) $3)}
 |   DO statement WHILE paren_comma_expression SEMICOLON
 	        	         {DOWHILE (smooth_expression (fst $4), $2, joinLoc $1 $5, joinLoc (snd $4) $5)}
-|   FOR LPAREN for_clause opt_expression
-	        SEMICOLON opt_expression RPAREN statement location
-	                         {FOR ($3, $4, $6, $8, joinLoc $1 $9, joinLoc $2 $7)}
+|   FOR LPAREN for_clause location opt_expression location
+	        SEMICOLON location opt_expression location RPAREN statement location
+	                         {let (fc, fc_loc) = $3 in FOR (fc, fc_loc, $5, joinLoc $4 $6, $9, joinLoc $8 $10, $12, joinLoc $1 $13, joinLoc $2 $11)}
 |   IDENT COLON attribute_nocv_list location statement_no_null
 		                 {(* The only attribute that should appear here
                                      is "unused". For now, we drop this on the
@@ -989,8 +990,8 @@ statement_no_null:
 
 
 for_clause:
-    opt_expression SEMICOLON     { FC_EXP $1 }
-|   declaration                  { FC_DECL $1 }
+    location opt_expression SEMICOLON     { (FC_EXP $2, joinLoc $1 $3) }
+|   location declaration location         { (FC_DECL $2, joinLoc $1 $3) }
 ;
 
 declaration:                                /* ISO 6.7.*/

src/frontc/cprint.ml

@@ -633,7 +633,7 @@ and print_statement stat =
       print_expression_level 0 exp;
       print ");";
       new_line ();
-  | FOR (fc1, exp2, exp3, stat, loc, eloc) ->
+  | FOR (fc1, _, exp2, _, exp3, _, stat, loc, eloc) ->
       setLoc(loc);
       printl ["for";"("];
       (match fc1 with