diff options
Diffstat (limited to 'cil/src/formatcil.ml')
-rw-r--r-- | cil/src/formatcil.ml | 215 |
1 files changed, 215 insertions, 0 deletions
diff --git a/cil/src/formatcil.ml b/cil/src/formatcil.ml new file mode 100644 index 00000000..33bc749f --- /dev/null +++ b/cil/src/formatcil.ml @@ -0,0 +1,215 @@ +(* + * + * Copyright (c) 2001-2002, + * George C. Necula <necula@cs.berkeley.edu> + * Scott McPeak <smcpeak@cs.berkeley.edu> + * Wes Weimer <weimer@cs.berkeley.edu> + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are + * met: + * + * 1. Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * + * 3. The names of the contributors may not be used to endorse or promote + * products derived from this software without specific prior written + * permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS + * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED + * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A + * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER + * OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, + * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, + * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR + * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF + * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + * + *) +open Cil +open Pretty +open Trace (* sm: 'trace' function *) +module E = Errormsg +module H = Hashtbl + +let noMemoize = ref false + +let expMemoTable : + (string, (((string * formatArg) list -> exp) * + (exp -> formatArg list option))) H.t = H.create 23 + +let typeMemoTable : + (string, (((string * formatArg) list -> typ) * + (typ -> formatArg list option))) H.t = H.create 23 + +let lvalMemoTable : + (string, (((string * formatArg) list -> lval) * + (lval -> formatArg list option))) H.t = H.create 23 + +let instrMemoTable : + (string, ((location -> (string * formatArg) list -> instr) * + (instr -> formatArg list option))) H.t = H.create 23 + +let stmtMemoTable : + (string, ((string -> typ -> varinfo) -> + location -> + (string * formatArg) list -> stmt)) H.t = H.create 23 + +let stmtsMemoTable : + (string, ((string -> typ -> varinfo) -> + location -> + (string * formatArg) list -> stmt list)) H.t = H.create 23 + + +let doParse (prog: string) + (theParser: (Lexing.lexbuf -> Formatparse.token) + -> Lexing.lexbuf -> 'a) + (memoTable: (string, 'a) H.t) : 'a = + try + if !noMemoize then raise Not_found else + H.find memoTable prog + with Not_found -> begin + let lexbuf = Formatlex.init prog in + try + Formatparse.initialize Formatlex.initial lexbuf; + let res = theParser Formatlex.initial lexbuf in + H.add memoTable prog res; + Formatlex.finish (); + res + with Parsing.Parse_error -> begin + Formatlex.finish (); + E.s (E.error "Parsing error: %s" prog) + end + | e -> begin + ignore (E.log "Caught %s while parsing\n" (Printexc.to_string e)); + Formatlex.finish (); + raise e + end + end + + +let cExp (prog: string) : (string * formatArg) list -> exp = + let cf = doParse prog Formatparse.expression expMemoTable in + (fst cf) + +let cLval (prog: string) : (string * formatArg) list -> lval = + let cf = doParse prog Formatparse.lval lvalMemoTable in + (fst cf) + +let cType (prog: string) : (string * formatArg) list -> typ = + let cf = doParse prog Formatparse.typename typeMemoTable in + (fst cf) + +let cInstr (prog: string) : location -> (string * formatArg) list -> instr = + let cf = doParse prog Formatparse.instr instrMemoTable in + (fst cf) + +let cStmt (prog: string) : (string -> typ -> varinfo) -> + location -> (string * formatArg) list -> stmt = + let cf = doParse prog Formatparse.stmt stmtMemoTable in + cf + +let cStmts (prog: string) : + (string -> typ -> varinfo) -> + location -> (string * formatArg) list -> stmt list = + let cf = doParse prog Formatparse.stmt_list stmtsMemoTable in + cf + + + +(* Match an expression *) +let dExp (prog: string) : exp -> formatArg list option = + let df = doParse prog Formatparse.expression expMemoTable in + (snd df) + +(* Match an lvalue *) +let dLval (prog: string) : lval -> formatArg list option = + let df = doParse prog Formatparse.lval lvalMemoTable in + (snd df) + + +(* Match a type *) +let dType (prog: string) : typ -> formatArg list option = + let df = doParse prog Formatparse.typename typeMemoTable in + (snd df) + + + +(* Match an instruction *) +let dInstr (prog: string) : instr -> formatArg list option = + let df = doParse prog Formatparse.instr instrMemoTable in + (snd df) + + +let test () = + (* Construct a dummy function *) + let func = emptyFunction "test_formatcil" in + (* Construct a few varinfo *) + let res = makeLocalVar func "res" (TPtr(intType, [])) in + let fptr = makeLocalVar func "fptr" + (TPtr(TFun(intType, None, false, []), [])) in + (* Construct an instruction *) + let makeInstr () = + Call(Some (var res), + Lval (Mem (CastE(TPtr(TFun(TPtr(intType, []), + Some [ ("", intType, []); + ("a2", TPtr(intType, []), []); + ("a3", TPtr(TPtr(intType, []), + []), []) ], + false, []), []), + Lval (var fptr))), + NoOffset), + [ ], locUnknown) + in + let times = 100000 in + (* Make the instruction the regular way *) + Stats.time "make instruction regular" + (fun _ -> for i = 0 to times do ignore (makeInstr ()) done) + (); + (* Now make the instruction interpreted *) + noMemoize := true; + Stats.time "make instruction interpreted" + (fun _ -> for i = 0 to times do + let _ = + cInstr "%v:res = (* ((int * (*)(int, int * a2, int * * a3))%v:fptr))();" + locUnknown [ ("res", Fv res); + ("fptr", Fv fptr) ] + in + () + done) + (); + (* Now make the instruction interpreted with memoization *) + noMemoize := false; + Stats.time "make instruction interpreted memoized" + (fun _ -> for i = 0 to times do + let _ = + cInstr "%v:res = (* ((int * (*)(int, int * a2, int * * a3))%v:fptr))();" + locUnknown [ ("res", Fv res); ("fptr", Fv fptr) ] + in + () + done) + (); + (* Now make the instruction interpreted with partial application *) + let partInstr = + cInstr "%v:res = (* ((int * (*)(int, int * a2, int * * a3))%v:fptr))();" in + Stats.time "make instruction interpreted partial" + (fun _ -> for i = 0 to times do + let _ = + partInstr + locUnknown [ ("res", Fv res); ("fptr", Fv fptr) ] + in + () + done) + (); + + () + + |