From e070513172411493bd5db89a70748b6ea72de981 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 12:14:08 +0300 Subject: [PATCH 1/8] Add synthetic field to Cil.location --- src/cil.ml | 7 +++++-- src/cil.mli | 1 + src/frontc/cabs2cil.ml | 2 +- 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 288c49ce4..8ba7918d4 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -868,6 +868,7 @@ and location = { endLine: int; (** End line number. Negative means unknown. *) endByte: int; (** End byte position. Negative means unknown. *) endColumn: int; (** End column number. Negative means unknown. *) + synthetic: bool; (** Synthetic location, doesn't precisely match source. *) } (* Type signatures. Two types are identical iff they have identical @@ -886,7 +887,8 @@ let locUnknown = { line = -1; column = -1; endLine = -1; endByte = -1; - endColumn = -1;} + endColumn = -1; + synthetic = true;} (* A reference to the current location *) let currentLoc : location ref = ref locUnknown @@ -3167,7 +3169,8 @@ let builtinLoc: location = { line = 1; column = 0; endLine = -1; endByte = -1; - endColumn = -1;} + endColumn = -1; + synthetic = true;} diff --git a/src/cil.mli b/src/cil.mli index 57d0be532..cded7760c 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1103,6 +1103,7 @@ and location = { endLine: int; (** End line number. Negative means unknown. *) endByte: int; (** End byte position. Negative means unknown. *) endColumn: int; (** End column number. Negative means unknown. *) + synthetic: bool; (** Synthetic location, doesn't precisely match source. *) } diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 901d02e6b..44e88ce03 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -190,7 +190,7 @@ let debugLoc = false let convLoc (l : cabsloc) = if debugLoc then ignore (E.log "convLoc at %s: line %d, byte %d, column %d\n" l.filename l.lineno l.byteno l.columnno); - {line = l.lineno; file = l.filename; byte = l.byteno; column = l.columnno; endLine = l.endLineno; endByte = l.endByteno; endColumn = l.endColumnno;} + {line = l.lineno; file = l.filename; byte = l.byteno; column = l.columnno; endLine = l.endLineno; endByte = l.endByteno; endColumn = l.endColumnno; synthetic = false;} let isOldStyleVarArgName n = n = "__builtin_va_alist" From 935e929d04a4c26c3b4fcd278f9d79cc0a030345 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 12:58:15 +0300 Subject: [PATCH 2/8] Make for loop init and increment locations synthetic --- src/frontc/cabs2cil.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 44e88ce03..76d0e06f4 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -6652,8 +6652,8 @@ 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'; - currentExpLoc := eloc'; + currentLoc := {loc' with synthetic = true}; + currentExpLoc := {eloc' with synthetic = true}; enterScope (); (* Just in case we have a declaration *) let (se1, _, _) = match fc1 with @@ -6662,9 +6662,11 @@ and doStatement (s : A.statement) : chunk = in let (se3, _, _) = doExp false e3 ADrop in startLoop false; - let s' = doStatement s in currentLoc := loc'; currentExpLoc := eloc'; + let s' = doStatement s in + currentLoc := {loc' with synthetic = true}; + currentExpLoc := {eloc' with synthetic = true}; let s'' = consLabContinue se3 in let break_cond = breakChunk loc' in (* TODO: use eloc'? *) exitLoop (); From 8bbbc1791a8ae1a8a568f02eda2ecf61e8e048ab Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 12:58:52 +0300 Subject: [PATCH 3/8] Add more precise locations to initializer assignments --- src/frontc/cabs2cil.ml | 3 +++ src/frontc/cabshelper.ml | 2 ++ src/frontc/cparser.mly | 4 ++-- 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 76d0e06f4..4d60a5e0d 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -5885,6 +5885,9 @@ 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 diff --git a/src/frontc/cabshelper.ml b/src/frontc/cabshelper.ml index 451936510..f222176d3 100644 --- a/src/frontc/cabshelper.ml +++ b/src/frontc/cabshelper.ml @@ -29,6 +29,8 @@ let string_of_loc l = let joinLoc l1 l2 = match l1, l2 with | l1, l2 when l1.filename = l2.filename && l1.endByteno < 0 && l2.endByteno < 0 && l1.byteno <= l2.byteno -> {l1 with endLineno = l2.lineno; endByteno = l2.byteno; endColumnno = l2.columnno} + | l1, l2 when l1.filename = l2.filename && l1.endByteno < l2.byteno && l2.endByteno < 0 && l1.byteno <= l2.byteno -> + {l1 with endLineno = l2.lineno; endByteno = l2.byteno; endColumnno = l2.columnno} | l1, l2 when l1.filename = l2.filename && l1.endByteno = l2.endByteno && l1.byteno = l2.byteno -> l1 (* alias fundefs *) | _, _ -> diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index e1e9a65b8..8b96506a8 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -1036,8 +1036,8 @@ init_declarator_attr: ; init_declarator: /* ISO 6.7 */ declarator { ($1, NO_INIT) } -| declarator EQ init_expression - { ($1, $3) } +| declarator EQ init_expression location + { let (n, d, a, l) = $1 in ((n, d, a, joinLoc l $4), $3) } ; decl_spec_list_common: /* ISO 6.7 */ From bbd2561561b65ca1a4e2582d17f24081a8c95f59 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 15:01:52 +0300 Subject: [PATCH 4/8] Change intermediate exp/init side effect locs to synthetic --- src/frontc/cabs2cil.ml | 60 +++++++++++++++++++++++++++++++++++++----- 1 file changed, 53 insertions(+), 7 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 4d60a5e0d..ea3c0075d 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -840,6 +840,52 @@ module BlockChunk = let isNotEmpty (c: chunk) = not (isEmpty c) + (** Change all stmt and instr locs to synthetic, except the first one. + Expressions/initializers that expand to multiple instructions cannot have intermediate locations referenced. *) + let synthesizeLocs (c: chunk): chunk = + (* ignore (Pretty.eprintf "synthesizeLocs %a\n" d_chunk c); *) + let doLoc l = + (* ignore (Pretty.eprintf "synthesizeLoc %a in %a\n" d_loc l d_chunk c); *) + {l with synthetic = true} + in + let doInstr: instr -> instr = function + | Set (l, e, loc, eloc) -> Set (l, e, doLoc loc, doLoc eloc) + | VarDecl (v, loc) -> VarDecl (v, doLoc loc) + | Call (l, f, a, loc, eloc) -> Call (l, f, a, doLoc loc, doLoc eloc) + | Asm (a, b, c, d, e, loc) -> Asm (a, b, c, d, e, doLoc loc) + in + let doInstrs ~first = function + | [] -> [] + | x :: xs when first -> x :: List.map doInstr xs + | xs -> List.map doInstr xs + in + let rec doStmt ~first s = + let skind' = + let doLoc = if first then doLoc else Fun.id in + match s.skind with + | Instr xs -> Instr (doInstrs ~first xs) + | Return (e, loc) -> Return (e, doLoc loc) + | 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 (c, t, f, loc, eloc) -> If (c, doBlock ~first:false t, doBlock ~first:false f, doLoc loc, doLoc eloc) + | Switch (e, b, s, loc, eloc) -> Switch (e, doBlock ~first:false b, doStmts ~first:false s, doLoc loc, doLoc eloc) + | Loop (b, loc, eloc, s1, s2) -> Loop (doBlock ~first:false b, doLoc loc, doLoc eloc, Option.map (doStmt ~first:false) s1, Option.map (doStmt ~first:false) s2) + | Block b -> Block (doBlock ~first b) + in + {s with skind = skind'} + and doBlock ~first b = + {b with bstmts = doStmts ~first b.bstmts} + and doStmts ~first = function + | [] -> [] + | x :: xs -> doStmt ~first x :: List.map (doStmt ~first:false) xs + in + match c.stmts, c.postins with + | [], [] -> c + | [], postins -> {c with postins = List.rev (doInstrs ~first:true (List.rev postins))} + | stmts, postins -> {c with stmts = doStmts ~first:true stmts; postins = List.rev (doInstrs ~first:false (List.rev postins))} + let i2c (i: instr) = { empty with postins = [i] } @@ -3352,9 +3398,9 @@ and doExp (asconst: bool) (* This expression is used as a constant *) (se: chunk) (e: exp) (t: typ) : chunk * exp * typ = match newWhat with ADrop - | AType -> (se, e, t) + | AType -> (synthesizeLocs se, e, t) | AExpLeaveArrayFun -> - (se, e, t) (* It is important that we do not do "processArrayFun" in + (synthesizeLocs se, e, t) (* It is important that we do not do "processArrayFun" in * this case. We exploit this when we process the typeOf * construct *) | AExp _ -> @@ -3363,20 +3409,20 @@ and doExp (asconst: bool) (* This expression is used as a constant *) ignore (E.log "finishExp: e'=%a, t'=%a\n" d_exp e' d_type t'); *) - (se, e', t') + (synthesizeLocs se, e', t') | ASet (lv, lvt) -> begin (* See if the set was done already *) match e with Lval(lv') when lv == lv' -> - (se, e, t) + (synthesizeLocs se, e, t) | _ -> let (e', t') = processArrayFun e t in let (t'', e'') = castTo t' lvt e' in (* ignore (E.log "finishExp: e = %a\n e'' = %a\n" d_plainexp e d_plainexp e''); *) - (se +++ (Set(lv, e'', !currentLoc, !currentExpLoc)), e'', t'') + (synthesizeLocs (se +++ (Set(lv, e'', !currentLoc, !currentExpLoc))), e'', t'') end in let findField (n: string) (fidlist: fieldinfo list) : offset = @@ -5909,8 +5955,8 @@ and doDecl (isglobal: bool) : A.definition -> chunk = function acc end else match spec_res with - | Some spec_res -> acc @@ createLocal spec_res name - | None -> acc @@ createAutoLocal name + | Some spec_res -> acc @@ synthesizeLocs (createLocal spec_res name) + | None -> acc @@ synthesizeLocs (createAutoLocal name) in let res = List.fold_left doOneDeclarator empty nl in (* From 089694673e2881aa867a11108a089d0237d91aef Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 15:39:19 +0300 Subject: [PATCH 5/8] Change synthesizeLocs to mutate stmts --- src/frontc/cabs2cil.ml | 42 ++++++++++++++++++++++++++++-------------- 1 file changed, 28 insertions(+), 14 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index ea3c0075d..32bb77b38 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -859,32 +859,46 @@ module BlockChunk = | x :: xs when first -> x :: List.map doInstr xs | xs -> List.map doInstr xs in - let rec doStmt ~first s = - let skind' = - let doLoc = if first then doLoc else Fun.id in - match s.skind with + (* must mutate stmts in order to not break refs (for gotos) *) + let rec doStmt ~first s: unit = + let doLoc = if first then doLoc else Fun.id in + s.skind <- match s.skind with | Instr xs -> Instr (doInstrs ~first xs) | Return (e, loc) -> Return (e, doLoc loc) | 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 (c, t, f, loc, eloc) -> If (c, doBlock ~first:false t, doBlock ~first:false f, doLoc loc, doLoc eloc) - | Switch (e, b, s, loc, eloc) -> Switch (e, doBlock ~first:false b, doStmts ~first:false s, doLoc loc, doLoc eloc) - | Loop (b, loc, eloc, s1, s2) -> Loop (doBlock ~first:false b, doLoc loc, doLoc eloc, Option.map (doStmt ~first:false) s1, Option.map (doStmt ~first:false) s2) - | Block b -> Block (doBlock ~first b) - in - {s with skind = skind'} + | If (c, t, f, loc, eloc) -> + doBlock ~first:false t; + doBlock ~first:false f; + If (c, t, f, doLoc loc, doLoc eloc) + | Switch (e, b, s, loc, eloc) -> + doBlock ~first:false b; + doStmts ~first:false s; + Switch (e, b, s, doLoc loc, doLoc eloc) + | Loop (b, loc, eloc, s1, s2) -> + doBlock ~first:false b; + Option.iter (doStmt ~first:false) s1; + Option.iter (doStmt ~first:false) s2; + Loop (b, doLoc loc, doLoc eloc, s1, s2) + | Block b -> + doBlock ~first b; + s.skind and doBlock ~first b = - {b with bstmts = doStmts ~first b.bstmts} + doStmts ~first b.bstmts and doStmts ~first = function - | [] -> [] - | x :: xs -> doStmt ~first x :: List.map (doStmt ~first:false) xs + | [] -> () + | x :: xs -> + doStmt ~first x; + List.iter (doStmt ~first:false) xs in match c.stmts, c.postins with | [], [] -> c | [], postins -> {c with postins = List.rev (doInstrs ~first:true (List.rev postins))} - | stmts, postins -> {c with stmts = doStmts ~first:true stmts; postins = List.rev (doInstrs ~first:false (List.rev postins))} + | stmts, postins -> + doStmts ~first:true stmts; + {c with postins = List.rev (doInstrs ~first:false (List.rev postins))} let i2c (i: instr) = { empty with postins = [i] } From 65d4c8ae97cc0e0e11489c86df902d1e7a20c1f6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 15:39:40 +0300 Subject: [PATCH 6/8] Avoid Fun.id to support old OCaml versions --- src/frontc/cabs2cil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 32bb77b38..652b61ae0 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -861,7 +861,7 @@ module BlockChunk = in (* must mutate stmts in order to not break refs (for gotos) *) let rec doStmt ~first s: unit = - let doLoc = if first then doLoc else Fun.id in + let doLoc = if first then doLoc else fun x -> x in s.skind <- match s.skind with | Instr xs -> Instr (doInstrs ~first xs) | Return (e, loc) -> Return (e, doLoc loc) From 9c465b311fa36cbe8d3c9650c3de9406e9f73295 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 14 Jun 2022 15:49:33 +0300 Subject: [PATCH 7/8] Avoid Option.iter to support old OCaml versions --- src/frontc/cabs2cil.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 652b61ae0..8ee55ad78 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -879,8 +879,9 @@ module BlockChunk = Switch (e, b, s, doLoc loc, doLoc eloc) | Loop (b, loc, eloc, s1, s2) -> doBlock ~first:false b; - Option.iter (doStmt ~first:false) s1; - Option.iter (doStmt ~first:false) s2; + let option_iter f = function Some v -> f v | None -> () in (* Option.iter for older OCaml versions *) + option_iter (doStmt ~first:false) s1; + option_iter (doStmt ~first:false) s2; Loop (b, doLoc loc, doLoc eloc, s1, s2) | Block b -> doBlock ~first b; From 3a4c3c40187ac9ba9007019ab396759532187bc2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 17 Jun 2022 14:41:00 +0300 Subject: [PATCH 8/8] Improve synthetic location documentation --- src/cil.ml | 3 ++- src/cil.mli | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 8ba7918d4..e47ca571c 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -868,7 +868,8 @@ and location = { endLine: int; (** End line number. Negative means unknown. *) endByte: int; (** End byte position. Negative means unknown. *) endColumn: int; (** End column number. Negative means unknown. *) - synthetic: bool; (** Synthetic location, doesn't precisely match source. *) + synthetic: bool; (** Synthetic location, doesn't necessarily precisely correspond to a location in original source code, e.g. due to CIL transformations. + @see for some examples. *) } (* Type signatures. Two types are identical iff they have identical diff --git a/src/cil.mli b/src/cil.mli index cded7760c..6374b7354 100644 --- a/src/cil.mli +++ b/src/cil.mli @@ -1103,7 +1103,8 @@ and location = { endLine: int; (** End line number. Negative means unknown. *) endByte: int; (** End byte position. Negative means unknown. *) endColumn: int; (** End column number. Negative means unknown. *) - synthetic: bool; (** Synthetic location, doesn't precisely match source. *) + synthetic: bool; (** Synthetic location, doesn't necessarily precisely correspond to a location in original source code, e.g. due to CIL transformations. + @see for some examples. *) }