From da9e00f53bd306ef2546836ccf2dc91bc72fa318 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 14 Feb 2024 17:18:30 +0200 Subject: [PATCH 1/7] Add expression location to return --- src/check.ml | 3 ++- src/cil.ml | 17 ++++++++-------- src/cil.mli | 5 +++-- src/ext/dataslicing/dataslicing.ml | 10 ++++----- src/ext/liveness/usedef.ml | 8 ++++---- src/ext/pta/ptranal.ml | 2 +- src/ext/syntacticsearch/funcFunction.ml | 8 ++++---- src/ext/syntacticsearch/funcVar.ml | 2 +- src/formatparse.mly | 2 +- src/frontc/cabs.ml | 2 +- src/frontc/cabs2cil.ml | 27 ++++++++++++++----------- src/frontc/cabshelper.ml | 2 +- src/frontc/cabsvisit.ml | 4 ++-- src/frontc/cparser.mly | 4 ++-- src/frontc/cprint.ml | 2 +- 15 files changed, 52 insertions(+), 46 deletions(-) diff --git a/src/check.ml b/src/check.ml index 2924fbe48..06a030223 100644 --- a/src/check.ml +++ b/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") diff --git a/src/cil.ml b/src/cil.ml index 8a28dc19e..4bec87a9c 100755 --- a/src/cil.ml +++ b/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 diff --git a/src/cil.mli b/src/cil.mli index a2ee2d506..099b6e8ea 100644 --- a/src/cil.mli +++ b/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 diff --git a/src/ext/dataslicing/dataslicing.ml b/src/ext/dataslicing/dataslicing.ml index dbd3276a3..3d9da12fd 100644 --- a/src/ext/dataslicing/dataslicing.ml +++ b/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, diff --git a/src/ext/liveness/usedef.ml b/src/ext/liveness/usedef.ml index 76afb839b..f002fb19d 100644 --- a/src/ext/liveness/usedef.ml +++ b/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, _, _) -> diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index 2e8dffd6e..cb9df89d3 100644 --- a/src/ext/pta/ptranal.ml +++ b/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 -> diff --git a/src/ext/syntacticsearch/funcFunction.ml b/src/ext/syntacticsearch/funcFunction.ml index fd66acd8b..10e1e6a1a 100644 --- a/src/ext/syntacticsearch/funcFunction.ml +++ b/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 diff --git a/src/ext/syntacticsearch/funcVar.ml b/src/ext/syntacticsearch/funcVar.ml index 857d0b042..cdee5d74b 100644 --- a/src/ext/syntacticsearch/funcVar.ml +++ b/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 diff --git a/src/formatparse.mly b/src/formatparse.mly index f119fc2cc..494c7f4e9 100644 --- a/src/formatparse.mly +++ b/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 -> diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml index d13025b53..7a9db7b14 100644 --- a/src/frontc/cabs.ml +++ b/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 *) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index cb9e3685e..a91265f47 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -859,7 +859,7 @@ module BlockChunk = let doLoc = if first then fun x -> x else doLoc in s.skind <- match s.skind with | Instr xs -> Instr (doInstrs ~first xs) - | Return (e, loc) -> Return (e, doLoc loc) + | Return (e, loc, eloc) -> Return (e, doLoc loc, doLoc eloc) | Goto (s, loc) -> Goto (s, doLoc loc) | ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc) | Break loc -> Break (doLoc loc) @@ -907,7 +907,7 @@ module BlockChunk = let rec doStmt s: unit = s.skind <- match s.skind with | Instr xs -> Instr (doInstrs xs) - | Return (e, loc) -> Return (e, doLoc loc) + | Return (e, loc, eloc) -> Return (e, doLoc loc, doLoc eloc) | Goto (s, loc) -> Goto (s, doLoc loc) | ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc) | Break loc -> Break (doLoc loc) @@ -973,8 +973,8 @@ module BlockChunk = let skipChunk = empty - let returnChunk (e: exp option) (l: location) : chunk = - { stmts = [ mkStmt (Return(e, l)) ]; + let returnChunk (e: exp option) (l: location) (el: location) : chunk = + { stmts = [ mkStmt (Return(e, l, el)) ]; postins = []; cases = [] } @@ -5919,7 +5919,7 @@ and doAliasFun vtype (thisname:string) (othername:string) (argsToList formals) in let call = A.CALL (A.VARIABLE othername, args) in let stmt = if isVoidType rt then A.COMPUTATION(call, loc) - else A.RETURN(call, loc) + else A.RETURN(call, loc, loc) in let body = { A.blabels = []; A.battrs = []; A.bstmts = [stmt] } in let fdef = A.FUNDEF (sname, body, loc, loc) in @@ -6471,7 +6471,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function then !currentFunctionFDEC.sbody.bstmts <- !currentFunctionFDEC.sbody.bstmts - @ [mkStmt (Return(retval, endloc))] + @ [mkStmt (Return(retval, endloc, locUnknown))] end; (* ignore (E.log "The env after finishing the body of %s:\n%t\n" @@ -6769,29 +6769,32 @@ and doStatement (s : A.statement) : chunk = currentLoc := loc'; continueOrLabelChunk loc' - | A.RETURN (A.NOTHING, loc) -> + | A.RETURN (A.NOTHING, loc, eloc) -> let loc' = convLoc loc in + let eloc' = convLoc eloc in currentLoc := loc'; + currentExpLoc := eloc'; if not (isVoidType !currentReturnType) then ignore (warn "Return statement without a value in function returning %a" d_type !currentReturnType); - returnChunk None loc' + returnChunk None loc' eloc' - | A.RETURN (e, loc) -> + | A.RETURN (e, loc, eloc) -> let loc' = convLoc loc in + let eloc' = convLoc eloc in currentLoc := loc'; - currentExpLoc := loc'; (* TODO: separate expression loc *) + currentExpLoc := eloc'; (* Sometimes we return the result of a void function call *) if isVoidType !currentReturnType then begin ignore (warnOpt "Return statement with a value in function returning void"); let (se, _, _) = doExp false e ADrop in - se @@ returnChunk None loc' + se @@ returnChunk None loc' eloc' end else begin let rt = typeRemoveAttributes ["warn_unused_result"] !currentReturnType in let (se, e', et) = doExp false e (AExp (Some rt)) in let (et'', e'') = castTo et rt e' in - se @@ (returnChunk (Some e'') loc') + se @@ (returnChunk (Some e'') loc' eloc') end | A.SWITCH (e, s, loc, eloc) -> diff --git a/src/frontc/cabshelper.ml b/src/frontc/cabshelper.ml index f222176d3..b0165117d 100644 --- a/src/frontc/cabshelper.ml +++ b/src/frontc/cabshelper.ml @@ -93,7 +93,7 @@ begin | FOR(_,_,_,_,loc,_) -> loc | BREAK(loc) -> loc | CONTINUE(loc) -> loc - | RETURN(_,loc) -> loc + | RETURN(_,loc,_) -> loc | SWITCH(_,_,loc,_) -> loc | CASE(_,_,loc,_) -> loc | CASERANGE(_,_,_,loc,_) -> loc diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml index f6344874c..85d44f933 100644 --- a/src/frontc/cabsvisit.ml +++ b/src/frontc/cabsvisit.ml @@ -393,9 +393,9 @@ and childrenStatement vis s = if fc1' != fc1 || e2' != e2 || e3' != e3 || s4' != s4 then FOR (fc1', e2', e3', s4', l, el) else s | BREAK _ | CONTINUE _ | GOTO _ -> s - | RETURN (e, l) -> + | RETURN (e, l, el) -> let e' = ve e in - if e' != e then RETURN (e', l) else s + if e' != e then RETURN (e', l, el) else s | SWITCH (e, s1, l, el) -> let e' = ve e in let s1' = vs l s1 in diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 17fa5a34d..db8431cdc 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -972,9 +972,9 @@ statement_no_null: {CASERANGE (fst $2, fst $4, $6, joinLoc $1 $7, joinLoc $1 $5)} | DEFAULT COLON statement location {DEFAULT ($3, joinLoc $1 $4, joinLoc $1 $2)} -| RETURN SEMICOLON {RETURN (NOTHING, joinLoc $1 $2)} +| RETURN SEMICOLON {RETURN (NOTHING, joinLoc $1 $2, cabslu)} | RETURN comma_expression SEMICOLON - {RETURN (smooth_expression (fst $2), joinLoc $1 $3)} + {RETURN (smooth_expression (fst $2), joinLoc $1 $3, joinLoc (snd $2) $3)} | BREAK SEMICOLON {BREAK (joinLoc $1 $2)} | CONTINUE SEMICOLON {CONTINUE (joinLoc $1 $2)} | GOTO IDENT SEMICOLON diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml index 07a75ada5..2ea32fce6 100644 --- a/src/frontc/cprint.ml +++ b/src/frontc/cprint.ml @@ -650,7 +650,7 @@ and print_statement stat = | CONTINUE (loc) -> setLoc(loc); print "continue;"; new_line () - | RETURN (exp, loc) -> + | RETURN (exp, loc, eloc) -> setLoc(loc); print "return"; if exp = NOTHING From 8a6d35976a77f3459d55d5808ea4937557aa0b99 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Feb 2024 10:32:00 +0200 Subject: [PATCH 2/7] Use same statement location for all initializer statements --- src/frontc/cabs2cil.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index a91265f47..dc0694b25 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -5953,9 +5953,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function (* Do all the variables and concatenate the resulting statements *) let doOneDeclarator (acc: chunk) (name: init_name) = let (n,ndt,a,l),_ = name in - currentLoc := convLoc l; currentExpLoc := convLoc l; (* eloc for local initializer assignment instruction *) - (* Do the specifiers exactly once *) if isglobal then begin let spec_res = match spec_res with Some s -> s | _ -> failwith "Option.get" in let bt,_,_,attrs = spec_res in From 5eda9045937e202caa92e37e9c8c77d2a527cfd5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Feb 2024 10:32:41 +0200 Subject: [PATCH 3/7] Fix non-first initializer having non-synthetic location --- src/frontc/cabs2cil.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index dc0694b25..34868656e 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -5975,15 +5975,15 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function acc end else match spec_res with - | Some spec_res -> acc @@ SynthetizeLoc.doChunkTail (createLocal spec_res name) - | None -> acc @@ SynthetizeLoc.doChunkTail (createAutoLocal name) + | Some spec_res -> acc @@ createLocal spec_res name + | None -> acc @@ createAutoLocal name in let res = List.fold_left doOneDeclarator empty nl in (* ignore (E.log "after doDecl %a: res=%a\n" d_loc !currentLoc d_chunk res); *) - res + SynthetizeLoc.doChunkTail res From ee64e4a30eef8b69483a88111ad91aec90eed2ac Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Feb 2024 10:39:56 +0200 Subject: [PATCH 4/7] Make first initializer eloc synthetic --- src/frontc/cabs2cil.ml | 45 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 44 insertions(+), 1 deletion(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 34868656e..76d99f1af 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -932,6 +932,49 @@ module BlockChunk = | stmts, postins -> doStmts stmts; c + + let eDoInstr: instr -> instr = function + | Set (l, e, loc, eloc) -> Set (l, e, loc, doLoc eloc) + | VarDecl (v, loc) -> VarDecl (v, loc) + | Call (l, f, a, loc, eloc) -> Call (l, f, a, loc, doLoc eloc) + | Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, loc) + + (** Change first stmt or instr eloc to synthetic. *) + let eDoChunkHead (c: chunk): chunk = + (* ignore (Pretty.eprintf "synthesizeFirstLoc %a\n" d_chunk c); *) + let doInstrs = function + | [] -> [] + | x :: xs -> eDoInstr x :: xs + in + (* must mutate stmts in order to not break refs (for gotos) *) + let rec doStmt s: unit = + s.skind <- match s.skind with + | Instr xs -> Instr (doInstrs xs) + | Return (e, loc, eloc) -> Return (e, loc, doLoc eloc) + | Goto (s, loc) -> Goto (s, doLoc loc) + | ComputedGoto (e, loc) -> ComputedGoto (e, doLoc loc) + | Break loc -> Break (doLoc loc) + | Continue loc -> Continue (doLoc loc) + | If _ + | Switch _ + | Loop _ -> + s.skind + | Block b -> + doBlock b; + s.skind + and doBlock b = + doStmts b.bstmts + and doStmts = function + | [] -> () + | x :: xs -> + doStmt x + in + match c.stmts, c.postins with + | [], [] -> c + | [], postins -> {c with postins = List.rev (doInstrs (List.rev postins))} + | stmts, postins -> + doStmts stmts; + c end let i2c (i: instr) = @@ -5983,7 +6026,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function ignore (E.log "after doDecl %a: res=%a\n" d_loc !currentLoc d_chunk res); *) - SynthetizeLoc.doChunkTail res + SynthetizeLoc.eDoChunkHead (SynthetizeLoc.doChunkTail res) From fb471582d7e9685ab705ba57f7a6675b97ca8f64 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 20 Feb 2024 13:07:42 +0200 Subject: [PATCH 5/7] Make first for initializer loc non-synthetic --- src/frontc/cabs2cil.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 76d99f1af..c23fca745 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6769,7 +6769,7 @@ and doStatement (s : A.statement) : chunk = | A.FOR(fc1,e2,e3,s,loc,eloc) -> begin let loc' = convLoc loc in let eloc' = convLoc eloc in - currentLoc := SynthetizeLoc.doLoc loc'; + currentLoc := loc'; currentExpLoc := SynthetizeLoc.doLoc eloc'; enterScope (); (* Just in case we have a declaration *) let (se1, _, _) = @@ -6777,7 +6777,7 @@ and doStatement (s : A.statement) : chunk = FC_EXP e1 -> doExp false e1 ADrop | FC_DECL d1 -> (doDecl false d1, zero, voidType) in - let se1 = SynthetizeLoc.doChunkHead se1 in + let se1 = SynthetizeLoc.eDoChunkHead (SynthetizeLoc.doChunkTail se1) in let (se3, _, _) = doExp false e3 ADrop in let se3 = SynthetizeLoc.doChunkHead se3 in startLoop false; From f87d5c8aa0fffde0fe1c7076af5df360a40abb54 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 28 Feb 2024 15:13:18 +0200 Subject: [PATCH 6/7] Add comments about synthetic location changes --- src/frontc/cabs2cil.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index c23fca745..314f7a27d 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6026,6 +6026,8 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function ignore (E.log "after doDecl %a: res=%a\n" d_loc !currentLoc d_chunk res); *) + (* First transformed assign instruction from declaration initializer has non-synthetic statement location. + All following locations are synthetic. *) SynthetizeLoc.eDoChunkHead (SynthetizeLoc.doChunkTail res) @@ -6769,7 +6771,7 @@ and doStatement (s : A.statement) : chunk = | A.FOR(fc1,e2,e3,s,loc,eloc) -> begin let loc' = convLoc loc in let eloc' = convLoc eloc in - currentLoc := loc'; + currentLoc := loc'; (* For loop statement location is not synthetic. *) currentExpLoc := SynthetizeLoc.doLoc eloc'; enterScope (); (* Just in case we have a declaration *) let (se1, _, _) = @@ -6777,6 +6779,9 @@ and doStatement (s : A.statement) : chunk = FC_EXP e1 -> doExp false e1 ADrop | FC_DECL d1 -> (doDecl false d1, zero, voidType) 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 From ae3a4949d478fad77e004c6fe15a7c83427df59f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 1 Mar 2024 13:24:00 +0200 Subject: [PATCH 7/7] Don't override statement location for for initializer --- src/frontc/cabs2cil.ml | 36 ++++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 16 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 314f7a27d..83d135ac8 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -5966,7 +5966,7 @@ and doAliasFun vtype (thisname:string) (othername:string) in let body = { A.blabels = []; A.battrs = []; A.bstmts = [stmt] } in let fdef = A.FUNDEF (sname, body, loc, loc) in - ignore (doDecl true fdef); + ignore (doDecl true false fdef); (* doAliasFun only called for isglobal by guard *) (* get the new function *) let v,_ = try lookupGlobalVar thisname with Not_found -> E.s (bug "error in doDecl") in @@ -5974,9 +5974,10 @@ and doAliasFun vtype (thisname:string) (othername:string) (* Do one declaration *) -and doDecl (isglobal: bool) : A.definition -> chunk = function +and doDecl (isglobal: bool) (isstmt: bool) : A.definition -> chunk = function | A.DECDEF ((s, nl), loc) -> - currentLoc := convLoc loc; + if isglobal || isstmt then + currentLoc := convLoc loc; currentExpLoc := convLoc loc; (* eloc for local initializer assignment instruction *) (* Do the specifiers exactly once *) let sugg = @@ -6033,20 +6034,22 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function | A.TYPEDEF (ng, loc) -> - currentLoc := convLoc(loc); - doTypedef ng; empty + if isglobal || isstmt then + currentLoc := convLoc(loc); + doTypedef ng; empty | A.ONLYTYPEDEF (s, loc) -> - currentLoc := convLoc(loc); + if isglobal || isstmt then + currentLoc := convLoc(loc); doOnlyTypedef s; empty | A.GLOBASM (s,loc) when isglobal -> - currentLoc := convLoc(loc); + currentLoc := convLoc(loc); (* isglobal by guard *) cabsPushGlobal (GAsm (s, !currentLoc)); empty | A.PRAGMA (a, loc) when isglobal -> begin - currentLoc := convLoc(loc); + currentLoc := convLoc(loc); (* isglobal by guard *) match doAttr ("dummy", [a]) with [Attr("dummy", [a'])] -> let a'' = @@ -6069,7 +6072,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function (body : A.block), loc, _) when isglobal && isExtern specs && isInline specs && (H.mem genv (n ^ "__extinline")) -> - currentLoc := convLoc(loc); + currentLoc := convLoc(loc); (* isglobal by guard *) let othervi, _ = lookupVar (n ^ "__extinline") in if othervi.vname = n then (* The previous entry in the env is also an extern inline version @@ -6084,7 +6087,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function ^^ " reserved for CIL.\n") n n n) end; (* Treat it as a prototype *) - doDecl isglobal (A.DECDEF ((specs, [((n,dt,a,loc'), A.NO_INIT)]), loc)) + doDecl isglobal isstmt (A.DECDEF ((specs, [((n,dt,a,loc'), A.NO_INIT)]), loc)) | A.FUNDEF (((specs,(n,dt,a, _)) : A.single_name), (body : A.block), loc1, loc2) when isglobal -> @@ -6092,7 +6095,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function let funloc = convLoc (joinLoc loc1 loc2) in (* TODO: do in parser and include RBRACE end *) let endloc = convLoc (joinLoc loc2 loc2) in (* TODO: what to do about range of inserted Return? *) (* ignore (E.log "Definition of %s at %a\n" n d_loc funloc); *) - currentLoc := funloc; + currentLoc := funloc; (* isglobal by guard *) currentExpLoc := funloc; (* TODO: location just for declaration *) E.withContext (fun _ -> dprintf "2cil: %s" n) @@ -6531,7 +6534,8 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function end (* FUNDEF *) | LINKAGE (n, loc, dl) -> - currentLoc := convLoc loc; + if isglobal || isstmt then + currentLoc := convLoc loc; if n <> "C" then ignore (warn "Encountered linkage specification \"%s\"" n); if not isglobal then @@ -6539,7 +6543,7 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function (* For now drop the linkage on the floor !!! *) List.iter (fun d -> - let s = doDecl isglobal d in + let s = doDecl isglobal isstmt d in if isNotEmpty s then E.s (bug "doDecl returns non-empty statement for global")) dl; @@ -6777,7 +6781,7 @@ and doStatement (s : A.statement) : chunk = let (se1, _, _) = match fc1 with FC_EXP e1 -> doExp false e1 ADrop - | FC_DECL d1 -> (doDecl false d1, zero, voidType) + | FC_DECL d1 -> (doDecl false false d1, zero, voidType) 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. @@ -6949,7 +6953,7 @@ and doStatement (s : A.statement) : chunk = end | A.DEFINITION d -> - let s = doDecl false d in + let s = doDecl false true d in (* ignore (E.log "Def at %a: %a\n" d_loc !currentLoc d_chunk s); *) @@ -7060,7 +7064,7 @@ let convFile (f : A.file) : Cil.file = let globalidx = ref 0 in let doOneGlobal (d: A.definition) = - let s = doDecl true d in + let s = doDecl true false d in if isNotEmpty s then E.s (bug "doDecl returns non-empty statement for global"); (* See if this is one of the globals which we can leave alone. Increment