From 86cec5272cffc55638b0d8098cb7301685ead01e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 12:15:13 +0200 Subject: [PATCH 1/4] Attempt add adding attribute when nested --- src/frontc/cabs2cil.ml | 17 ++++++++++++++--- src/frontc/cabs2cil.mli | 6 ++++++ 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 52d3a2c3f..4b3dd42e0 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -75,6 +75,13 @@ let nocil: int ref = ref (-1) *) let alwaysGenerateVarDecl = false +(** Add an attribute to all variables which are not declared at the top scope, + so tools building on CIL can know which variables were pulled up. + Should be disabled when printing CIL code, as compilers will warn about this attribute. +*) +let addNestedScopeAttr = ref true +let body_nest_count = ref 0 + (** Indicates whether we're allowed to duplicate small chunks. *) let allowDuplication: bool ref = ref true @@ -557,9 +564,11 @@ let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo = in (* Store all locals in the slocals (in reversed order). We'll reverse them and take out the formals at the end of the function *) - if not vi.vglob then - !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals; - + if not vi.vglob then( + if List.length !scopes > 1 then + newvi.vattr <- Attr("goblint_cil_nested", []) :: newvi.vattr; + !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals) + ; (if addtoenv then if vi.vglob then addGlobalToEnv vi.vname (EnvVar newvi) @@ -6618,6 +6627,7 @@ and assignInit (lv: lval) (* Now define the processors for body and statement *) and doBody (blk: A.block) : chunk = + body_nest_count := !body_nest_count + 1; enterScope (); (* Rename the labels and add them to the environment *) List.iter (fun l -> ignore (genNewLocalLabel l)) blk.blabels; @@ -6632,6 +6642,7 @@ and doBody (blk: A.block) : chunk = empty blk.A.bstmts) in + body_nest_count := !body_nest_count - 1; exitScope (); diff --git a/src/frontc/cabs2cil.mli b/src/frontc/cabs2cil.mli index e2e2a4843..b7b6c719c 100644 --- a/src/frontc/cabs2cil.mli +++ b/src/frontc/cabs2cil.mli @@ -45,6 +45,12 @@ val forceRLArgEval: bool ref -1 to disable *) val nocil: int ref +(** Add an attribute to all variables which are not declared at the top scope, + so tools building on CIL can know which variables were pulled up. + Should be disabled when printing CIL code, as compilers will warn about this attribute. +*) +val addNestedScopeAttr: bool ref + (** Indicates whether we're allowed to duplicate small chunks of code. *) val allowDuplication: bool ref From df6a5fc71b9e8f72857d77e3c492a93f344b26ff Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 12:19:37 +0200 Subject: [PATCH 2/4] bump threshold --- 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 4b3dd42e0..a9413917a 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -565,7 +565,7 @@ let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo = (* Store all locals in the slocals (in reversed order). We'll reverse them and take out the formals at the end of the function *) if not vi.vglob then( - if List.length !scopes > 1 then + if List.length !scopes > 2 then newvi.vattr <- Attr("goblint_cil_nested", []) :: newvi.vattr; !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals) ; From dbf7fcdaa1d2e8a9916ca0fd379eb802cb34973b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 12:35:25 +0200 Subject: [PATCH 3/4] Rewrite code to be a bit more efficient --- src/frontc/cabs2cil.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index a9413917a..0c0c604d2 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -564,10 +564,18 @@ let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo = in (* Store all locals in the slocals (in reversed order). We'll reverse them and take out the formals at the end of the function *) - if not vi.vglob then( - if List.length !scopes > 2 then - newvi.vattr <- Attr("goblint_cil_nested", []) :: newvi.vattr; - !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals) + if not vi.vglob then ( + (if !addNestedScopeAttr then + (* two scopes implies top-level scope in the function, one is created for the FUNDEF (includes formals etc), + one for the body which is a block *) + match !scopes with + | _::_::_::_ -> + (* i.e. List.length scopes > 2 *) + newvi.vattr <- Attr("goblint_cil_nested", []) :: newvi.vattr + | _ -> () + ); + !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals + ) ; (if addtoenv then if vi.vglob then From ae251652a4fd84bd8e30ebfb75eb01641f6f1740 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 12:36:45 +0200 Subject: [PATCH 4/4] Cleanup, set default for new attribute to false --- src/frontc/cabs2cil.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index 0c0c604d2..616669caa 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -79,8 +79,7 @@ let alwaysGenerateVarDecl = false so tools building on CIL can know which variables were pulled up. Should be disabled when printing CIL code, as compilers will warn about this attribute. *) -let addNestedScopeAttr = ref true -let body_nest_count = ref 0 +let addNestedScopeAttr = ref false (** Indicates whether we're allowed to duplicate small chunks. *) let allowDuplication: bool ref = ref true @@ -6635,7 +6634,6 @@ and assignInit (lv: lval) (* Now define the processors for body and statement *) and doBody (blk: A.block) : chunk = - body_nest_count := !body_nest_count + 1; enterScope (); (* Rename the labels and add them to the environment *) List.iter (fun l -> ignore (genNewLocalLabel l)) blk.blabels; @@ -6650,7 +6648,6 @@ and doBody (blk: A.block) : chunk = empty blk.A.bstmts) in - body_nest_count := !body_nest_count - 1; exitScope ();