Merge pull request #97 from goblint/frontc-standalone-exp

Expose standalone expression parsing via Frontc

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

src/frontc/cabs2cil.mli

@@ -106,3 +106,8 @@ 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
+
+val currentFunctionFDEC: Cil.fundec ref

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 *)

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 ()

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 <Cabs.definition list> file interpret globals
 
 %type <Cabs.definition> global
@@ -356,7 +356,7 @@ let transformOffsetOf (speclist, dtype) member =
 %type <Cabs.statement> statement
 %type <Cabs.constant * cabsloc> constant
 %type <int64 list Queue.t * Cabs.wchar_type * cabsloc> string_list
-%type <Cabs.expression * cabsloc> expression
+%type <Cabs.expression * Cabs.cabsloc> expression
 %type <Cabs.expression> opt_expression
 %type <Cabs.init_expression> init_expression
 %type <Cabs.expression list * cabsloc> comma_expression

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

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