From a6c158d8db352f38db0ad026e22128321031e185 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 26 May 2022 10:07:20 +0300 Subject: [PATCH 1/2] Expose standalone expression parsing via Frontc --- src/frontc/cabs2cil.ml | 46 ++++++++++++++++++++++++++++++++++++++++- src/frontc/cabs2cil.mli | 3 +++ src/frontc/clexer.mli | 1 + src/frontc/clexer.mll | 12 +++++++++++ src/frontc/cparser.mly | 4 ++-- src/frontc/frontc.ml | 25 ++++++++++++++++++++++ src/frontc/frontc.mli | 2 ++ 7 files changed, 90 insertions(+), 3 deletions(-) diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index c60c29727..a29fe913e 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -332,6 +332,7 @@ let env : (string, envdata * location) H.t = H.create 307 (* Just like env, except that it simply collects all the information (i.e. entries * are never removed and it is also not emptied after every file). *) let environment : (string, envdata * location) H.t = H.create 307 +let genvironment : (string, envdata * location) H.t = H.create 307 (* We also keep a global environment. This is always a subset of the env *) let genv : (string, envdata * location) H.t = H.create 307 @@ -373,7 +374,8 @@ let addGlobalToEnv (k: string) (d: envdata) : unit = H.add env k (d, !currentLoc); H.add environment k (d, !currentLoc); (* Also add it to the global environment *) - H.add genv k (d, !currentLoc) + H.add genv k (d, !currentLoc); + H.add genvironment k (d, !currentLoc) @@ -6988,3 +6990,45 @@ let convFile (f : A.file) : Cil.file = globinit = None; globinitcalled = false; } + + +let convStandaloneExp ~genv:genv' ~env:env' (e : A.expression) : Cil.exp option = + Cil.initCIL (); (* make sure we have initialized CIL *) + + (* remove parentheses from the Cabs *) + let e = V.visitCabsExpression (new stripParenClass) e in + + (* Clean up the global types *) + initGlobals(); + startFile (); + IH.clear noProtoFunctions; + H.clear compInfoNameEnv; + H.clear enumInfoNameEnv; + IH.clear mustTurnIntoDef; + H.clear alreadyDefined; + H.clear staticLocals; + H.clear typedefs; + H.clear isomorphicStructs; + annonCompFieldNameId := 0; + if !E.verboseFlag || !Cilutil.printStages then + ignore (E.log "Converting CABS->CIL\n"); + + H.iter (H.add genv) genv'; + H.iter (H.add env) env'; + + let cil_exp = doPureExp e in + + IH.clear noProtoFunctions; + IH.clear mustTurnIntoDef; + H.clear alreadyDefined; + H.clear compInfoNameEnv; + H.clear enumInfoNameEnv; + H.clear isomorphicStructs; + H.clear staticLocals; + H.clear typedefs; + H.clear env; + H.clear genv; + IH.clear callTempVars; + + (* We are done *) + cil_exp diff --git a/src/frontc/cabs2cil.mli b/src/frontc/cabs2cil.mli index 49ce1d1a7..9b62a954d 100644 --- a/src/frontc/cabs2cil.mli +++ b/src/frontc/cabs2cil.mli @@ -106,3 +106,6 @@ type envdata = (** A hashtable containing a mapping of variables, enums, types and labels to varinfo, typ, etc. *) (* It enables a lookup of the original variable names before the alpha conversion by cabs2cil *) val environment : (string, envdata * Cil.location) Hashtbl.t +val genvironment : (string, envdata * Cil.location) Hashtbl.t + +val convStandaloneExp: genv:(string, envdata * Cil.location) Hashtbl.t -> env:(string, envdata * Cil.location) Hashtbl.t -> Cabs.expression -> Cil.exp option diff --git a/src/frontc/clexer.mli b/src/frontc/clexer.mli index 5d90b4ebe..f32e60a7a 100644 --- a/src/frontc/clexer.mli +++ b/src/frontc/clexer.mli @@ -43,6 +43,7 @@ val init: filename:string -> Lexing.lexbuf +val initFromString: string -> Lexing.lexbuf val finish: unit -> unit (* This is the main parser function *) diff --git a/src/frontc/clexer.mll b/src/frontc/clexer.mll index 7e1385b20..37872c72a 100644 --- a/src/frontc/clexer.mll +++ b/src/frontc/clexer.mll @@ -283,6 +283,18 @@ let init ~(filename: string) : Lexing.lexbuf = Lexerhack.add_identifier := add_identifier; E.startParsing filename +let initFromString (s: string) : Lexing.lexbuf = + init_lexicon (); + (* Inititialize the pointer in Errormsg *) + Lexerhack.add_type := add_type; + (* add some built-in types which are handled as Tnamed in cabs2cil *) + add_type "__int128_t"; (* __int128 *) + add_type "__uint128_t"; (* unsigned __int128 *) + Lexerhack.push_context := push_context; + Lexerhack.pop_context := pop_context; + Lexerhack.add_identifier := add_identifier; + E.startParsingFromString s + let finish () = E.finishParsing () diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly index 7e76f54c0..e1e9a65b8 100644 --- a/src/frontc/cparser.mly +++ b/src/frontc/cparser.mly @@ -346,7 +346,7 @@ let transformOffsetOf (speclist, dtype) member = %left IDENT /* Non-terminals informations */ -%start interpret file +%start interpret file expression %type file interpret globals %type global @@ -356,7 +356,7 @@ let transformOffsetOf (speclist, dtype) member = %type statement %type constant %type string_list -%type expression +%type expression %type opt_expression %type init_expression %type comma_expression diff --git a/src/frontc/frontc.ml b/src/frontc/frontc.ml index 52c1cc960..35652b2a6 100644 --- a/src/frontc/frontc.ml +++ b/src/frontc/frontc.ml @@ -264,3 +264,28 @@ let parse_helper fname = let parse fname = (fun () -> snd(parse_helper fname ())) let parse_with_cabs fname = (fun () -> parse_helper fname ()) + +let parse_standalone_exp s = + try + if !E.verboseFlag then ignore (E.log "Frontc is parsing string: %s\n" s); + flush !E.logChannel; + (* if !E.verboseFlag then ignore @@ Parsing.set_trace true; *) + let lexbuf = Clexer.initFromString s in + let (cabs, _) = Stats.time "parse" (Cparser.expression (Whitetrack.wraplexer clexer)) lexbuf in + Whitetrack.setFinalWhite (Clexer.get_white ()); + Clexer.finish (); + cabs + with + | Parsing.Parse_error -> begin + ignore (E.log "Parsing error"); + Clexer.finish (); + close_output (); + (* raise (ParseError("Parse error")) *) + let backtrace = Printexc.get_raw_backtrace () in + Printexc.raise_with_backtrace (ParseError("Parse error")) backtrace (* re-raise with captured inner backtrace *) + end + | e -> begin + ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e)); + Clexer.finish (); + raise e + end diff --git a/src/frontc/frontc.mli b/src/frontc/frontc.mli index 2a903393e..930b8d3ec 100644 --- a/src/frontc/frontc.mli +++ b/src/frontc/frontc.mli @@ -50,3 +50,5 @@ val args: (string * Arg.spec * string) list val parse: string -> (unit -> Cil.file) val parse_with_cabs: string -> (unit -> Cabs.file * Cil.file) + +val parse_standalone_exp: string -> Cabs.expression From fe7da7b4203735d84670e68f3044a9bf33bd6e65 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 26 May 2022 10:50:11 +0300 Subject: [PATCH 2/2] Expose Cabs2cil.currentFunctionFDEC This can be set from Goblint before convStandaloneExp. --- src/frontc/cabs2cil.mli | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontc/cabs2cil.mli b/src/frontc/cabs2cil.mli index 9b62a954d..4af8ea2d3 100644 --- a/src/frontc/cabs2cil.mli +++ b/src/frontc/cabs2cil.mli @@ -109,3 +109,5 @@ val environment : (string, envdata * Cil.location) Hashtbl.t val genvironment : (string, envdata * Cil.location) Hashtbl.t val convStandaloneExp: genv:(string, envdata * Cil.location) Hashtbl.t -> env:(string, envdata * Cil.location) Hashtbl.t -> Cabs.expression -> Cil.exp option + +val currentFunctionFDEC: Cil.fundec ref