--- /dev/null
+#! /bin/sh /usr/share/dpatch/dpatch-run
+## 001_tinyos.dpatch by <rsmckown@gmail.com>
+##
+## All lines beginning with `## DP:' are a description of the patch.
+## DP: http://www.stanford.edu/tinyos/toolchain/repo/deputy.patch,
+## DP: adjusted for use with dpatch (patch from one level up).
+
+@DPATCH@
+
+diff -urN deputy-tinyos-1.1.orig/bin/deputy deputy-tinyos-1.1/bin/deputy
+--- deputy-tinyos-1.1.orig/bin/deputy 2008-08-07 08:25:12.000000000 -0600
++++ deputy-tinyos-1.1/bin/deputy 2008-08-27 08:41:22.000000000 -0600
+@@ -51,7 +51,7 @@
+ $::deputyhome = "$FindBin::RealBin/..";
+
+ # Now force the libc patch.
+-if (! grep { $_ eq "--linux" } @ARGV) {
++if ((! grep { $_ eq "--linux" } @ARGV) && (! grep(/--nolib/, @ARGV))) {
+ push @ARGV, "--patch=$::deputyhome/include/libc_patch.i";
+ }
+
+diff -urN deputy-tinyos-1.1.orig/cil/src/cil.ml deputy-tinyos-1.1/cil/src/cil.ml
+--- deputy-tinyos-1.1.orig/cil/src/cil.ml 2008-08-07 08:25:14.000000000 -0600
++++ deputy-tinyos-1.1/cil/src/cil.ml 2008-08-27 08:41:22.000000000 -0600
+@@ -1223,6 +1223,13 @@
+ | CastE(_, e) -> isInteger e
+ | _ -> None
+
++let rec isIntegerKind : exp -> ikind option = function
++ | Const(CInt64 (_,k,_)) -> Some k
++ | Const(CChr c) -> Some IInt
++ | Const(CEnum(v, s, ei)) -> isIntegerKind v
++ | CastE(_, e) -> isIntegerKind e
++ | _ -> None
++
+
+ (** Convert a 64-bit int to an OCaml int, or raise an exception if that
+ can't be done. *)
+diff -urN deputy-tinyos-1.1.orig/cil/src/cil.mli deputy-tinyos-1.1/cil/src/cil.mli
+--- deputy-tinyos-1.1.orig/cil/src/cil.mli 2008-08-07 08:25:14.000000000 -0600
++++ deputy-tinyos-1.1/cil/src/cil.mli 2008-08-27 08:41:22.000000000 -0600
+@@ -1612,6 +1612,11 @@
+ Otherwise, return None. *)
+ val isInteger: exp -> int64 option
+
++(** If the given expression is a (possibly cast'ed)
++ character or an integer constant, return that integer's kind.
++ Otherwise, return None. *)
++val isIntegerKind: exp -> ikind option
++
+ (** Convert a 64-bit int to an OCaml int, or raise an exception if that
+ can't be done. *)
+ val i64_to_int: int64 -> int
+diff -urN deputy-tinyos-1.1.orig/cil/src/frontc/cabs2cil.ml deputy-tinyos-1.1/cil/src/frontc/cabs2cil.ml
+--- deputy-tinyos-1.1.orig/cil/src/frontc/cabs2cil.ml 2008-08-07 08:25:14.000000000 -0600
++++ deputy-tinyos-1.1/cil/src/frontc/cabs2cil.ml 2008-08-27 08:41:22.000000000 -0600
+@@ -2379,9 +2379,10 @@
+ | (kname, e, cloc) :: rest ->
+ (* constant-eval 'e' to determine tag value *)
+ let e' = getIntConstExp e in
++ let c' = constFold true e' in
+ let e' =
+- match isInteger (constFold true e') with
+- Some i -> if !lowerConstants then kinteger64 IInt i else e'
++ match (isInteger c', isIntegerKind c') with
++ (Some i, Some ik) -> if !lowerConstants then kinteger64 ik i else e'
+ | _ -> E.s (error "Constant initializer %a not an integer" d_exp e')
+ in
+ processName kname e' (convLoc cloc) rest
+@@ -3147,7 +3148,7 @@
+ finishExp empty (Lval(var vi)) vi.vtype
+ | EnvEnum (tag, typ), _ ->
+ if !Cil.lowerConstants then
+- finishExp empty tag typ
++ finishExp empty tag (typeOf tag)
+ else begin
+ let ei =
+ match unrollType typ with
+diff -urN deputy-tinyos-1.1.orig/cil/src/frontc/cabs2cil.ml.orig deputy-tinyos-1.1/cil/src/frontc/cabs2cil.ml.orig
+--- deputy-tinyos-1.1.orig/cil/src/frontc/cabs2cil.ml.orig 1969-12-31 17:00:00.000000000 -0700
++++ deputy-tinyos-1.1/cil/src/frontc/cabs2cil.ml.orig 2008-08-07 08:25:14.000000000 -0600
+@@ -0,0 +1,6380 @@
++(*
++ *
++ * 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.
++ *
++ *)
++
++(* Type check and elaborate ABS to CIL *)
++
++(* The references to ISO means ANSI/ISO 9899-1999 *)
++module A = Cabs
++module C = Cabshelper
++module V = Cabsvisit
++module E = Errormsg
++module H = Hashtbl
++module IH = Inthash
++module AL = Alpha
++
++open Cabs
++open Cabshelper
++open Pretty
++open Cil
++open Trace
++
++
++let mydebugfunction () =
++ E.s (error "mydebugfunction")
++
++let debugGlobal = false
++
++let continueOnError = true
++
++(** Turn on tranformation that forces correct parameter evaluation order *)
++let forceRLArgEval = ref false
++
++(** Leave a certain global alone. Use a negative number to disable. *)
++let nocil: int ref = ref (-1)
++
++(** Indicates whether we're allowed to duplicate small chunks. *)
++let allowDuplication: bool ref = ref true
++
++(** If false, the destination of a Call instruction should always have the
++ same type as the function's return type. Where needed, CIL will insert
++ a temporary to make this happen.
++
++ If true, the destination type may differ from the return type, so there
++ is an implicit cast. This is useful for analyses involving [malloc],
++ because the instruction "T* x = malloc(...);" won't be broken into
++ two instructions, so it's easy to find the allocation type.
++
++ This is false by default. Set to true to replicate the behavior
++ of CIL 1.3.5 and earlier.
++*)
++let doCollapseCallCast: bool ref = ref false
++
++(** Disables caching of globals during parsing. This is handy when we want
++ * to parse additional source files without hearing about confclits. *)
++let cacheGlobals: bool ref = ref true
++
++(** A hook into the code for processing typeof. *)
++let typeForTypeof: (Cil.typ -> Cil.typ) ref = ref (fun t -> t)
++
++(** A hook into the code that creates temporary local vars. By default this
++ is the identity function, but you can overwrite it if you need to change the
++ types of cabs2cil-introduced temp variables. *)
++let typeForInsertedVar: (Cil.typ -> Cil.typ) ref = ref (fun t -> t)
++
++(** Like [typeForInsertedVar], but for casts.
++ * Casts in the source code are exempt from this hook. *)
++let typeForInsertedCast: (Cil.typ -> Cil.typ) ref = ref (fun t -> t)
++
++(** A hook into the code that remaps argument names in the appropriate
++ * attributes. *)
++let typeForCombinedArg: ((string, string) H.t -> typ -> typ) ref =
++ ref (fun _ t -> t)
++
++(** A hook into the code that remaps argument names in the appropriate
++ * attributes. *)
++let attrsForCombinedArg: ((string, string) H.t ->
++ attributes -> attributes) ref =
++ ref (fun _ t -> t)
++
++(* ---------- source error message handling ------------- *)
++let lu = locUnknown
++let cabslu = {lineno = -10;
++ filename = "cabs lu";
++ byteno = -10;
++ ident = 0;}
++
++
++(** Interface to the Cprint printer *)
++let withCprint (f: 'a -> unit) (x: 'a) : unit =
++ Cprint.commit (); Cprint.flush ();
++ let old = !Cprint.out in
++ Cprint.out := !E.logChannel;
++ f x;
++ Cprint.commit (); Cprint.flush ();
++ flush !Cprint.out;
++ Cprint.out := old
++
++
++(** Keep a list of the variable ID for the variables that were created to
++ * hold the result of function calls *)
++let callTempVars: unit IH.t = IH.create 13
++
++(* Keep a list of functions that were called without a prototype. *)
++let noProtoFunctions : bool IH.t = IH.create 13
++
++(* Check that s starts with the prefix p *)
++let prefix p s =
++ let lp = String.length p in
++ let ls = String.length s in
++ lp <= ls && String.sub s 0 lp = p
++
++(***** COMPUTED GOTO ************)
++
++(* The address of labels are small integers (starting from 0). A computed
++ * goto is replaced with a switch on the address of the label. We generate
++ * only one such switch and we'll jump to it from all computed gotos. To
++ * accomplish this we'll add a local variable to store the target of the
++ * goto. *)
++
++(* The local variable in which to put the detination of the goto and the
++ * statement where to jump *)
++let gotoTargetData: (varinfo * stmt) option ref = ref None
++
++(* The "addresses" of labels *)
++let gotoTargetHash: (string, int) H.t = H.create 13
++let gotoTargetNextAddr: int ref = ref 0
++
++
++(********** TRANSPARENT UNION ******)
++(* Check if a type is a transparent union, and return the first field if it
++ * is *)
++let isTransparentUnion (t: typ) : fieldinfo option =
++ match unrollType t with
++ TComp (comp, _) when not comp.cstruct ->
++ (* Turn transparent unions into the type of their first field *)
++ if hasAttribute "transparent_union" (typeAttrs t) then begin
++ match comp.cfields with
++ f :: _ -> Some f
++ | _ -> E.s (unimp "Empty transparent union: %s" (compFullName comp))
++ end else
++ None
++ | _ -> None
++
++(* When we process an argument list, remember the argument index which has a
++ * transparent union type, along with the original type. We need this to
++ * process function definitions *)
++let transparentUnionArgs : (int * typ) list ref = ref []
++
++let debugLoc = false
++let convLoc (l : cabsloc) =
++ if debugLoc then
++ ignore (E.log "convLoc at %s: line %d, btye %d\n" l.filename l.lineno l.byteno);
++ {line = l.lineno; file = l.filename; byte = l.byteno;}
++
++
++let isOldStyleVarArgName n =
++ if !msvcMode then n = "va_alist"
++ else n = "__builtin_va_alist"
++
++let isOldStyleVarArgTypeName n =
++ if !msvcMode then n = "va_list" || n = "__ccured_va_list"
++ else n = "__builtin_va_alist_t"
++
++let isVariadicListType t =
++ match unrollType t with
++ | TBuiltin_va_list _ -> true
++ | _ -> false
++
++(* Weimer
++ * multi-character character constants
++ * In MSCV, this code works:
++ *
++ * long l1 = 'abcd'; // note single quotes
++ * char * s = "dcba";
++ * long * lptr = ( long * )s;
++ * long l2 = *lptr;
++ * assert(l1 == l2);
++ *
++ * We need to change a multi-character character literal into the
++ * appropriate integer constant. However, the plot sickens: we
++ * must also be able to handle things like 'ab\nd' (value = * "d\nba")
++ * and 'abc' (vale = *"cba").
++ *
++ * First we convert 'AB\nD' into the list [ 65 ; 66 ; 10 ; 68 ], then we
++ * multiply and add to get the desired value.
++ *)
++
++(* Given a character constant (like 'a' or 'abc') as a list of 64-bit
++ * values, turn it into a CIL constant. Multi-character constants are
++ * treated as multi-digit numbers with radix given by the bit width of
++ * the specified type (either char or wchar_t). *)
++let reduce_multichar typ : int64 list -> int64 =
++ let radix = bitsSizeOf typ in
++ List.fold_left
++ (fun acc -> Int64.add (Int64.shift_left acc radix))
++ Int64.zero
++
++let interpret_character_constant char_list =
++ let value = reduce_multichar charType char_list in
++ if value < (Int64.of_int 256) then
++ (* ISO C 6.4.4.4.10: single-character constants have type int *)
++ (CChr(Char.chr (Int64.to_int value))), intType
++ else begin
++ let orig_rep = None (* Some("'" ^ (String.escaped str) ^ "'") *) in
++ if value <= (Int64.of_int32 Int32.max_int) then
++ (CInt64(value,IULong,orig_rep)),(TInt(IULong,[]))
++ else
++ (CInt64(value,IULongLong,orig_rep)),(TInt(IULongLong,[]))
++ end
++
++(*** EXPRESSIONS *************)
++
++ (* We collect here the program *)
++let theFile : global list ref = ref []
++let theFileTypes : global list ref = ref []
++
++let initGlobals () = theFile := []; theFileTypes := []
++
++
++let cabsPushGlobal (g: global) =
++ pushGlobal g ~types:theFileTypes ~variables:theFile
++
++(* Keep track of some variable ids that must be turned into definitions. We
++ * do this when we encounter what appears a definition of a global but
++ * without initializer. We leave it a declaration because maybe down the road
++ * we see another definition with an initializer. But if we don't see any
++ * then we turn the last such declaration into a definition without
++ * initializer *)
++let mustTurnIntoDef: bool IH.t = IH.create 117
++
++(* Globals that have already been defined. Indexed by the variable name. *)
++let alreadyDefined: (string, location) H.t = H.create 117
++
++(* Globals that were created due to static local variables. We chose their
++ * names to be distinct from any global encountered at the time. But we might
++ * see a global with conflicting name later in the file. *)
++let staticLocals: (string, varinfo) H.t = H.create 13
++
++
++(* Typedefs. We chose their names to be distinct from any global encounterd
++ * at the time. But we might see a global with conflicting name later in the
++ * file *)
++let typedefs: (string, typeinfo) H.t = H.create 13
++
++let popGlobals () =
++ let rec revonto (tail: global list) = function
++ [] -> tail
++
++ | GVarDecl (vi, l) :: rest
++ when vi.vstorage != Extern && IH.mem mustTurnIntoDef vi.vid ->
++ IH.remove mustTurnIntoDef vi.vid;
++ revonto (GVar (vi, {init = None}, l) :: tail) rest
++
++ | x :: rest -> revonto (x :: tail) rest
++ in
++ revonto (revonto [] !theFile) !theFileTypes
++
++
++(********* ENVIRONMENTS ***************)
++
++(* The environment is kept in two distinct data structures. A hash table maps
++ * each original variable name into a varinfo (for variables, or an
++ * enumeration tag, or a type). (Note that the varinfo might contain an
++ * alpha-converted name different from that of the lookup name.) The Ocaml
++ * hash tables can keep multiple mappings for a single key. Each time the
++ * last mapping is returned and upon deletion the old mapping is restored. To
++ * keep track of local scopes we also maintain a list of scopes (represented
++ * as lists). *)
++type envdata =
++ EnvVar of varinfo (* The name refers to a variable
++ * (which could also be a function) *)
++ | EnvEnum of exp * typ (* The name refers to an enumeration
++ * tag for which we know the value
++ * and the host type *)
++ | EnvTyp of typ (* The name is of the form "struct
++ * foo", or "union foo" or "enum foo"
++ * and refers to a type. Note that
++ * the name of the actual type might
++ * be different from foo due to alpha
++ * conversion *)
++ | EnvLabel of string (* The name refers to a label. This
++ * is useful for GCC's locally
++ * declared labels. The lookup name
++ * for this category is "label foo" *)
++
++let env : (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
++
++ (* In the scope we keep the original name, so we can remove them from the
++ * hash table easily *)
++type undoScope =
++ UndoRemoveFromEnv of string
++ | UndoResetAlphaCounter of location AL.alphaTableData ref *
++ location AL.alphaTableData
++ | UndoRemoveFromAlphaTable of string
++
++let scopes : undoScope list ref list ref = ref []
++
++let isAtTopLevel () =
++ !scopes = []
++
++
++(* When you add to env, you also add it to the current scope *)
++let addLocalToEnv (n: string) (d: envdata) =
++(* ignore (E.log "%a: adding local %s to env\n" d_loc !currentLoc n); *)
++ H.add env n (d, !currentLoc);
++ (* If we are in a scope, then it means we are not at top level. Add the
++ * name to the scope *)
++ (match !scopes with
++ [] -> begin
++ match d with
++ EnvVar _ ->
++ E.s (E.bug "addLocalToEnv: not in a scope when adding %s!" n)
++ | _ -> () (* We might add types *)
++ end
++ | s :: _ ->
++ s := (UndoRemoveFromEnv n) :: !s)
++
++
++let addGlobalToEnv (k: string) (d: envdata) : unit =
++(* ignore (E.log "%a: adding global %s to env\n" d_loc !currentLoc k); *)
++ H.add env k (d, !currentLoc);
++ (* Also add it to the global environment *)
++ H.add genv k (d, !currentLoc)
++
++
++
++(* Create a new name based on a given name. The new name is formed from a
++ * prefix (obtained from the given name as the longest prefix that ends with
++ * a non-digit), followed by a '_' and then by a positive integer suffix. The
++ * first argument is a table mapping name prefixes with the largest suffix
++ * used so far for that prefix. The largest suffix is one when only the
++ * version without suffix has been used. *)
++let alphaTable : (string, location AL.alphaTableData ref) H.t = H.create 307
++ (* vars and enum tags. For composite types we have names like "struct
++ * foo" or "union bar" *)
++
++(* To keep different name scopes different, we add prefixes to names
++ * specifying the kind of name: the kind can be one of "" for variables or
++ * enum tags, "struct" for structures and unions (they share the name space),
++ * "enum" for enumerations, or "type" for types *)
++let kindPlusName (kind: string)
++ (origname: string) : string =
++ if kind = "" then origname else
++ kind ^ " " ^ origname
++
++
++let stripKind (kind: string) (kindplusname: string) : string =
++ let l = 1 + String.length kind in
++ if l > 1 then
++ String.sub kindplusname l (String.length kindplusname - l)
++ else
++ kindplusname
++
++let newAlphaName (globalscope: bool) (* The name should have global scope *)
++ (kind: string)
++ (origname: string) : string * location =
++ let lookupname = kindPlusName kind origname in
++ (* If we are in a scope then it means that we are alpha-converting a local
++ * name. Go and add stuff to reset the state of the alpha table but only to
++ * the top-most scope (that of the enclosing function) *)
++ let rec findEnclosingFun = function
++ [] -> (* At global scope *)()
++ | [s] -> begin
++ let prefix = AL.getAlphaPrefix lookupname in
++ try
++ let countref = H.find alphaTable prefix in
++ s := (UndoResetAlphaCounter (countref, !countref)) :: !s
++ with Not_found ->
++ s := (UndoRemoveFromAlphaTable prefix) :: !s
++ end
++ | _ :: rest -> findEnclosingFun rest
++ in
++ if not globalscope then
++ findEnclosingFun !scopes;
++ let newname, oldloc =
++ AL.newAlphaName alphaTable None lookupname !currentLoc in
++ stripKind kind newname, oldloc
++
++
++
++
++let explodeString (nullterm: bool) (s: string) : char list =
++ let rec allChars i acc =
++ if i < 0 then acc
++ else allChars (i - 1) ((String.get s i) :: acc)
++ in
++ allChars (-1 + String.length s)
++ (if nullterm then [Char.chr 0] else [])
++
++(*** In order to process GNU_BODY expressions we must record that a given
++ *** COMPUTATION is interesting *)
++let gnu_body_result : (A.statement * ((exp * typ) option ref)) ref
++ = ref (A.NOP cabslu, ref None)
++
++(*** When we do statements we need to know the current return type *)
++let currentReturnType : typ ref = ref (TVoid([]))
++let currentFunctionFDEC: fundec ref = ref dummyFunDec
++
++
++let lastStructId = ref 0
++let anonStructName (k: string) (suggested: string) =
++ incr lastStructId;
++ "__anon" ^ k ^ (if suggested <> "" then "_" ^ suggested else "")
++ ^ "_" ^ (string_of_int (!lastStructId))
++
++
++let constrExprId = ref 0
++
++
++let startFile () =
++ H.clear env;
++ H.clear genv;
++ H.clear alphaTable;
++ lastStructId := 0
++
++
++
++let enterScope () =
++ scopes := (ref []) :: !scopes
++
++ (* Exit a scope and clean the environment. We do not yet delete from
++ * the name table *)
++let exitScope () =
++ let this, rest =
++ match !scopes with
++ car :: cdr -> car, cdr
++ | [] -> E.s (error "Not in a scope")
++ in
++ scopes := rest;
++ let rec loop = function
++ [] -> ()
++ | UndoRemoveFromEnv n :: t ->
++ H.remove env n; loop t
++ | UndoRemoveFromAlphaTable n :: t -> H.remove alphaTable n; loop t
++ | UndoResetAlphaCounter (vref, oldv) :: t ->
++ vref := oldv;
++ loop t
++ in
++ loop !this
++
++(* Lookup a variable name. Return also the location of the definition. Might
++ * raise Not_found *)
++let lookupVar (n: string) : varinfo * location =
++ match H.find env n with
++ (EnvVar vi), loc -> vi, loc
++ | _ -> raise Not_found
++
++
++let lookupGlobalVar (n: string) : varinfo * location =
++ match H.find genv n with
++ (EnvVar vi), loc -> vi, loc
++ | _ -> raise Not_found
++
++let docEnv () =
++ let acc : (string * (envdata * location)) list ref = ref [] in
++ let doone () = function
++ EnvVar vi, l ->
++ dprintf "Var(%s,global=%b) (at %a)" vi.vname vi.vglob d_loc l
++ | EnvEnum (tag, typ), l -> dprintf "Enum (at %a)" d_loc l
++ | EnvTyp t, l -> text "typ"
++ | EnvLabel l, _ -> text ("label " ^ l)
++ in
++ H.iter (fun k d -> acc := (k, d) :: !acc) env;
++ docList ~sep:line (fun (k, d) -> dprintf " %s -> %a" k doone d) () !acc
++
++
++
++(* Add a new variable. Do alpha-conversion if necessary *)
++let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo =
++(*
++ ignore (E.log "%t: alphaConvert(addtoenv=%b) %s" d_thisloc addtoenv vi.vname);
++*)
++ (* Announce the name to the alpha conversion table *)
++ let newname, oldloc = newAlphaName (addtoenv && vi.vglob) "" vi.vname in
++ (* Make a copy of the vi if the name has changed. Never change the name for
++ * global variables *)
++ let newvi =
++ if vi.vname = newname then
++ vi
++ else begin
++ if vi.vglob then begin
++ (* Perhaps this is because we have seen a static local which happened
++ * to get the name that we later want to use for a global. *)
++ try
++ let static_local_vi = H.find staticLocals vi.vname in
++ H.remove staticLocals vi.vname;
++ (* Use the new name for the static local *)
++ static_local_vi.vname <- newname;
++ (* And continue using the last one *)
++ vi
++ with Not_found -> begin
++ (* Or perhaps we have seen a typedef which stole our name. This is
++ possible because typedefs use the same name space *)
++ try
++ let typedef_ti = H.find typedefs vi.vname in
++ H.remove typedefs vi.vname;
++ (* Use the new name for the typedef instead *)
++ typedef_ti.tname <- newname;
++ (* And continue using the last name *)
++ vi
++ with Not_found ->
++ E.s (E.error "It seems that we would need to rename global %s (to %s) because of previous occurrence at %a"
++ vi.vname newname d_loc oldloc);
++ end
++ end else begin
++ (* We have changed the name of a local variable. Can we try to detect
++ * if the other variable was also local in the same scope? Not for
++ * now. *)
++ copyVarinfo vi newname
++ end
++ end
++ 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 addtoenv then
++ if vi.vglob then
++ addGlobalToEnv vi.vname (EnvVar newvi)
++ else
++ addLocalToEnv vi.vname (EnvVar newvi));
++(*
++ ignore (E.log " new=%s\n" newvi.vname);
++*)
++(* ignore (E.log "After adding %s alpha table is: %a\n"
++ newvi.vname docAlphaTable alphaTable); *)
++ newvi
++
++
++(* Strip the "const" from the type. It is unfortunate that const variables
++ * can only be set in initialization. Once we decided to move all
++ * declarations to the top of the functions, we have no way of setting a
++ * "const" variable. Furthermore, if the type of the variable is an array or
++ * a struct we must recursively strip the "const" from fields and array
++ * elements. *)
++let rec stripConstLocalType (t: typ) : typ =
++ let dc a =
++ if hasAttribute "const" a then
++ dropAttribute "const" a
++ else a
++ in
++ match t with
++ | TPtr (bt, a) ->
++ (* We want to be able to detect by pointer equality if the type has
++ * changed. So, don't realloc the type unless necessary. *)
++ let a' = dc a in if a != a' then TPtr(bt, a') else t
++ | TInt (ik, a) ->
++ let a' = dc a in if a != a' then TInt(ik, a') else t
++ | TFloat(fk, a) ->
++ let a' = dc a in if a != a' then TFloat(fk, a') else t
++ | TNamed (ti, a) ->
++ (* We must go and drop the consts from the typeinfo as well ! *)
++ let t' = stripConstLocalType ti.ttype in
++ if t != t' then begin
++ (* ignore (warn "Stripping \"const\" from typedef %s\n" ti.tname); *)
++ ti.ttype <- t'
++ end;
++ let a' = dc a in if a != a' then TNamed(ti, a') else t
++
++ | TEnum (ei, a) ->
++ let a' = dc a in if a != a' then TEnum(ei, a') else t
++
++ | TArray(bt, leno, a) ->
++ (* We never assign to the array. So, no need to change the const. But
++ * we must change it on the base type *)
++ let bt' = stripConstLocalType bt in
++ if bt' != bt then TArray(bt', leno, a) else t
++
++ | TComp(ci, a) ->
++ (* Must change both this structure as well as its fields *)
++ List.iter
++ (fun f ->
++ let t' = stripConstLocalType f.ftype in
++ if t' != f.ftype then begin
++ ignore (warnOpt "Stripping \"const\" from field %s of %s\n"
++ f.fname (compFullName ci));
++ f.ftype <- t'
++ end)
++ ci.cfields;
++ let a' = dc a in if a != a' then TComp(ci, a') else t
++
++ (* We never assign functions either *)
++ | TFun(rt, args, va, a) -> t
++ | TVoid a ->
++ let a' = dc a in if a != a' then TVoid a' else t
++ | TBuiltin_va_list a ->
++ let a' = dc a in if a != a' then TBuiltin_va_list a' else t
++
++
++let constFoldTypeVisitor = object (self)
++ inherit nopCilVisitor
++ method vtype t: typ visitAction =
++ match t with
++ TArray(bt, Some len, a) ->
++ let len' = constFold true len in
++ ChangeDoChildrenPost (
++ TArray(bt, Some len', a),
++ (fun x -> x)
++ )
++ | _ -> DoChildren
++end
++
++(* Const-fold any expressions that appear as array lengths in this type *)
++let constFoldType (t:typ) : typ =
++ visitCilType constFoldTypeVisitor t
++
++let typeSigNoAttrs: typ -> typsig = typeSigWithAttrs (fun _ -> [])
++
++(* Create a new temporary variable *)
++let newTempVar (descr:doc) (descrpure:bool) typ =
++ if !currentFunctionFDEC == dummyFunDec then
++ E.s (bug "newTempVar called outside a function");
++(* ignore (E.log "stripConstLocalType(%a) for temporary\n" d_type typ); *)
++ let t' = (!typeForInsertedVar) (stripConstLocalType typ) in
++ (* Start with the name "tmp". The alpha converter will fix it *)
++ let vi = makeVarinfo false "tmp" t' in
++ vi.vdescr <- descr;
++ vi.vdescrpure <- descrpure;
++ alphaConvertVarAndAddToEnv false vi (* Do not add to the environment *)
++(*
++ { vname = "tmp"; (* addNewVar will make the name fresh *)
++ vid = newVarId "tmp" false;
++ vglob = false;
++ vtype = t';
++ vdecl = locUnknown;
++ vinline = false;
++ vattr = [];
++ vaddrof = false;
++ vreferenced = false; (* sm *)
++ vstorage = NoStorage;
++ }
++*)
++
++let mkAddrOfAndMark ((b, off) as lval) : exp =
++ (* Mark the vaddrof flag if b is a variable *)
++ (match b with
++ Var vi -> vi.vaddrof <- true
++ | _ -> ());
++ mkAddrOf lval
++
++(* Call only on arrays *)
++let mkStartOfAndMark ((b, off) as lval) : exp =
++ (* Mark the vaddrof flag if b is a variable *)
++ (match b with
++ Var vi -> vi.vaddrof <- true
++ | _ -> ());
++ let res = StartOf lval in
++ res
++
++
++
++ (* Keep a set of self compinfo for composite types *)
++let compInfoNameEnv : (string, compinfo) H.t = H.create 113
++let enumInfoNameEnv : (string, enuminfo) H.t = H.create 113
++
++
++let lookupTypeNoError (kind: string)
++ (n: string) : typ * location =
++ let kn = kindPlusName kind n in
++ match H.find env kn with
++ EnvTyp t, l -> t, l
++ | _ -> raise Not_found
++
++let lookupType (kind: string)
++ (n: string) : typ * location =
++ try
++ lookupTypeNoError kind n
++ with Not_found ->
++ E.s (error "Cannot find type %s (kind:%s)\n" n kind)
++
++(* Create the self ref cell and add it to the map. Return also an indication
++ * if this is a new one. *)
++let createCompInfo (iss: bool) (n: string) : compinfo * bool =
++ (* Add to the self cell set *)
++ let key = (if iss then "struct " else "union ") ^ n in
++ try
++ H.find compInfoNameEnv key, false (* Only if not already in *)
++ with Not_found -> begin
++ (* Create a compinfo. This will have "cdefined" false. *)
++ let res = mkCompInfo iss n (fun _ -> []) [] in
++ H.add compInfoNameEnv key res;
++ res, true
++ end
++
++(* Create the self ref cell and add it to the map. Return an indication
++ * whether this is a new one. *)
++let createEnumInfo (n: string) : enuminfo * bool =
++ (* Add to the self cell set *)
++ try
++ H.find enumInfoNameEnv n, false (* Only if not already in *)
++ with Not_found -> begin
++ (* Create a enuminfo *)
++ let enum = { ename = n; eitems = [];
++ eattr = []; ereferenced = false; } in
++ H.add enumInfoNameEnv n enum;
++ enum, true
++ end
++
++
++ (* kind is either "struct" or "union" or "enum" and n is a name *)
++let findCompType (kind: string) (n: string) (a: attributes) =
++ let makeForward () =
++ (* This is a forward reference, either because we have not seen this
++ * struct already or because we want to create a version with different
++ * attributes *)
++ if kind = "enum" then
++ let enum, isnew = createEnumInfo n in
++ if isnew then
++ cabsPushGlobal (GEnumTagDecl (enum, !currentLoc));
++ TEnum (enum, a)
++ else
++ let iss = if kind = "struct" then true else false in
++ let self, isnew = createCompInfo iss n in
++ if isnew then
++ cabsPushGlobal (GCompTagDecl (self, !currentLoc));
++ TComp (self, a)
++ in
++ try
++ let old, _ = lookupTypeNoError kind n in (* already defined *)
++ let olda = typeAttrs old in
++ if Util.equals olda a then old else makeForward ()
++ with Not_found -> makeForward ()
++
++
++(* A simple visitor that searchs a statement for labels *)
++class canDropStmtClass pRes = object
++ inherit nopCilVisitor
++
++ method vstmt s =
++ if s.labels != [] then
++ (pRes := false; SkipChildren)
++ else
++ if !pRes then DoChildren else SkipChildren
++
++ method vinst _ = SkipChildren
++ method vexpr _ = SkipChildren
++
++end
++let canDropStatement (s: stmt) : bool =
++ let pRes = ref true in
++ let vis = new canDropStmtClass pRes in
++ ignore (visitCilStmt vis s);
++ !pRes
++
++(**** Occasionally we see structs with no name and no fields *)
++
++
++module BlockChunk =
++ struct
++ type chunk = {
++ stmts: stmt list;
++ postins: instr list; (* Some instructions to append at
++ * the ends of statements (in
++ * reverse order) *)
++ cases: stmt list; (* A list of case statements
++ * (statements with Case labels)
++ * visible at the outer level *)
++ }
++
++ let d_chunk () (c: chunk) =
++ dprintf "@[{ @[%a@] };@?%a@]"
++ (docList ~sep:(chr ';') (d_stmt ())) c.stmts
++ (docList ~sep:(chr ';') (d_instr ())) (List.rev c.postins)
++
++ let empty =
++ { stmts = []; postins = []; cases = []; }
++
++ let isEmpty (c: chunk) =
++ c.postins == [] && c.stmts == []
++
++ let isNotEmpty (c: chunk) = not (isEmpty c)
++
++ let i2c (i: instr) =
++ { empty with postins = [i] }
++
++ (* Occasionally, we'll have to push postins into the statements *)
++ let pushPostIns (c: chunk) : stmt list =
++ if c.postins = [] then c.stmts
++ else
++ let rec toLast = function
++ [{skind=Instr il} as s] as stmts ->
++ s.skind <- Instr (il @ (List.rev c.postins));
++ stmts
++
++ | [] -> [mkStmt (Instr (List.rev c.postins))]
++
++ | a :: rest -> a :: toLast rest
++ in
++ compactStmts (toLast c.stmts)
++
++
++ let c2block (c: chunk) : block =
++ { battrs = [];
++ bstmts = pushPostIns c;
++ }
++
++ (* Add an instruction at the end. Never refer to this instruction again
++ * after you call this *)
++ let (+++) (c: chunk) (i : instr) =
++ {c with postins = i :: c.postins}
++
++ (* Append two chunks. Never refer to the original chunks after you call
++ * this. And especially never share c2 with somebody else *)
++ let (@@) (c1: chunk) (c2: chunk) =
++ { stmts = compactStmts (pushPostIns c1 @ c2.stmts);
++ postins = c2.postins;
++ cases = c1.cases @ c2.cases;
++ }
++
++ let skipChunk = empty
++
++ let returnChunk (e: exp option) (l: location) : chunk =
++ { stmts = [ mkStmt (Return(e, l)) ];
++ postins = [];
++ cases = []
++ }
++
++ let ifChunk (be: exp) (l: location) (t: chunk) (e: chunk) : chunk =
++
++ { stmts = [ mkStmt(If(be, c2block t, c2block e, l))];
++ postins = [];
++ cases = t.cases @ e.cases;
++ }
++
++ (* We can duplicate a chunk if it has a few simple statements, and if
++ * it does not have cases *)
++ let duplicateChunk (c: chunk) = (* raises Failure if you should not
++ * duplicate this chunk *)
++ if not !allowDuplication then
++ raise (Failure "cannot duplicate: disallowed by user");
++ if c.cases != [] then raise (Failure "cannot duplicate: has cases") else
++ let pCount = ref (List.length c.postins) in
++ { stmts =
++ List.map
++ (fun s ->
++ if s.labels != [] then
++ raise (Failure "cannot duplicate: has labels");
++ (match s.skind with
++ If _ | Switch _ | Loop _ | Block _ ->
++ raise (Failure "cannot duplicate: complex stmt")
++ | Instr il ->
++ pCount := !pCount + List.length il
++ | _ -> incr pCount);
++ if !pCount > 5 then raise (Failure ("cannot duplicate: too many instr"));
++ (* We can just copy it because there is nothing to share here.
++ * Except maybe for the ref cell in Goto but it is Ok to share
++ * that, I think *)
++ { s with sid = s.sid}) c.stmts;
++ postins = c.postins; (* There is no shared stuff in instructions *)
++ cases = []
++ }
++(*
++ let duplicateChunk (c: chunk) =
++ if isEmpty c then c else raise (Failure ("cannot duplicate: isNotEmpty"))
++*)
++ (* We can drop a chunk if it does not have labels inside *)
++ let canDrop (c: chunk) =
++ List.for_all canDropStatement c.stmts
++
++ let loopChunk (body: chunk) : chunk =
++ (* Make the statement *)
++ let loop = mkStmt (Loop (c2block body, !currentLoc, None, None)) in
++ { stmts = [ loop (* ; n *) ];
++ postins = [];
++ cases = body.cases;
++ }
++
++ let breakChunk (l: location) : chunk =
++ { stmts = [ mkStmt (Break l) ];
++ postins = [];
++ cases = [];
++ }
++
++ let continueChunk (l: location) : chunk =
++ { stmts = [ mkStmt (Continue l) ];
++ postins = [];
++ cases = []
++ }
++
++ (* Keep track of the gotos *)
++ let backPatchGotos : (string, stmt ref list ref) H.t = H.create 17
++ let addGoto (lname: string) (bref: stmt ref) : unit =
++ let gotos =
++ try
++ H.find backPatchGotos lname
++ with Not_found -> begin
++ let gotos = ref [] in
++ H.add backPatchGotos lname gotos;
++ gotos
++ end
++ in
++ gotos := bref :: !gotos
++
++ (* Keep track of the labels *)
++ let labelStmt : (string, stmt) H.t = H.create 17
++ let initLabels () =
++ H.clear backPatchGotos;
++ H.clear labelStmt
++
++ let resolveGotos () =
++ H.iter
++ (fun lname gotos ->
++ try
++ let dest = H.find labelStmt lname in
++ List.iter (fun gref -> gref := dest) !gotos
++ with Not_found -> begin
++ E.s (error "Label %s not found\n" lname)
++ end)
++ backPatchGotos
++
++ (* Get the first statement in a chunk. Might need to change the
++ * statements in the chunk *)
++ let getFirstInChunk (c: chunk) : stmt * stmt list =
++ (* Get the first statement and add the label to it *)
++ match c.stmts with
++ s :: _ -> s, c.stmts
++ | [] -> (* Add a statement *)
++ let n = mkEmptyStmt () in
++ n, n :: c.stmts
++
++ let consLabel (l: string) (c: chunk) (loc: location)
++ (in_original_program_text : bool) : chunk =
++ (* Get the first statement and add the label to it *)
++ let labstmt, stmts' = getFirstInChunk c in
++ (* Add the label *)
++ labstmt.labels <- Label (l, loc, in_original_program_text) ::
++ labstmt.labels;
++ H.add labelStmt l labstmt;
++ if c.stmts == stmts' then c else {c with stmts = stmts'}
++
++ let s2c (s:stmt) : chunk =
++ { stmts = [ s ];
++ postins = [];
++ cases = [];
++ }
++
++ let gotoChunk (ln: string) (l: location) : chunk =
++ let gref = ref dummyStmt in
++ addGoto ln gref;
++ { stmts = [ mkStmt (Goto (gref, l)) ];
++ postins = [];
++ cases = [];
++ }
++
++ let caseRangeChunk (el: exp list) (l: location) (next: chunk) =
++ let fst, stmts' = getFirstInChunk next in
++ let labels = List.map (fun e -> Case (e, l)) el in
++ fst.labels <- labels @ fst.labels;
++ { next with stmts = stmts'; cases = fst :: next.cases}
++
++ let defaultChunk (l: location) (next: chunk) =
++ let fst, stmts' = getFirstInChunk next in
++ let lb = Default l in
++ fst.labels <- lb :: fst.labels;
++ { next with stmts = stmts'; cases = fst :: next.cases}
++
++
++ let switchChunk (e: exp) (body: chunk) (l: location) =
++ (* Make the statement *)
++ let defaultSeen = ref false in
++ let checkForDefault lb : unit =
++ match lb with
++ Default _ -> if !defaultSeen then
++ E.s (error "Switch statement at %a has duplicate default entries."
++ d_loc l);
++ defaultSeen := true
++ | _ -> ()
++ in
++ let cases = (* eliminate duplicate entries from body.cases.
++ A statement is added to body.cases for each case label
++ it has. *)
++ List.fold_right (fun s acc ->
++ if List.memq s acc then acc
++ else begin
++ List.iter checkForDefault s.labels;
++ s::acc
++ end)
++ body.cases
++ []
++ in
++ let switch = mkStmt (Switch (e, c2block body,
++ cases,
++ l)) in
++ { stmts = [ switch (* ; n *) ];
++ postins = [];
++ cases = [];
++ }
++
++ let mkFunctionBody (c: chunk) : block =
++ resolveGotos (); initLabels ();
++ if c.cases <> [] then
++ E.s (error "Switch cases not inside a switch statement\n");
++ c2block c
++
++ end
++
++open BlockChunk
++
++
++(************ Labels ***********)
++(* Since we turn dowhile and for loops into while we need to take care in
++ * processing the continue statement. For each loop that we enter we place a
++ * marker in a list saying what kinds of loop it is. When we see a continue
++ * for a Non-while loop we must generate a label for the continue *)
++type loopstate =
++ While
++ | NotWhile of string ref
++
++let continues : loopstate list ref = ref []
++
++let startLoop iswhile =
++ continues := (if iswhile then While else NotWhile (ref "")) :: !continues
++
++(* Sometimes we need to create new label names *)
++let newLabelName (base: string) = fst (newAlphaName false "label" base)
++
++let continueOrLabelChunk (l: location) : chunk =
++ match !continues with
++ [] -> E.s (error "continue not in a loop")
++ | While :: _ -> continueChunk l
++ | NotWhile lr :: _ ->
++ if !lr = "" then begin
++ lr := newLabelName "__Cont"
++ end;
++ gotoChunk !lr l
++
++let consLabContinue (c: chunk) =
++ match !continues with
++ [] -> E.s (error "labContinue not in a loop")
++ | While :: rest -> c
++ | NotWhile lr :: rest -> if !lr = "" then c else consLabel !lr c !currentLoc false
++
++let exitLoop () =
++ match !continues with
++ [] -> E.s (error "exit Loop not in a loop")
++ | _ :: rest -> continues := rest
++
++
++(* In GCC we can have locally declared labels. *)
++let genNewLocalLabel (l: string) =
++ (* Call the newLabelName to register the label name in the alpha conversion
++ * table. *)
++ let l' = newLabelName l in
++ (* Add it to the environment *)
++ addLocalToEnv (kindPlusName "label" l) (EnvLabel l');
++ l'
++
++let lookupLabel (l: string) =
++ try
++ match H.find env (kindPlusName "label" l) with
++ EnvLabel l', _ -> l'
++ | _ -> raise Not_found
++ with Not_found ->
++ l
++
++
++(** ALLOCA ***)
++let allocaFun () =
++ if !msvcMode then begin
++ let name = "alloca" in
++ let fdec = emptyFunction name in
++ fdec.svar.vtype <-
++ TFun(voidPtrType, Some [ ("len", !typeOfSizeOf, []) ], false, []);
++ fdec.svar
++ end
++ else
++ (* Use __builtin_alloca where possible, because this can be used
++ even when gcc is invoked with -fno-builtin *)
++ let alloca, _ = lookupGlobalVar "__builtin_alloca" in
++ alloca
++
++(* Maps local variables that are variable sized arrays to the expression that
++ * denotes their length *)
++let varSizeArrays : exp IH.t = IH.create 17
++
++(**** EXP actions ***)
++type expAction =
++ ADrop (* Drop the result. Only the
++ * side-effect is interesting *)
++ | AType (* Only the type of the result
++ is interesting. *)
++ | ASet of lval * typ (* Put the result in a given lval,
++ * provided it matches the type. The
++ * type is the type of the lval.
++ * The location of lval is guaranteed
++ * not to depend on its own value,
++ * e.g. p[p[0]] when p[0] is initially
++ * 0, so the location won't change
++ * after assignment. *)
++ | AExp of typ option (* Return the exp as usual.
++ * Optionally we can specify an
++ * expected type. This is useful for
++ * constants. The expected type is
++ * informational only, we do not
++ * guarantee that the converted
++ * expression has that type.You must
++ * use a doCast afterwards to make
++ * sure. *)
++ | AExpLeaveArrayFun (* Do it like an expression, but do
++ * not convert arrays of functions
++ * into pointers *)
++
++
++(*** Result of compiling conditional expressions *)
++type condExpRes =
++ CEExp of chunk * exp (* Do a chunk and then an expression *)
++ | CEAnd of condExpRes * condExpRes
++ | CEOr of condExpRes * condExpRes
++ | CENot of condExpRes
++
++(******** CASTS *********)
++let integralPromotion (t : typ) : typ = (* c.f. ISO 6.3.1.1 *)
++ match unrollType t with
++ TInt ((IShort|IUShort|IChar|ISChar|IUChar), a) ->
++ if bitsSizeOf t < bitsSizeOf (TInt (IInt, [])) then
++ TInt(IInt, a)
++ else
++ TInt(IUInt, a)
++ | TInt _ -> t
++ | TEnum (_, a) -> TInt(IInt, a)
++ | t -> E.s (error "integralPromotion: not expecting %a" d_type t)
++
++
++let arithmeticConversion (* c.f. ISO 6.3.1.8 *)
++ (t1: typ)
++ (t2: typ) : typ =
++ let checkToInt _ = () in (* dummies for now *)
++ let checkToFloat _ = () in
++ match unrollType t1, unrollType t2 with
++ TFloat(FLongDouble, _), _ -> checkToFloat t2; t1
++ | _, TFloat(FLongDouble, _) -> checkToFloat t1; t2
++ | TFloat(FDouble, _), _ -> checkToFloat t2; t1
++ | _, TFloat (FDouble, _) -> checkToFloat t1; t2
++ | TFloat(FFloat, _), _ -> checkToFloat t2; t1
++ | _, TFloat (FFloat, _) -> checkToFloat t1; t2
++ | _, _ -> begin
++ let t1' = integralPromotion t1 in
++ let t2' = integralPromotion t2 in
++ match unrollType t1', unrollType t2' with
++ TInt(IULongLong, _), _ -> checkToInt t2'; t1'
++ | _, TInt(IULongLong, _) -> checkToInt t1'; t2'
++
++ (* We assume a long long is always larger than a long *)
++ | TInt(ILongLong, _), _ -> checkToInt t2'; t1'
++ | _, TInt(ILongLong, _) -> checkToInt t1'; t2'
++
++ | TInt(IULong, _), _ -> checkToInt t2'; t1'
++ | _, TInt(IULong, _) -> checkToInt t1'; t2'
++
++
++ | TInt(ILong,_), TInt(IUInt,_)
++ when bitsSizeOf t1' <= bitsSizeOf t2' -> TInt(IULong,[])
++ | TInt(IUInt,_), TInt(ILong,_)
++ when bitsSizeOf t2' <= bitsSizeOf t1' -> TInt(IULong,[])
++
++ | TInt(ILong, _), _ -> checkToInt t2'; t1'
++ | _, TInt(ILong, _) -> checkToInt t1'; t2'
++
++ | TInt(IUInt, _), _ -> checkToInt t2'; t1'
++ | _, TInt(IUInt, _) -> checkToInt t1'; t2'
++
++ | TInt(IInt, _), TInt (IInt, _) -> t1'
++
++ | _, _ -> E.s (error "arithmeticConversion")
++ end
++
++
++(* Specify whether the cast is from the source code *)
++let rec castTo ?(fromsource=false)
++ (ot : typ) (nt : typ) (e : exp) : (typ * exp ) =
++ let debugCast = false in
++ if debugCast then
++ ignore (E.log "%t: castTo:%s %a->%a\n"
++ d_thisloc
++ (if fromsource then "(source)" else "")
++ d_type ot d_type nt);
++
++ if not fromsource && Util.equals (typeSig ot) (typeSig nt) then
++ (* Do not put the cast if it is not necessary, unless it is from the
++ * source. *)
++ (ot, e)
++ else begin
++ let nt' = unrollType nt in
++ let nt' = if fromsource then nt' else !typeForInsertedCast nt' in
++ let result = (nt',
++ if !insertImplicitCasts || fromsource then Cil.mkCastT e ot nt' else e) in
++
++ if debugCast then
++ ignore (E.log "castTo: ot=%a nt=%a\n result is %a\n"
++ d_type ot d_type nt'
++ d_plainexp (snd result));
++
++ (* Now see if we can have a cast here *)
++ match unrollType ot, nt' with
++ TNamed _, _
++ | _, TNamed _ -> E.s (bug "unrollType failed in castTo")
++ | TInt(ikindo,_), TInt(ikindn,_) ->
++ (* We used to ignore attributes on integer-integer casts. Not anymore *)
++ (* if ikindo = ikindn then (nt, e) else *)
++ result
++
++ | TPtr (told, _), TPtr(tnew, _) -> result
++
++ | TInt _, TPtr _ -> result
++
++ | TPtr _, TInt _ -> result
++
++ | TArray _, TPtr _ -> result
++
++ | TArray(t1,_,_), TArray(t2,None,_) when Util.equals (typeSig t1) (typeSig t2) -> (nt', e)
++
++ | TPtr _, TArray(_,_,_) -> (nt', e)
++
++ | TEnum _, TInt _ -> result
++ | TFloat _, (TInt _|TEnum _) -> result
++ | (TInt _|TEnum _), TFloat _ -> result
++ | TFloat _, TFloat _ -> result
++ | TInt _, TEnum _ -> result
++ | TEnum _, TEnum _ -> result
++
++ | TEnum _, TPtr _ -> result
++ | TBuiltin_va_list _, (TInt _ | TPtr _) ->
++ result
++
++ | (TInt _ | TPtr _), TBuiltin_va_list _ ->
++ ignore (warnOpt "Casting %a to __builtin_va_list" d_type ot);
++ result
++
++ | TPtr _, TEnum _ ->
++ ignore (warnOpt "Casting a pointer into an enumeration type");
++ result
++
++ (* The expression is evaluated for its side-effects *)
++ | (TInt _ | TEnum _ | TPtr _ ), TVoid _ ->
++ (ot, e)
++
++ (* Even casts between structs are allowed when we are only
++ * modifying some attributes *)
++ | TComp (comp1, a1), TComp (comp2, a2) when comp1.ckey = comp2.ckey ->
++ result
++
++ (** If we try to pass a transparent union value to a function
++ * expecting a transparent union argument, the argument type would
++ * have been changed to the type of the first argument, and we'll
++ * see a cast from a union to the type of the first argument. Turn
++ * that into a field access *)
++ | TComp(tunion, a1), nt -> begin
++ match isTransparentUnion ot with
++ None -> E.s (error "cabs2cil/castTo: illegal cast %a -> %a@!"
++ d_type ot d_type nt')
++ | Some fstfield -> begin
++ (* We do it now only if the expression is an lval *)
++ let e' =
++ match e with
++ Lval lv ->
++ Lval (addOffsetLval (Field(fstfield, NoOffset)) lv)
++ | _ -> E.s (unimp "castTo: transparent union expression is not an lval: %a\n" d_exp e)
++ in
++ (* Continue casting *)
++ castTo ~fromsource:fromsource fstfield.ftype nt' e'
++ end
++ end
++ | _ ->
++ (* strip attributes for a cleaner error message *)
++ let ot'' = setTypeAttrs ot [] in
++ let nt'' = setTypeAttrs nt' [] in
++ E.s (error "cabs2cil/castTo: illegal cast %a -> %a@!"
++ d_type ot'' d_type nt'')
++ end
++
++(* Like Cil.mkCastT, but it calls typeForInsertedCast *)
++let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
++ Cil.mkCastT e oldt (!typeForInsertedCast newt)
++
++let makeCast ~(e: exp) ~(newt: typ) =
++ makeCastT e (typeOf e) newt
++
++(* A cast that is used for conditional expressions. Pointers are Ok *)
++let checkBool (ot : typ) (e : exp) : bool =
++ match unrollType ot with
++ TInt _ -> true
++ | TPtr _ -> true
++ | TEnum _ -> true
++ | TFloat _ -> true
++ | _ -> E.s (error "castToBool %a" d_type ot)
++
++(* Given an expression that is being coerced to bool,
++ is it a nonzero constant? *)
++let rec isConstTrue (e:exp): bool =
++ match e with
++ | Const(CInt64 (n,_,_)) -> n <> Int64.zero
++ | Const(CChr c) -> 0 <> Char.code c
++ | Const(CStr _ | CWStr _) -> true
++ | Const(CReal(f, _, _)) -> f <> 0.0;
++ | CastE(_, e) -> isConstTrue e
++ | _ -> false
++
++(* Given an expression that is being coerced to bool, is it zero?
++ This is a more general version of Cil.isZero, which only handles integers.
++ On constant expressions, either isConstTrue or isConstFalse will hold. *)
++let rec isConstFalse (e:exp): bool =
++ match e with
++ | Const(CInt64 (n,_,_)) -> n = Int64.zero
++ | Const(CChr c) -> 0 = Char.code c
++ | Const(CReal(f, _, _)) -> f = 0.0;
++ | CastE(_, e) -> isConstFalse e
++ | _ -> false
++
++
++
++(* We have our own version of addAttributes that does not allow duplicates *)
++let cabsAddAttributes al0 (al: attributes) : attributes =
++ if al0 == [] then al else
++ List.fold_left
++ (fun acc (Attr(an, _) as a) ->
++ (* See if the attribute is already in there *)
++ match filterAttributes an acc with
++ [] -> addAttribute a acc (* Nothing with that name *)
++ | a' :: _ ->
++ if Util.equals a a' then
++ acc (* Already in *)
++ else begin
++ addAttribute a acc (* Keep both attributes *)
++ end)
++ al
++ al0
++
++
++
++let cabsTypeAddAttributes a0 t =
++ begin
++ match a0 with
++ | [] ->
++ (* no attributes, keep same type *)
++ t
++ | _ ->
++ (* anything else: add a0 to existing attributes *)
++ let add (a: attributes) = cabsAddAttributes a0 a in
++ match t with
++ TVoid a -> TVoid (add a)
++ | TInt (ik, a) ->
++ (* Here we have to watch for the mode attribute *)
++(* sm: This stuff is to handle a GCC extension where you can request integers*)
++(* of specific widths using the "mode" attribute syntax; for example: *)
++(* typedef int int8_t __attribute__ ((__mode__ ( __QI__ ))) ; *)
++(* The cryptic "__QI__" defines int8_t to be 8 bits wide, instead of the *)
++(* 32 bits you'd guess if you didn't know about "mode". The relevant *)
++(* testcase is test/small2/mode_sizes.c, and it was inspired by my *)
++(* /usr/include/sys/types.h. *)
++(* *)
++(* A consequence of this handling is that we throw away the mode *)
++(* attribute, which we used to go out of our way to avoid printing anyway.*)
++(* DG: Use machine model to pick correct type *)
++ let ik', a0' =
++ (* Go over the list of new attributes and come back with a
++ * filtered list and a new integer kind *)
++ List.fold_left
++ (fun (ik', a0') a0one ->
++ match a0one with
++ Attr("mode", [ACons(mode,[])]) -> begin
++ (trace "gccwidth" (dprintf "I see mode %s applied to an int type\n"
++ mode (* #$@!#@ ML! d_type t *) ));
++ (* assuming int is the word size *)
++ try
++ let size = match stripUnderscores mode with
++ "byte" -> 1
++ | "word" -> !Machdep.theMachine.Machdep.sizeof_int
++ | "pointer" -> !Machdep.theMachine.Machdep.sizeof_ptr
++ | "QI" -> 1
++ | "HI" -> 2
++ | "SI" -> 4
++ | "DI" -> 8
++ | "TI" -> 16
++ | "OI" -> 32
++ | _ -> raise Not_found in
++ let nk = intKindForSize size in
++ ((if isSigned ik' then nk else unsignedVersionOf nk), a0')
++ with Not_found ->
++ (ignore (error "GCC width mode %s applied to unexpected type, or unexpected mode"
++ mode));
++ (ik', a0one :: a0')
++ end
++ | _ -> (ik', a0one :: a0'))
++ (ik, [])
++ a0
++ in
++ TInt (ik', cabsAddAttributes a0' a)
++
++ | TFloat (fk, a) -> TFloat (fk, add a)
++ | TEnum (enum, a) -> TEnum (enum, add a)
++ | TPtr (t, a) -> TPtr (t, add a)
++ | TArray (t, l, a) -> TArray (t, l, add a)
++ | TFun (t, args, isva, a) -> TFun(t, args, isva, add a)
++ | TComp (comp, a) -> TComp (comp, add a)
++ | TNamed (t, a) -> TNamed (t, add a)
++ | TBuiltin_va_list a -> TBuiltin_va_list (add a)
++ end
++
++
++(* Do types *)
++ (* Combine the types. Raises the Failure exception with an error message.
++ * isdef says whether the new type is for a definition *)
++type combineWhat =
++ CombineFundef (* The new definition is for a function definition. The old
++ * is for a prototype *)
++ | CombineFunarg (* Comparing a function argument type with an old prototype
++ * arg *)
++ | CombineFunret (* Comparing the return of a function with that from an old
++ * prototype *)
++ | CombineOther
++
++(* We sometimes want to succeed in combining two structure types that are
++ * identical except for the names of the structs. We keep a list of types
++ * that are known to be equal *)
++let isomorphicStructs : (string * string, bool) H.t = H.create 15
++
++let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
++ match oldt, t with
++ | TVoid olda, TVoid a -> TVoid (cabsAddAttributes olda a)
++ | TInt (oldik, olda), TInt (ik, a) ->
++ let combineIK oldk k =
++ if oldk = k then oldk else
++ (* GCC allows a function definition to have a more precise integer
++ * type than a prototype that says "int" *)
++ if not !msvcMode && oldk = IInt && bitsSizeOf t <= 32
++ && (what = CombineFunarg || what = CombineFunret) then
++ k
++ else
++ raise (Failure "different integer types")
++ in
++ TInt (combineIK oldik ik, cabsAddAttributes olda a)
++ | TFloat (oldfk, olda), TFloat (fk, a) ->
++ let combineFK oldk k =
++ if oldk = k then oldk else
++ (* GCC allows a function definition to have a more precise integer
++ * type than a prototype that says "double" *)
++ if not !msvcMode && oldk = FDouble && k = FFloat
++ && (what = CombineFunarg || what = CombineFunret) then
++ k
++ else
++ raise (Failure "different floating point types")
++ in
++ TFloat (combineFK oldfk fk, cabsAddAttributes olda a)
++ | TEnum (_, olda), TEnum (ei, a) ->
++ TEnum (ei, cabsAddAttributes olda a)
++
++ (* Strange one. But seems to be handled by GCC *)
++ | TEnum (oldei, olda) , TInt(IInt, a) -> TEnum(oldei,
++ cabsAddAttributes olda a)
++ (* Strange one. But seems to be handled by GCC *)
++ | TInt(IInt, olda), TEnum (ei, a) -> TEnum(ei, cabsAddAttributes olda a)
++
++
++ | TComp (oldci, olda) , TComp (ci, a) ->
++ if oldci.cstruct <> ci.cstruct then
++ raise (Failure "different struct/union types");
++ let comb_a = cabsAddAttributes olda a in
++ if oldci.cname = ci.cname then
++ TComp (oldci, comb_a)
++ else
++ (* Now maybe they are actually the same *)
++ if H.mem isomorphicStructs (oldci.cname, ci.cname) then
++ (* We know they are the same *)
++ TComp (oldci, comb_a)
++ else begin
++ (* If one has 0 fields (undefined) while the other has some fields
++ * we accept it *)
++ let oldci_nrfields = List.length oldci.cfields in
++ let ci_nrfields = List.length ci.cfields in
++ if oldci_nrfields = 0 then
++ TComp (ci, comb_a)
++ else if ci_nrfields = 0 then
++ TComp (oldci, comb_a)
++ else begin
++ (* Make sure that at least they have the same number of fields *)
++ if oldci_nrfields <> ci_nrfields then begin
++(*
++ ignore (E.log "different number of fields: %s had %d and %s had %d\n"
++ oldci.cname oldci_nrfields
++ ci.cname ci_nrfields);
++*)
++ raise (Failure "different structs(number of fields)");
++ end;
++ (* Assume they are the same *)
++ H.add isomorphicStructs (oldci.cname, ci.cname) true;
++ H.add isomorphicStructs (ci.cname, oldci.cname) true;
++ (* Check that the fields are isomorphic and watch for Failure *)
++ (try
++ List.iter2 (fun oldf f ->
++ if oldf.fbitfield <> f.fbitfield then
++ raise (Failure "different structs(bitfield info)");
++ if oldf.fattr <> f.fattr then
++ raise (Failure "different structs(field attributes)");
++ (* Make sure the types are compatible *)
++ ignore (combineTypes CombineOther oldf.ftype f.ftype);
++ ) oldci.cfields ci.cfields
++ with Failure _ as e -> begin
++ (* Our assumption was wrong. Forget the isomorphism *)
++ ignore (E.log "\tFailed in our assumption that %s and %s are isomorphic\n"
++ oldci.cname ci.cname);
++ H.remove isomorphicStructs (oldci.cname, ci.cname);
++ H.remove isomorphicStructs (ci.cname, oldci.cname);
++ raise e
++ end);
++ (* We get here if we succeeded *)
++ TComp (oldci, comb_a)
++ end
++ end
++
++ | TArray (oldbt, oldsz, olda), TArray (bt, sz, a) ->
++ let newbt = combineTypes CombineOther oldbt bt in
++ let newsz =
++ match oldsz, sz with
++ None, Some _ -> sz
++ | Some _, None -> oldsz
++ | None, None -> sz
++ | Some oldsz', Some sz' ->
++ (* They are not structurally equal. But perhaps they are equal if
++ * we evaluate them. Check first machine independent comparison *)
++ let checkEqualSize (machdep: bool) =
++ let oldsz'', sz''=
++ (* cast both to the same type. This prevents complaints such as
++ "((int)1) <> ((char)1)" *)
++ if machdep then
++ mkCast oldsz' !typeOfSizeOf, mkCast sz' !typeOfSizeOf
++ else
++ oldsz', sz'
++ in
++ Util.equals (constFold machdep oldsz'')
++ (constFold machdep sz'')
++ in
++ if checkEqualSize false then
++ oldsz
++ else if checkEqualSize true then begin
++ ignore (warn "Array type comparison succeeds only based on machine-dependent constant evaluation: %a and %a\n"
++ d_exp oldsz' d_exp sz');
++ oldsz
++ end else
++ raise (Failure "different array lengths")
++
++ in
++ TArray (newbt, newsz, cabsAddAttributes olda a)
++
++ | TPtr (oldbt, olda), TPtr (bt, a) ->
++ TPtr (combineTypes CombineOther oldbt bt, cabsAddAttributes olda a)
++
++ | TFun (_, _, _, [Attr("missingproto",_)]), TFun _ -> t
++
++ | TFun (oldrt, oldargs, oldva, olda), TFun (rt, args, va, a) ->
++ if oldva != va then
++ raise (Failure "diferent vararg specifiers");
++ let defrt = combineTypes
++ (if what = CombineFundef then CombineFunret else CombineOther)
++ oldrt rt in
++ (* If one does not have arguments, believe the one with the
++ * arguments *)
++ let newargs, newrt, olda' =
++ if oldargs = None then args, defrt, olda else
++ if args = None then oldargs, defrt, olda else
++ let oldargslist = argsToList oldargs in
++ let argslist = argsToList args in
++ if List.length oldargslist <> List.length argslist then
++ raise (Failure "different number of arguments")
++ else begin
++ (* Construct a mapping between old and new argument names. *)
++ let map = H.create 5 in
++ List.iter2
++ (fun (on, _, _) (an, _, _) -> H.replace map on an)
++ oldargslist argslist;
++ (* Go over the arguments and update the old ones with the
++ * adjusted types *)
++ Some
++ (List.map2
++ (fun (on, ot, oa) (an, at, aa) ->
++ (* Update the names. Always prefer the new name. This is
++ * very important if the prototype uses different names than
++ * the function definition. *)
++ let n = if an <> "" then an else on in
++ (* Adjust the old type. This hook allows Deputy to do
++ * alpha renaming of dependent attributes. *)
++ let ot' = !typeForCombinedArg map ot in
++ let t =
++ combineTypes
++ (if what = CombineFundef then
++ CombineFunarg else CombineOther)
++ ot' at
++ in
++ let a = addAttributes oa aa in
++ (n, t, a))
++ oldargslist argslist),
++ (let oldrt' = !typeForCombinedArg map oldrt in
++ combineTypes
++ (if what = CombineFundef then CombineFunret else CombineOther)
++ oldrt' rt),
++ !attrsForCombinedArg map olda
++ end
++ in
++ TFun (newrt, newargs, oldva, cabsAddAttributes olda' a)
++
++ | TNamed (oldt, olda), TNamed (t, a) when oldt.tname = t.tname ->
++ TNamed (oldt, cabsAddAttributes olda a)
++
++ | TBuiltin_va_list olda, TBuiltin_va_list a ->
++ TBuiltin_va_list (cabsAddAttributes olda a)
++
++ (* Unroll first the new type *)
++ | _, TNamed (t, a) ->
++ let res = combineTypes what oldt t.ttype in
++ cabsTypeAddAttributes a res
++
++ (* And unroll the old type as well if necessary *)
++ | TNamed (oldt, a), _ ->
++ let res = combineTypes what oldt.ttype t in
++ cabsTypeAddAttributes a res
++
++ | _ -> raise (Failure "different type constructors")
++
++
++let extInlineSuffRe = Str.regexp "\\(.+\\)__extinline"
++
++(* Create and cache varinfo's for globals. Starts with a varinfo but if the
++ * global has been declared already it might come back with another varinfo.
++ * Returns the varinfo to use (might be the old one), and an indication
++ * whether the variable exists already in the environment *)
++let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
++ let debug = false in
++ if not !cacheGlobals then vi, false else
++ try (* See if already defined, in the global environment. We could also
++ * look it up in the whole environment but in that case we might see a
++ * local. This can happen when we declare an extern variable with
++ * global scope but we are in a local scope. *)
++
++ (* We lookup in the environement. If this is extern inline then the name
++ * was already changed to foo__extinline. We lookup with the old name *)
++ let lookupname =
++ if vi.vstorage = Static then
++ if Str.string_match extInlineSuffRe vi.vname 0 then
++ Str.matched_group 1 vi.vname
++ else
++ vi.vname
++ else
++ vi.vname
++ in
++ if debug then
++ ignore (E.log "makeGlobalVarinfo isadef=%b vi.vname=%s (lookup = %s)\n"
++ isadef vi.vname lookupname);
++
++ (* This may throw an exception Not_found *)
++ let oldvi, oldloc = lookupGlobalVar lookupname in
++ if debug then
++ ignore (E.log " %s already in the env at loc %a\n"
++ vi.vname d_loc oldloc);
++ (* It was already defined. We must reuse the varinfo. But clean up the
++ * storage. *)
++ let newstorage = (** See 6.2.2 *)
++ match oldvi.vstorage, vi.vstorage with
++ (* Extern and something else is that thing *)
++ | Extern, other
++ | other, Extern -> other
++
++ | NoStorage, other
++ | other, NoStorage -> other
++
++
++ | _ ->
++ if vi.vstorage != oldvi.vstorage then
++ ignore (warn
++ "Inconsistent storage specification for %s. Previous declaration: %a"
++ vi.vname d_loc oldloc);
++ vi.vstorage
++ in
++ oldvi.vinline <- oldvi.vinline || vi.vinline;
++ oldvi.vstorage <- newstorage;
++ (* If the new declaration has a section attribute, remove any
++ * preexisting section attribute. This mimics behavior of gcc that is
++ * required to compile the Linux kernel properly. *)
++ if hasAttribute "section" vi.vattr then
++ oldvi.vattr <- dropAttribute "section" oldvi.vattr;
++ (* Union the attributes *)
++ oldvi.vattr <- cabsAddAttributes oldvi.vattr vi.vattr;
++ begin
++ try
++ oldvi.vtype <-
++ combineTypes
++ (if isadef then CombineFundef else CombineOther)
++ oldvi.vtype vi.vtype;
++ with Failure reason ->
++ ignore (E.log "old type = %a\n" d_plaintype oldvi.vtype);
++ ignore (E.log "new type = %a\n" d_plaintype vi.vtype);
++ E.s (error "Declaration of %s does not match previous declaration from %a (%s)."
++ vi.vname d_loc oldloc reason)
++ end;
++
++ (* Found an old one. Keep the location always from the definition *)
++ if isadef then begin
++ oldvi.vdecl <- vi.vdecl;
++ end;
++ oldvi, true
++
++ with Not_found -> begin (* A new one. *)
++ if debug then
++ ignore (E.log " %s not in the env already\n" vi.vname);
++ (* Announce the name to the alpha conversion table. This will not
++ * actually change the name of the vi. See the definition of
++ * alphaConvertVarAndAddToEnv *)
++ alphaConvertVarAndAddToEnv true vi, false
++ end
++
++let conditionalConversion (t2: typ) (t3: typ) : typ =
++ let tresult = (* ISO 6.5.15 *)
++ match unrollType t2, unrollType t3 with
++ (TInt _ | TEnum _ | TFloat _),
++ (TInt _ | TEnum _ | TFloat _) ->
++ arithmeticConversion t2 t3
++ | TComp (comp2,_), TComp (comp3,_)
++ when comp2.ckey = comp3.ckey -> t2
++ | TPtr(_, _), TPtr(TVoid _, _) -> t2
++ | TPtr(TVoid _, _), TPtr(_, _) -> t3
++ | TPtr _, TPtr _ when Util.equals (typeSig t2) (typeSig t3) -> t2
++ | TPtr _, TInt _ -> t2 (* most likely comparison with 0 *)
++ | TInt _, TPtr _ -> t3 (* most likely comparison with 0 *)
++
++ (* When we compare two pointers of diffent type, we combine them
++ * using the same algorithm when combining multiple declarations of
++ * a global *)
++ | (TPtr _) as t2', (TPtr _ as t3') -> begin
++ try combineTypes CombineOther t2' t3'
++ with Failure msg -> begin
++ ignore (warn "A.QUESTION: %a does not match %a (%s)"
++ d_type (unrollType t2) d_type (unrollType t3) msg);
++ t2 (* Just pick one *)
++ end
++ end
++ | _, _ -> E.s (error "A.QUESTION for invalid combination of types")
++ in
++ tresult
++
++(* Some utilitites for doing initializers *)
++
++let debugInit = false
++
++type preInit =
++ | NoInitPre
++ | SinglePre of exp
++ | CompoundPre of int ref (* the maximum used index *)
++ * preInit array ref (* an array with initializers *)
++
++(* Instructions on how to handle designators *)
++type handleDesignators =
++ | Handle (* Handle them yourself *)
++ | DoNotHandle (* Do not handle them your self *)
++ | HandleAsNext (* First behave as if you have a NEXT_INIT. Useful for going
++ * into nested designators *)
++ | HandleFirst (* Handle only the first designator *)
++
++(* Set an initializer *)
++let rec setOneInit (this: preInit)
++ (o: offset) (e: exp) : preInit =
++ match o with
++ NoOffset -> SinglePre e
++ | _ ->
++ let idx, (* Index in the current comp *)
++ restoff (* Rest offset *) =
++ match o with
++ | Index(Const(CInt64(i,_,_)), off) -> i64_to_int i, off
++ | Field (f, off) ->
++ (* Find the index of the field *)
++ let rec loop (idx: int) = function
++ [] -> E.s (bug "Cannot find field %s" f.fname)
++ | f' :: _ when f'.fname = f.fname -> idx
++ | _ :: restf -> loop (idx + 1) restf
++ in
++ loop 0 f.fcomp.cfields, off
++ | _ -> E.s (bug "setOneInit: non-constant index")
++ in
++ let pMaxIdx, pArray =
++ match this with
++ NoInitPre -> (* No initializer so far here *)
++ ref idx, ref (Array.create (max 32 (idx + 1)) NoInitPre)
++
++ | CompoundPre (pMaxIdx, pArray) ->
++ if !pMaxIdx < idx then begin
++ pMaxIdx := idx;
++ (* Maybe we also need to grow the array *)
++ let l = Array.length !pArray in
++ if l <= idx then begin
++ let growBy = max (max 32 (idx + 1 - l)) (l / 2) in
++ let newarray = Array.make (growBy + idx) NoInitPre in
++ Array.blit !pArray 0 newarray 0 l;
++ pArray := newarray
++ end
++ end;
++ pMaxIdx, pArray
++ | SinglePre e ->
++ E.s (unimp "Index %d is already initialized" idx)
++ in
++ assert (idx >= 0 && idx < Array.length !pArray);
++ let this' = setOneInit !pArray.(idx) restoff e in
++ !pArray.(idx) <- this';
++ CompoundPre (pMaxIdx, pArray)
++
++
++(* collect a CIL initializer, given the original syntactic initializer
++ * 'preInit'; this returns a type too, since initialization of an array
++ * with unspecified size actually changes the array's type
++ * (ANSI C, 6.7.8, para 22) *)
++let rec collectInitializer
++ (this: preInit)
++ (thistype: typ) : (init * typ) =
++ if this = NoInitPre then (makeZeroInit thistype), thistype
++ else
++ match unrollType thistype, this with
++ | _ , SinglePre e -> SingleInit e, thistype
++ | TArray (bt, leno, at), CompoundPre (pMaxIdx, pArray) ->
++ let (len: int), newtype =
++ (* normal case: use array's declared length, newtype=thistype *)
++ match leno with
++ Some len -> begin
++ match constFold true len with
++ Const(CInt64(ni, _, _)) when ni >= 0L ->
++ (i64_to_int ni), TArray(bt,leno,at)
++
++ | _ -> E.s (error "Array length is not a constant expression %a"
++ d_exp len)
++ end
++ | _ ->
++ (* unsized array case, length comes from initializers *)
++ (!pMaxIdx + 1,
++ TArray (bt, Some (integer (!pMaxIdx + 1)), at))
++ in
++ if !pMaxIdx >= len then
++ E.s (E.bug "collectInitializer: too many initializers(%d >= %d)\n"
++ !pMaxIdx len);
++ (* len could be extremely big. So omit the last initializers, if they
++ * are many (more than 16) *)
++(*
++ ignore (E.log "collectInitializer: len = %d, pMaxIdx= %d\n"
++ len !pMaxIdx); *)
++ let endAt =
++ if len - 1 > !pMaxIdx + 16 then
++ !pMaxIdx
++ else
++ len - 1
++ in
++ (* Make one zero initializer to be used next *)
++ let oneZeroInit = makeZeroInit bt in
++ let rec collect (acc: (offset * init) list) (idx: int) =
++ if idx = -1 then acc
++ else
++ let thisi =
++ if idx > !pMaxIdx then oneZeroInit
++ else (fst (collectInitializer !pArray.(idx) bt))
++ in
++ collect ((Index(integer idx, NoOffset), thisi) :: acc) (idx - 1)
++ in
++
++ CompoundInit (newtype, collect [] endAt), newtype
++
++ | TComp (comp, _), CompoundPre (pMaxIdx, pArray) when comp.cstruct ->
++ let rec collect (idx: int) = function
++ [] -> []
++ | f :: restf ->
++ if f.fname = missingFieldName then
++ collect (idx + 1) restf
++ else
++ let thisi =
++ if idx > !pMaxIdx then
++ makeZeroInit f.ftype
++ else
++ collectFieldInitializer !pArray.(idx) f
++ in
++ (Field(f, NoOffset), thisi) :: collect (idx + 1) restf
++ in
++ CompoundInit (thistype, collect 0 comp.cfields), thistype
++
++ | TComp (comp, _), CompoundPre (pMaxIdx, pArray) when not comp.cstruct ->
++ (* Find the field to initialize *)
++ let rec findField (idx: int) = function
++ [] -> E.s (bug "collectInitializer: union")
++ | _ :: rest when idx < !pMaxIdx && !pArray.(idx) = NoInitPre ->
++ findField (idx + 1) rest
++ | f :: _ when idx = !pMaxIdx ->
++ Field(f, NoOffset),
++ collectFieldInitializer !pArray.(idx) f
++ | _ -> E.s (error "Can initialize only one field for union")
++ in
++ if !msvcMode && !pMaxIdx != 0 then
++ ignore (warn "On MSVC we can initialize only the first field of a union");
++ CompoundInit (thistype, [ findField 0 comp.cfields ]), thistype
++
++ | _ -> E.s (unimp "collectInitializer")
++
++and collectFieldInitializer
++ (this: preInit)
++ (f: fieldinfo) : init =
++ (* collect, and rewrite type *)
++ let init,newtype = (collectInitializer this f.ftype) in
++ f.ftype <- newtype;
++ init
++
++
++type stackElem =
++ InArray of offset * typ * int * int ref (* offset of parent, base type,
++ * length, current index. If the
++ * array length is unspecified we
++ * use Int.max_int *)
++ | InComp of offset * compinfo * fieldinfo list (* offset of parent,
++ base comp, current fields *)
++
++
++(* A subobject is given by its address. The address is read from the end of
++ * the list (the bottom of the stack), starting with the current object *)
++type subobj = { mutable stack: stackElem list; (* With each stack element we
++ * store the offset of its
++ * PARENT *)
++ mutable eof: bool; (* The stack is empty and we reached the
++ * end *)
++ mutable soTyp: typ; (* The type of the subobject. Set using
++ * normalSubobj after setting stack. *)
++ mutable soOff: offset; (* The offset of the subobject. Set
++ * using normalSubobj after setting
++ * stack. *)
++ curTyp: typ; (* Type of current object. See ISO for
++ * the definition of the current object *)
++ curOff: offset; (* The offset of the current obj *)
++ host: varinfo; (* The host that we are initializing.
++ * For error messages *)
++ }
++
++
++(* Make a subobject iterator *)
++let rec makeSubobj
++ (host: varinfo)
++ (curTyp: typ)
++ (curOff: offset) =
++ let so =
++ { host = host; curTyp = curTyp; curOff = curOff;
++ stack = []; eof = false;
++ (* The next are fixed by normalSubobj *)
++ soTyp = voidType; soOff = NoOffset } in
++ normalSubobj so;
++ so
++
++ (* Normalize a stack so the we always point to a valid subobject. Do not
++ * descend into type *)
++and normalSubobj (so: subobj) : unit =
++ match so.stack with
++ [] -> so.soOff <- so.curOff; so.soTyp <- so.curTyp
++ (* The array is over *)
++ | InArray (parOff, bt, leno, current) :: rest ->
++ if leno = !current then begin (* The array is over *)
++ if debugInit then ignore (E.log "Past the end of array\n");
++ so.stack <- rest;
++ advanceSubobj so
++ end else begin
++ so.soTyp <- bt;
++ so.soOff <- addOffset (Index(integer !current, NoOffset)) parOff
++ end
++
++ (* The fields are over *)
++ | InComp (parOff, comp, nextflds) :: rest ->
++ if nextflds == [] then begin (* No more fields here *)
++ if debugInit then ignore (E.log "Past the end of structure\n");
++ so.stack <- rest;
++ advanceSubobj so
++ end else begin
++ let fst = List.hd nextflds in
++ so.soTyp <- fst.ftype;
++ so.soOff <- addOffset (Field(fst, NoOffset)) parOff
++ end
++
++ (* Advance to the next subobject. Always apply to a normalized object *)
++and advanceSubobj (so: subobj) : unit =
++ if so.eof then E.s (bug "advanceSubobj past end");
++ match so.stack with
++ | [] -> if debugInit then ignore (E.log "Setting eof to true\n");
++ so.eof <- true
++ | InArray (parOff, bt, leno, current) :: rest ->
++ if debugInit then ignore (E.log " Advancing to [%d]\n" (!current + 1));
++ (* so.stack <- InArray (parOff, bt, leno, current + 1) :: rest; *)
++ incr current;
++ normalSubobj so
++
++ (* The fields are over *)
++ | InComp (parOff, comp, nextflds) :: rest ->
++ if debugInit then
++ ignore (E.log "Advancing past .%s\n" (List.hd nextflds).fname);
++ let flds' = try List.tl nextflds with _ -> E.s (bug "advanceSubobj") in
++ so.stack <- InComp(parOff, comp, flds') :: rest;
++ normalSubobj so
++
++
++
++(* Find the fields to initialize in a composite. *)
++let fieldsToInit
++ (comp: compinfo)
++ (designator: string option)
++ : fieldinfo list =
++ (* Never look at anonymous fields *)
++ let flds1 =
++ List.filter (fun f -> f.fname <> missingFieldName) comp.cfields in
++ let flds2 =
++ match designator with
++ None -> flds1
++ | Some fn ->
++ let rec loop = function
++ [] -> E.s (error "Cannot find designated field %s" fn)
++ | (f :: _) as nextflds when f.fname = fn -> nextflds
++ | _ :: rest -> loop rest
++ in
++ loop flds1
++ in
++ (* If it is a union we only initialize one field *)
++ match flds2 with
++ [] -> []
++ | (f :: rest) as toinit ->
++ if comp.cstruct then toinit else [f]
++
++
++let integerArrayLength (leno: exp option) : int =
++ match leno with
++ None -> max_int
++ | Some len -> begin
++ try lenOfArray leno
++ with LenOfArray ->
++ E.s (error "Initializing non-constant-length array\n length=%a\n"
++ d_exp len)
++ end
++
++(* sm: I'm sure something like this already exists, but ... *)
++let isNone (o : 'a option) : bool =
++ match o with
++ | None -> true
++ | Some _ -> false
++
++
++let annonCompFieldNameId = ref 0
++let annonCompFieldName = "__annonCompField"
++
++
++
++(* Utility ***)
++let rec replaceLastInList
++ (lst: A.expression list)
++ (how: A.expression -> A.expression) : A.expression list=
++ match lst with
++ [] -> []
++ | [e] -> [how e]
++ | h :: t -> h :: replaceLastInList t how
++
++
++
++
++
++let convBinOp (bop: A.binary_operator) : binop =
++ match bop with
++ A.ADD -> PlusA
++ | A.SUB -> MinusA
++ | A.MUL -> Mult
++ | A.DIV -> Div
++ | A.MOD -> Mod
++ | A.BAND -> BAnd
++ | A.BOR -> BOr
++ | A.XOR -> BXor
++ | A.SHL -> Shiftlt
++ | A.SHR -> Shiftrt
++ | A.EQ -> Eq
++ | A.NE -> Ne
++ | A.LT -> Lt
++ | A.LE -> Le
++ | A.GT -> Gt
++ | A.GE -> Ge
++ | _ -> E.s (error "convBinOp")
++
++(**** PEEP-HOLE optimizations ***)
++let afterConversion (c: chunk) : chunk =
++ (* Now scan the statements and find Instr blocks *)
++
++ (** We want to collapse sequences of the form "tmp = f(); v = tmp". This
++ * will help significantly with the handling of calls to malloc, where it
++ * is important to have the cast at the same place as the call *)
++ let collapseCallCast = function
++ Call(Some(Var vi, NoOffset), f, args, l),
++ Set(destlv, CastE (newt, Lval(Var vi', NoOffset)), _)
++ when (not vi.vglob &&
++ String.length vi.vname >= 3 &&
++ (* Watch out for the possibility that we have an implied cast in
++ * the call *)
++ (let tcallres =
++ match unrollType (typeOf f) with
++ TFun (rt, _, _, _) -> rt
++ | _ -> E.s (E.bug "Function call to a non-function")
++ in
++ Util.equals (typeSig tcallres) (typeSig vi.vtype) &&
++ Util.equals (typeSig newt) (typeSig (typeOfLval destlv))) &&
++ IH.mem callTempVars vi.vid &&
++ vi' == vi)
++ -> Some [Call(Some destlv, f, args, l)]
++ | i1,i2 -> None
++ in
++ (* First add in the postins *)
++ let sl = pushPostIns c in
++ if !doCollapseCallCast then
++ peepHole2 collapseCallCast sl;
++ { c with stmts = sl; postins = [] }
++
++(***** Try to suggest a name for the anonymous structures *)
++let suggestAnonName (nl: A.name list) =
++ match nl with
++ [] -> ""
++ | (n, _, _, _) :: _ -> n
++
++
++(** Optional constant folding of binary operations *)
++let optConstFoldBinOp (machdep: bool) (bop: binop)
++ (e1: exp) (e2:exp) (t: typ) =
++ if !lowerConstants then
++ constFoldBinOp machdep bop e1 e2 t
++ else
++ BinOp(bop, e1, e2, t)
++
++(****** TYPE SPECIFIERS *******)
++let rec doSpecList (suggestedAnonName: string) (* This string will be part of
++ * the names for anonymous
++ * structures and enums *)
++ (specs: A.spec_elem list)
++ (* Returns the base type, the storage, whether it is inline and the
++ * (unprocessed) attributes *)
++ : typ * storage * bool * A.attribute list =
++ (* Do one element and collect the type specifiers *)
++ let isinline = ref false in (* If inline appears *)
++ (* The storage is placed here *)
++ let storage : storage ref = ref NoStorage in
++
++ (* Collect the attributes. Unfortunately, we cannot treat GCC
++ * __attributes__ and ANSI C const/volatile the same way, since they
++ * associate with structures differently. Specifically, ANSI
++ * qualifiers never apply to structures (ISO 6.7.3), whereas GCC
++ * attributes always do (GCC manual 4.30). Therefore, they are
++ * collected and processed separately. *)
++ let attrs : A.attribute list ref = ref [] in (* __attribute__, etc. *)
++ let cvattrs : A.cvspec list ref = ref [] in (* const/volatile *)
++
++ let doSpecElem (se: A.spec_elem)
++ (acc: A.typeSpecifier list)
++ : A.typeSpecifier list =
++ match se with
++ A.SpecTypedef -> acc
++ | A.SpecInline -> isinline := true; acc
++ | A.SpecStorage st ->
++ if !storage <> NoStorage then
++ E.s (error "Multiple storage specifiers");
++ let sto' =
++ match st with
++ A.NO_STORAGE -> NoStorage
++ | A.AUTO -> NoStorage
++ | A.REGISTER -> Register
++ | A.STATIC -> Static
++ | A.EXTERN -> Extern
++ in
++ storage := sto';
++ acc
++
++ | A.SpecCV cv -> cvattrs := cv :: !cvattrs; acc
++ | A.SpecAttr a -> attrs := a :: !attrs; acc
++ | A.SpecType ts -> ts :: acc
++ | A.SpecPattern _ -> E.s (E.bug "SpecPattern in cabs2cil input")
++ in
++ (* Now scan the list and collect the type specifiers. Preserve the order *)
++ let tspecs = List.fold_right doSpecElem specs [] in
++
++ let tspecs' =
++ (* GCC allows a named type that appears first to be followed by things
++ * like "short", "signed", "unsigned" or "long". *)
++ match tspecs with
++ A.Tnamed n :: (_ :: _ as rest) when not !msvcMode ->
++ (* If rest contains "short" or "long" then drop the Tnamed *)
++ if List.exists (function A.Tshort -> true
++ | A.Tlong -> true | _ -> false) rest then
++ rest
++ else
++ tspecs
++
++ | _ -> tspecs
++ in
++ (* Sort the type specifiers *)
++ let sortedspecs =
++ let order = function (* Don't change this *)
++ | A.Tvoid -> 0
++ | A.Tsigned -> 1
++ | A.Tunsigned -> 2
++ | A.Tchar -> 3
++ | A.Tshort -> 4
++ | A.Tlong -> 5
++ | A.Tint -> 6
++ | A.Tint64 -> 7
++ | A.Tfloat -> 8
++ | A.Tdouble -> 9
++ | _ -> 10 (* There should be at most one of the others *)
++ in
++ List.stable_sort (fun ts1 ts2 -> compare (order ts1) (order ts2)) tspecs'
++ in
++ let getTypeAttrs () : A.attribute list =
++ (* Partitions the attributes in !attrs.
++ Type attributes are removed from attrs and returned, so that they
++ can go into the type definition. Name attributes are left in attrs,
++ so they will be returned by doSpecAttr and used in the variable
++ declaration.
++ Testcase: small1/attr9.c *)
++ let an, af, at = cabsPartitionAttributes ~default:AttrType !attrs in
++ attrs := an; (* Save the name attributes for later *)
++ if af <> [] then
++ E.s (error "Invalid position for function type attributes.");
++ at
++ in
++
++ (* And now try to make sense of it. See ISO 6.7.2 *)
++ let bt =
++ match sortedspecs with
++ [A.Tvoid] -> TVoid []
++ | [A.Tchar] -> TInt(IChar, [])
++ | [A.Tsigned; A.Tchar] -> TInt(ISChar, [])
++ | [A.Tunsigned; A.Tchar] -> TInt(IUChar, [])
++
++ | [A.Tshort] -> TInt(IShort, [])
++ | [A.Tsigned; A.Tshort] -> TInt(IShort, [])
++ | [A.Tshort; A.Tint] -> TInt(IShort, [])
++ | [A.Tsigned; A.Tshort; A.Tint] -> TInt(IShort, [])
++
++ | [A.Tunsigned; A.Tshort] -> TInt(IUShort, [])
++ | [A.Tunsigned; A.Tshort; A.Tint] -> TInt(IUShort, [])
++
++ | [] -> TInt(IInt, [])
++ | [A.Tint] -> TInt(IInt, [])
++ | [A.Tsigned] -> TInt(IInt, [])
++ | [A.Tsigned; A.Tint] -> TInt(IInt, [])
++
++ | [A.Tunsigned] -> TInt(IUInt, [])
++ | [A.Tunsigned; A.Tint] -> TInt(IUInt, [])
++
++ | [A.Tlong] -> TInt(ILong, [])
++ | [A.Tsigned; A.Tlong] -> TInt(ILong, [])
++ | [A.Tlong; A.Tint] -> TInt(ILong, [])
++ | [A.Tsigned; A.Tlong; A.Tint] -> TInt(ILong, [])
++
++ | [A.Tunsigned; A.Tlong] -> TInt(IULong, [])
++ | [A.Tunsigned; A.Tlong; A.Tint] -> TInt(IULong, [])
++
++ | [A.Tlong; A.Tlong] -> TInt(ILongLong, [])
++ | [A.Tsigned; A.Tlong; A.Tlong] -> TInt(ILongLong, [])
++ | [A.Tlong; A.Tlong; A.Tint] -> TInt(ILongLong, [])
++ | [A.Tsigned; A.Tlong; A.Tlong; A.Tint] -> TInt(ILongLong, [])
++
++ | [A.Tunsigned; A.Tlong; A.Tlong] -> TInt(IULongLong, [])
++ | [A.Tunsigned; A.Tlong; A.Tlong; A.Tint] -> TInt(IULongLong, [])
++
++ (* int64 is to support MSVC *)
++ | [A.Tint64] -> TInt(ILongLong, [])
++ | [A.Tsigned; A.Tint64] -> TInt(ILongLong, [])
++
++ | [A.Tunsigned; A.Tint64] -> TInt(IULongLong, [])
++
++ | [A.Tfloat] -> TFloat(FFloat, [])
++ | [A.Tdouble] -> TFloat(FDouble, [])
++
++ | [A.Tlong; A.Tdouble] -> TFloat(FLongDouble, [])
++
++ (* Now the other type specifiers *)
++ | [A.Tnamed n] -> begin
++ if n = "__builtin_va_list" &&
++ !Machdep.theMachine.Machdep.__builtin_va_list then begin
++ TBuiltin_va_list []
++ end else
++ let t =
++ match lookupType "type" n with
++ (TNamed _) as x, _ -> x
++ | typ -> E.s (error "Named type %s is not mapped correctly\n" n)
++ in
++ t
++ end
++
++ | [A.Tstruct (n, None, _)] -> (* A reference to a struct *)
++ if n = "" then E.s (error "Missing struct tag on incomplete struct");
++ findCompType "struct" n []
++ | [A.Tstruct (n, Some nglist, extraAttrs)] -> (* A definition of a struct *)
++ let n' =
++ if n <> "" then n else anonStructName "struct" suggestedAnonName in
++ (* Use the (non-cv, non-name) attributes in !attrs now *)
++ let a = extraAttrs @ (getTypeAttrs ()) in
++ makeCompType true n' nglist (doAttributes a)
++
++ | [A.Tunion (n, None, _)] -> (* A reference to a union *)
++ if n = "" then E.s (error "Missing union tag on incomplete union");
++ findCompType "union" n []
++ | [A.Tunion (n, Some nglist, extraAttrs)] -> (* A definition of a union *)
++ let n' =
++ if n <> "" then n else anonStructName "union" suggestedAnonName in
++ (* Use the attributes now *)
++ let a = extraAttrs @ (getTypeAttrs ()) in
++ makeCompType false n' nglist (doAttributes a)
++
++ | [A.Tenum (n, None, _)] -> (* Just a reference to an enum *)
++ if n = "" then E.s (error "Missing enum tag on incomplete enum");
++ findCompType "enum" n []
++
++ | [A.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *)
++ let n' =
++ if n <> "" then n else anonStructName "enum" suggestedAnonName in
++ (* make a new name for this enumeration *)
++ let n'', _ = newAlphaName true "enum" n' in
++
++ (* Create the enuminfo, or use one that was created already for a
++ * forward reference *)
++ let enum, _ = createEnumInfo n'' in
++ let a = extraAttrs @ (getTypeAttrs ()) in
++ enum.eattr <- doAttributes a;
++ let res = TEnum (enum, []) in
++
++ (* sm: start a scope for the enum tag values, since they *
++ * can refer to earlier tags *)
++ enterScope ();
++
++ (* as each name,value pair is determined, this is called *)
++ let rec processName kname (i: exp) loc rest = begin
++ (* add the name to the environment, but with a faked 'typ' field;
++ * we don't know the full type yet (since that includes all of the
++ * tag values), but we won't need them in here *)
++ addLocalToEnv kname (EnvEnum (i, res));
++
++ (* add this tag to the list so that it ends up in the real
++ * environment when we're finished *)
++ let newname, _ = newAlphaName true "" kname in
++
++ (kname, (newname, i, loc)) :: loop (increm i 1) rest
++ end
++
++ and loop i = function
++ [] -> []
++ | (kname, A.NOTHING, cloc) :: rest ->
++ (* use the passed-in 'i' as the value, since none specified *)
++ processName kname i (convLoc cloc) rest
++
++ | (kname, e, cloc) :: rest ->
++ (* constant-eval 'e' to determine tag value *)
++ let e' = getIntConstExp e in
++ let e' =
++ match isInteger (constFold true e') with
++ Some i -> if !lowerConstants then kinteger64 IInt i else e'
++ | _ -> E.s (error "Constant initializer %a not an integer" d_exp e')
++ in
++ processName kname e' (convLoc cloc) rest
++ in
++
++ (* sm: now throw away the environment we built for eval'ing the enum
++ * tags, so we can add to the new one properly *)
++ exitScope ();
++
++ let fields = loop zero eil in
++ (* Now set the right set of items *)
++ enum.eitems <- List.map (fun (_, x) -> x) fields;
++ (* Record the enum name in the environment *)
++ addLocalToEnv (kindPlusName "enum" n'') (EnvTyp res);
++ (* And define the tag *)
++ cabsPushGlobal (GEnumTag (enum, !currentLoc));
++ res
++
++
++ | [A.TtypeofE e] ->
++ let (c, e', t) = doExp false e AType in
++ let t' =
++ match e' with
++ StartOf(lv) -> typeOfLval lv
++ (* If this is a string literal, then we treat it as in sizeof*)
++ | Const (CStr s) -> begin
++ match typeOf e' with
++ TPtr(bt, _) -> (* This is the type of array elements *)
++ TArray(bt, Some (SizeOfStr s), [])
++ | _ -> E.s (bug "The typeOf a string is not a pointer type")
++ end
++ | _ -> t
++ in
++(*
++ ignore (E.log "typeof(%a) = %a\n" d_exp e' d_plaintype t');
++*)
++ !typeForTypeof t'
++
++ | [A.TtypeofT (specs, dt)] ->
++ let typ = doOnlyType specs dt in
++ typ
++
++ | _ ->
++ E.s (error "Invalid combination of type specifiers")
++ in
++ bt,!storage,!isinline,List.rev (!attrs @ (convertCVtoAttr !cvattrs))
++
++(* given some cv attributes, convert them into named attributes for
++ * uniform processing *)
++and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
++ match src with
++ | [] -> []
++ | CV_CONST :: tl -> ("const",[]) :: (convertCVtoAttr tl)
++ | CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
++ | CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
++
++
++and makeVarInfoCabs
++ ~(isformal: bool)
++ ~(isglobal: bool)
++ (ldecl : location)
++ (bt, sto, inline, attrs)
++ (n,ndt,a)
++ : varinfo =
++ let vtype, nattr =
++ doType (AttrName false)
++ ~allowVarSizeArrays:isformal (* For locals we handle var-sized arrays
++ before makeVarInfoCabs; for formals
++ we do it afterwards *)
++ bt (A.PARENTYPE(attrs, ndt, a)) in
++ if inline && not (isFunctionType vtype) then
++ ignore (error "inline for a non-function: %s" n);
++ let t =
++ if not isglobal && not isformal then begin
++ (* Sometimes we call this on the formal argument of a function with no
++ * arguments. Don't call stripConstLocalType in that case *)
++(* ignore (E.log "stripConstLocalType(%a) for %s\n" d_type vtype n); *)
++ stripConstLocalType vtype
++ end else
++ vtype
++ in
++ let vi = makeVarinfo isglobal n t in
++ vi.vstorage <- sto;
++ vi.vattr <- nattr;
++ vi.vdecl <- ldecl;
++
++ if false then
++ ignore (E.log "Created varinfo %s : %a\n" vi.vname d_type vi.vtype);
++
++ vi
++
++(* Process a local variable declaration and allow variable-sized arrays *)
++and makeVarSizeVarInfo (ldecl : location)
++ spec_res
++ (n,ndt,a)
++ : varinfo * chunk * exp * bool =
++ if not !msvcMode then
++ match isVariableSizedArray ndt with
++ None ->
++ makeVarInfoCabs ~isformal:false
++ ~isglobal:false
++ ldecl spec_res (n,ndt,a), empty, zero, false
++ | Some (ndt', se, len) ->
++ makeVarInfoCabs ~isformal:false
++ ~isglobal:false
++ ldecl spec_res (n,ndt',a), se, len, true
++ else
++ makeVarInfoCabs ~isformal:false
++ ~isglobal:false
++ ldecl spec_res (n,ndt,a), empty, zero, false
++
++and doAttr (a: A.attribute) : attribute list =
++ (* Strip the leading and trailing underscore *)
++ let stripUnderscore (n: string) : string =
++ let l = String.length n in
++ let rec start i =
++ if i >= l then
++ E.s (error "Invalid attribute name %s" n);
++ if String.get n i = '_' then start (i + 1) else i
++ in
++ let st = start 0 in
++ let rec finish i =
++ (* We know that we will stop at >= st >= 0 *)
++ if String.get n i = '_' then finish (i - 1) else i
++ in
++ let fin = finish (l - 1) in
++ String.sub n st (fin - st + 1)
++ in
++ match a with
++ | ("__attribute__", []) -> [] (* An empty list of gcc attributes *)
++ | (s, []) -> [Attr (stripUnderscore s, [])]
++ | (s, el) ->
++
++ let rec attrOfExp (strip: bool)
++ ?(foldenum=true)
++ (a: A.expression) : attrparam =
++ match a with
++ A.VARIABLE n -> begin
++ let n' = if strip then stripUnderscore n else n in
++ (** See if this is an enumeration *)
++ try
++ if not foldenum then raise Not_found;
++
++ match H.find env n' with
++ EnvEnum (tag, _), _ -> begin
++ match isInteger (constFold true tag) with
++ Some i64 when !lowerConstants -> AInt (i64_to_int i64)
++ | _ -> ACons(n', [])
++ end
++ | _ -> ACons (n', [])
++ with Not_found -> ACons(n', [])
++ end
++ | A.CONSTANT (A.CONST_STRING s) -> AStr s
++ | A.CONSTANT (A.CONST_INT str) -> begin
++ match parseInt str with
++ Const (CInt64 (v64,_,_)) ->
++ AInt (i64_to_int v64)
++ | _ ->
++ E.s (error "Invalid attribute constant: %s")
++ end
++ | A.CALL(A.VARIABLE n, args) -> begin
++ let n' = if strip then stripUnderscore n else n in
++ let ae' = List.map ae args in
++ ACons(n', ae')
++ end
++ | A.EXPR_SIZEOF e -> ASizeOfE (ae e)
++ | A.TYPE_SIZEOF (bt, dt) -> ASizeOf (doOnlyType bt dt)
++ | A.EXPR_ALIGNOF e -> AAlignOfE (ae e)
++ | A.TYPE_ALIGNOF (bt, dt) -> AAlignOf (doOnlyType bt dt)
++ | A.BINARY(A.AND, aa1, aa2) ->
++ ABinOp(LAnd, ae aa1, ae aa2)
++ | A.BINARY(A.OR, aa1, aa2) ->
++ ABinOp(LOr, ae aa1, ae aa2)
++ | A.BINARY(abop, aa1, aa2) ->
++ ABinOp (convBinOp abop, ae aa1, ae aa2)
++ | A.UNARY(A.PLUS, aa) -> ae aa
++ | A.UNARY(A.MINUS, aa) -> AUnOp (Neg, ae aa)
++ | A.UNARY(A.BNOT, aa) -> AUnOp(BNot, ae aa)
++ | A.UNARY(A.NOT, aa) -> AUnOp(LNot, ae aa)
++ | A.MEMBEROF (e, s) -> ADot (ae e, s)
++ | A.PAREN(e) -> attrOfExp strip ~foldenum:foldenum e
++ | A.UNARY(A.MEMOF, aa) -> AStar (ae aa)
++ | A.UNARY(A.ADDROF, aa) -> AAddrOf (ae aa)
++ | A.MEMBEROFPTR (aa1, s) -> ADot(AStar(ae aa1), s)
++ | A.INDEX(aa1, aa2) -> AIndex(ae aa1, ae aa2)
++ | A.QUESTION(aa1, aa2, aa3) -> AQuestion(ae aa1, ae aa2, ae aa3)
++ | _ ->
++ ignore (E.log "Invalid expression in attribute: ");
++ withCprint Cprint.print_expression a;
++ E.s (error "cabs2cil: invalid expression")
++
++ and ae (e: A.expression) = attrOfExp false e in
++
++ (* Sometimes we need to convert attrarg into attr *)
++ let arg2attr = function
++ | ACons (s, args) -> Attr (s, args)
++ | a ->
++ E.s (error "Invalid form of attribute: %a"
++ d_attrparam a);
++ in
++ if s = "__attribute__" then (* Just a wrapper for many attributes*)
++ List.map (fun e -> arg2attr (attrOfExp true ~foldenum:false e)) el
++ else if s = "__blockattribute__" then (* Another wrapper *)
++ List.map (fun e -> arg2attr (attrOfExp true ~foldenum:false e)) el
++ else if s = "__declspec" then
++ List.map (fun e -> arg2attr (attrOfExp false ~foldenum:false e)) el
++ else
++ [Attr(stripUnderscore s, List.map (attrOfExp ~foldenum:false false) el)]
++
++and doAttributes (al: A.attribute list) : attribute list =
++ List.fold_left (fun acc a -> cabsAddAttributes (doAttr a) acc) [] al
++
++(* A version of Cil.partitionAttributes that works on CABS attributes.
++ It would be better to use Cil.partitionAttributes instead to avoid
++ the extra doAttr conversions here, but that's hard to do in doSpecList.*)
++and cabsPartitionAttributes
++ ~(default:attributeClass)
++ (attrs: A.attribute list) :
++ A.attribute list * A.attribute list * A.attribute list =
++ let rec loop (n,f,t) = function
++ [] -> n, f, t
++ | a :: rest ->
++ let kind = match doAttr a with
++ [] -> default
++ | Attr(an, _)::_ ->
++ (try H.find attributeHash an with Not_found -> default)
++ in
++ match kind with
++ AttrName _ -> loop (a::n, f, t) rest
++ | AttrFunType _ ->
++ loop (n, a::f, t) rest
++ | AttrType -> loop (n, f, a::t) rest
++ in
++ loop ([], [], []) attrs
++
++
++
++and doType (nameortype: attributeClass) (* This is AttrName if we are doing
++ * the type for a name, or AttrType
++ * if we are doing this type in a
++ * typedef *)
++ ?(allowVarSizeArrays=false)
++ (bt: typ) (* The base type *)
++ (dt: A.decl_type)
++ (* Returns the new type and the accumulated name (or type attribute
++ if nameoftype = AttrType) attributes *)
++ : typ * attribute list =
++
++ (* Now do the declarator type. But remember that the structure of the
++ * declarator type is as printed, meaning that it is the reverse of the
++ * right one *)
++ let rec doDeclType (bt: typ) (acc: attribute list) = function
++ A.JUSTBASE -> bt, acc
++ | A.PARENTYPE (a1, d, a2) ->
++ let a1' = doAttributes a1 in
++ let a1n, a1f, a1t = partitionAttributes AttrType a1' in
++ let a2' = doAttributes a2 in
++ let a2n, a2f, a2t = partitionAttributes nameortype a2' in
++(*
++ ignore (E.log "doType: %a @[a1n=%a@!a1f=%a@!a1t=%a@!a2n=%a@!a2f=%a@!a2t=%a@]@!" d_loc !currentLoc d_attrlist a1n d_attrlist a1f d_attrlist a1t d_attrlist a2n d_attrlist a2f d_attrlist a2t);
++*)
++ let bt' = cabsTypeAddAttributes a1t bt in
++(*
++ ignore (E.log "bt' = %a\n" d_type bt');
++*)
++ let bt'', a1fadded =
++ match unrollType bt with
++ TFun _ -> cabsTypeAddAttributes a1f bt', true
++ | _ -> bt', false
++ in
++ (* Now recurse *)
++ let restyp, nattr = doDeclType bt'' acc d in
++ (* Add some more type attributes *)
++ let restyp = cabsTypeAddAttributes a2t restyp in
++ (* See if we can add some more type attributes *)
++ let restyp' =
++ match unrollType restyp with
++ TFun _ ->
++ if a1fadded then
++ cabsTypeAddAttributes a2f restyp
++ else
++ cabsTypeAddAttributes a2f
++ (cabsTypeAddAttributes a1f restyp)
++ | TPtr ((TFun _ as tf), ap) when not !msvcMode ->
++ if a1fadded then
++ TPtr(cabsTypeAddAttributes a2f tf, ap)
++ else
++ TPtr(cabsTypeAddAttributes a2f
++ (cabsTypeAddAttributes a1f tf), ap)
++ | _ ->
++ if a1f <> [] && not a1fadded then
++ E.s (error "Invalid position for (prefix) function type attributes:%a"
++ d_attrlist a1f);
++ if a2f <> [] then
++ E.s (error "Invalid position for (post) function type attributes:%a"
++ d_attrlist a2f);
++ restyp
++ in
++(*
++ ignore (E.log "restyp' = %a\n" d_type restyp');
++*)
++ (* Now add the name attributes and return *)
++ restyp', cabsAddAttributes a1n (cabsAddAttributes a2n nattr)
++
++ | A.PTR (al, d) ->
++ let al' = doAttributes al in
++ let an, af, at = partitionAttributes AttrType al' in
++ (* Now recurse *)
++ let restyp, nattr = doDeclType (TPtr(bt, at)) acc d in
++ (* See if we can do anything with function type attributes *)
++ let restyp' =
++ match unrollType restyp with
++ TFun _ -> cabsTypeAddAttributes af restyp
++ | TPtr((TFun _ as tf), ap) ->
++ TPtr(cabsTypeAddAttributes af tf, ap)
++ | _ ->
++ if af <> [] then
++ E.s (error "Invalid position for function type attributes:%a"
++ d_attrlist af);
++ restyp
++ in
++ (* Now add the name attributes and return *)
++ restyp', cabsAddAttributes an nattr
++
++
++ | A.ARRAY (d, al, len) ->
++ let lo =
++ match len with
++ A.NOTHING -> None
++ | _ ->
++ (* Check that len is a constant expression.
++ We used to also cast the length to int here, but that's
++ theoretically too restrictive on 64-bit machines. *)
++ let len' = doPureExp len in
++ if not (isIntegralType (typeOf len')) then
++ E.s (error "Array length %a does not have an integral type.");
++ if not allowVarSizeArrays then begin
++ (* Assert that len' is a constant *)
++ let elsz =
++ try (bitsSizeOf bt + 7) / 8
++ with _ -> 1 (** We get this if we cannot compute the size of
++ * one element. This can happen, when we define
++ * an extern, for example. We use 1 for now *)
++ in
++ (match constFold true len' with
++ Const(CInt64(i, _, _)) ->
++ if i < 0L then
++ E.s (error "Length of array is negative\n");
++ if Int64.mul i (Int64.of_int elsz) >= 0x80000000L then
++ E.s (error "Length of array is too large\n")
++
++ | l ->
++ if isConstant l then
++ (* e.g., there may be a float constant involved.
++ * We'll leave it to the user to ensure the length is
++ * non-negative, etc.*)
++ ignore(warn "Unable to do constant-folding on array length %a. Some CIL operations on this array may fail."
++ d_exp l)
++ else
++ E.s (error "Length of array is not a constant: %a\n"
++ d_exp l))
++ end;
++ Some len'
++ in
++ let al' = doAttributes al in
++ doDeclType (TArray(bt, lo, al')) acc d
++
++ | A.PROTO (d, args, isva) ->
++ (* Start a scope for the parameter names *)
++ enterScope ();
++ (* Intercept the old-style use of varargs.h. On GCC this means that
++ * we have ellipsis and a last argument "builtin_va_alist:
++ * builtin_va_alist_t". On MSVC we do not have the ellipsis and we
++ * have a last argument "va_alist: va_list" *)
++ let args', isva' =
++ if args != [] && !msvcMode = not isva then begin
++ let newisva = ref isva in
++ let rec doLast = function
++ [([A.SpecType (A.Tnamed atn)], (an, A.JUSTBASE, [], _))]
++ when isOldStyleVarArgTypeName atn &&
++ isOldStyleVarArgName an -> begin
++ (* Turn it into a vararg *)
++ newisva := true;
++ (* And forget about this argument *)
++ []
++ end
++
++ | a :: rest -> a :: doLast rest
++ | [] -> []
++ in
++ let args' = doLast args in
++ (args', !newisva)
++ end else (args, isva)
++ in
++ (* Make the argument as for a formal *)
++ let doOneArg (s, (n, ndt, a, cloc)) : varinfo =
++ let s' = doSpecList n s in
++ let vi = makeVarInfoCabs ~isformal:true ~isglobal:false
++ (convLoc cloc) s' (n,ndt,a) in
++ (* Add the formal to the environment, so it can be referenced by
++ other formals (e.g. in an array type, although that will be
++ changed to a pointer later, or though typeof). *)
++ addLocalToEnv vi.vname (EnvVar vi);
++ vi
++ in
++ let targs : varinfo list option =
++ match List.map doOneArg args' with
++ | [] -> None (* No argument list *)
++ | [t] when isVoidType t.vtype ->
++ Some []
++ | l -> Some l
++ in
++ exitScope ();
++ (* Turn [] types into pointers in the arguments and the result type.
++ * Turn function types into pointers to respective. This simplifies
++ * our life a lot, and is what the standard requires. *)
++ let turnArrayIntoPointer (bt: typ)
++ (lo: exp option) (a: attributes) : typ =
++ let a' : attributes =
++ match lo with
++ None -> a
++ | Some l -> begin
++ (* Transform the length into an attribute expression *)
++ try
++ let la : attrparam = expToAttrParam l in
++ addAttribute (Attr("arraylen", [ la ])) a
++ with NotAnAttrParam _ -> begin
++ ignore (warn "Cannot represent the length of array as an attribute");
++
++ a (* Leave unchanged *)
++ end
++ end
++ in
++ TPtr(bt, a')
++ in
++ let rec fixupArgumentTypes (argidx: int) (args: varinfo list) : unit =
++ match args with
++ [] -> ()
++ | a :: args' ->
++ (match unrollType a.vtype with
++ TArray(bt,lo,attr) ->
++ (* Note that for multi-dimensional arrays we strip off only
++ the first TArray and leave bt alone. *)
++ a.vtype <- turnArrayIntoPointer bt lo attr
++ | TFun _ -> a.vtype <- TPtr(a.vtype, [])
++ | TComp (comp, _) -> begin
++ match isTransparentUnion a.vtype with
++ None -> ()
++ | Some fstfield ->
++ transparentUnionArgs :=
++ (argidx, a.vtype) :: !transparentUnionArgs;
++ a.vtype <- fstfield.ftype;
++ end
++ | _ -> ());
++ fixupArgumentTypes (argidx + 1) args'
++ in
++ let args =
++ match targs with
++ None -> None
++ | Some argl ->
++ fixupArgumentTypes 0 argl;
++ Some (List.map (fun a -> (a.vname, a.vtype, a.vattr)) argl)
++ in
++ let tres =
++ match unrollType bt with
++ TArray(t,lo,attr) -> turnArrayIntoPointer t lo attr
++ | _ -> bt
++ in
++ doDeclType (TFun (tres, args, isva', [])) acc d
++
++ in
++ doDeclType bt [] dt
++
++(* If this is a declarator for a variable size array then turn it into a
++ pointer type and a length *)
++and isVariableSizedArray (dt: A.decl_type)
++ : (A.decl_type * chunk * exp) option =
++ let res = ref None in
++ let rec findArray = function
++ ARRAY (JUSTBASE, al, lo) when lo != A.NOTHING ->
++ (* Try to compile the expression to a constant *)
++ let (se, e', _) = doExp true lo (AExp (Some intType)) in
++ if isNotEmpty se || not (isConstant e') then begin
++ res := Some (se, e');
++ PTR (al, JUSTBASE)
++ end else
++ ARRAY (JUSTBASE, al, lo)
++ | ARRAY (dt, al, lo) -> ARRAY (findArray dt, al, lo)
++ | PTR (al, dt) -> PTR (al, findArray dt)
++ | JUSTBASE -> JUSTBASE
++ | PARENTYPE (prea, dt, posta) -> PARENTYPE (prea, findArray dt, posta)
++ | PROTO (dt, f, a) -> PROTO (findArray dt, f, a)
++ in
++ let dt' = findArray dt in
++ match !res with
++ None -> None
++ | Some (se, e) -> Some (dt', se, e)
++
++and doOnlyType (specs: A.spec_elem list) (dt: A.decl_type) : typ =
++ let bt',sto,inl,attrs = doSpecList "" specs in
++ if sto <> NoStorage || inl then
++ E.s (error "Storage or inline specifier in type only");
++ let tres, nattr = doType AttrType bt' (A.PARENTYPE(attrs, dt, [])) in
++ if nattr <> [] then
++ E.s (error "Name attributes in only_type: %a"
++ d_attrlist nattr);
++ tres
++
++
++and makeCompType (isstruct: bool)
++ (n: string)
++ (nglist: A.field_group list)
++ (a: attribute list) =
++ (* Make a new name for the structure *)
++ let kind = if isstruct then "struct" else "union" in
++ let n', _ = newAlphaName true kind n in
++ (* Create the self cell for use in fields and forward references. Or maybe
++ * one exists already from a forward reference *)
++ let comp, _ = createCompInfo isstruct n' in
++ let doFieldGroup ((s: A.spec_elem list),
++ (nl: (A.name * A.expression option) list)) : 'a list =
++ (* Do the specifiers exactly once *)
++ let sugg = match nl with
++ [] -> ""
++ | ((n, _, _, _), _) :: _ -> n
++ in
++ let bt, sto, inl, attrs = doSpecList sugg s in
++ (* Do the fields *)
++ let makeFieldInfo
++ (((n,ndt,a,cloc) : A.name), (widtho : A.expression option))
++ : fieldinfo =
++ if sto <> NoStorage || inl then
++ E.s (error "Storage or inline not allowed for fields");
++ let ftype, nattr =
++ doType (AttrName false) bt (A.PARENTYPE(attrs, ndt, a)) in
++ (* check for fields whose type is an undefined struct. This rules
++ out circularity:
++ struct C1 { struct C2 c2; }; //This line is now an error.
++ struct C2 { struct C1 c1; int dummy; };
++ *)
++ (match unrollType ftype with
++ TComp (ci',_) when not ci'.cdefined ->
++ E.s (error "Type of field %s is an undefined struct.\n" n)
++ | _ -> ());
++ let width =
++ match widtho with
++ None -> None
++ | Some w -> begin
++ (match unrollType ftype with
++ TInt (ikind, a) -> ()
++ | TEnum _ -> ()
++ | _ -> E.s (error "Base type for bitfield is not an integer type"));
++ match isIntegerConstant w with
++ Some n -> Some n
++ | None -> E.s (error "bitfield width is not an integer constant")
++ end
++ in
++ (* If the field is unnamed and its type is a structure of union type
++ * then give it a distinguished name *)
++ let n' =
++ if n = missingFieldName then begin
++ match unrollType ftype with
++ TComp _ -> begin
++ incr annonCompFieldNameId;
++ annonCompFieldName ^ (string_of_int !annonCompFieldNameId)
++ end
++ | _ -> n
++ end else
++ n
++ in
++ { fcomp = comp;
++ fname = n';
++ ftype = ftype;
++ fbitfield = width;
++ fattr = nattr;
++ floc = convLoc cloc
++ }
++ in
++ List.map makeFieldInfo nl
++ in
++
++
++ let flds = List.concat (List.map doFieldGroup nglist) in
++ if comp.cfields <> [] then begin
++ (* This appears to be a multiply defined structure. This can happen from
++ * a construct like "typedef struct foo { ... } A, B;". This is dangerous
++ * because at the time B is processed some forward references in { ... }
++ * appear as backward references, which coild lead to circularity in
++ * the type structure. We do a thourough check and then we reuse the type
++ * for A *)
++ let fieldsSig fs = List.map (fun f -> typeSig f.ftype) fs in
++ if not (Util.equals (fieldsSig comp.cfields) (fieldsSig flds)) then
++ ignore (error "%s seems to be multiply defined" (compFullName comp))
++ end else
++ comp.cfields <- flds;
++
++(* ignore (E.log "makeComp: %s: %a\n" comp.cname d_attrlist a); *)
++ comp.cattr <- a;
++ let res = TComp (comp, []) in
++ (* This compinfo is defined, even if there are no fields *)
++ comp.cdefined <- true;
++ (* Create a typedef for this one *)
++ cabsPushGlobal (GCompTag (comp, !currentLoc));
++
++ (* There must be a self cell created for this already *)
++ addLocalToEnv (kindPlusName kind n) (EnvTyp res);
++ (* Now create a typedef with just this type *)
++ res
++
++and preprocessCast (specs: A.specifier)
++ (dt: A.decl_type)
++ (ie: A.init_expression)
++ : A.specifier * A.decl_type * A.init_expression =
++ let typ = doOnlyType specs dt in
++ (* If we are casting to a union type then we have to treat this as a
++ * constructor expression. This is to handle the gcc extension that allows
++ * cast from a type of a field to the type of the union *)
++ let ie' =
++ match unrollType typ, ie with
++ TComp (c, _), A.SINGLE_INIT _ when not c.cstruct ->
++ A.COMPOUND_INIT [(A.INFIELD_INIT ("___matching_field",
++ A.NEXT_INIT),
++ ie)]
++ | _, _ -> ie
++ in
++ (* Maybe specs contains an unnamed composite. Replace with the name so that
++ * when we do again the specs we get the right name *)
++ let specs1 =
++ match typ with
++ TComp (ci, _) ->
++ List.map
++ (function
++ A.SpecType (A.Tstruct ("", flds, [])) ->
++ A.SpecType (A.Tstruct (ci.cname, None, []))
++ | A.SpecType (A.Tunion ("", flds, [])) ->
++ A.SpecType (A.Tunion (ci.cname, None, []))
++ | s -> s) specs
++ | _ -> specs
++ in
++ specs1, dt, ie'
++
++and getIntConstExp (aexp) : exp =
++ let c, e, _ = doExp true aexp (AExp None) in
++ if not (isEmpty c) then
++ E.s (error "Constant expression %a has effects" d_exp e);
++ match e with
++ (* first, filter for those Const exps that are integers *)
++ | Const (CInt64 _ ) -> e
++ | Const (CEnum _) -> e
++ | Const (CChr i) -> Const(charConstToInt i)
++
++ (* other Const expressions are not ok *)
++ | Const _ -> E.s (error "Expected integer constant and got %a" d_exp e)
++
++ (* now, anything else that 'doExp true' returned is ok (provided
++ that it didn't yield side effects); this includes, in particular,
++ the various sizeof and alignof expression kinds *)
++ | _ -> e
++
++and isIntegerConstant (aexp) : int option =
++ match doExp true aexp (AExp None) with
++ (c, e, _) when isEmpty c -> begin
++ match isInteger (constFold true e) with
++ Some i64 -> Some (i64_to_int i64)
++ | _ -> None
++ end
++ | _ -> None
++
++ (* Process an expression and in the process do some type checking,
++ * extract the effects as separate statements *)
++and doExp (asconst: bool) (* This expression is used as a constant *)
++ (e: A.expression)
++ (what: expAction) : (chunk * exp * typ) =
++ (* A subexpression of array type is automatically turned into StartOf(e).
++ * Similarly an expression of function type is turned into AddrOf. So
++ * essentially doExp should never return things of type TFun or TArray *)
++ let processArrayFun e t =
++ match e, unrollType t with
++ (Lval(lv) | CastE(_, Lval lv)), TArray(tbase, _, a) ->
++ mkStartOfAndMark lv, TPtr(tbase, a)
++ | (Lval(lv) | CastE(_, Lval lv)), TFun _ ->
++ mkAddrOfAndMark lv, TPtr(t, [])
++ | _, (TArray _ | TFun _) ->
++ E.s (error "Array or function expression is not lval: %a@!"
++ d_plainexp e)
++ | _ -> e, t
++ in
++ (* Before we return we call finishExp *)
++ let finishExp ?(newWhat=what)
++ (se: chunk) (e: exp) (t: typ) : chunk * exp * typ =
++ match newWhat with
++ ADrop
++ | AType -> (se, e, t)
++ | AExpLeaveArrayFun ->
++ (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 _ ->
++ let (e', t') = processArrayFun e t in
++(*
++ ignore (E.log "finishExp: e'=%a, t'=%a\n"
++ d_exp e' d_type t');
++*)
++ (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)
++ | _ ->
++ 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)), e'', t'')
++ end
++ in
++ let rec findField (n: string) (fidlist: fieldinfo list) : offset =
++ (* Depth first search for the field. This appears to be what GCC does.
++ * MSVC checks that there are no ambiguous field names, so it does not
++ * matter how we search *)
++ let rec search = function
++ [] -> NoOffset (* Did not find *)
++ | fid :: rest when fid.fname = n -> Field(fid, NoOffset)
++ | fid :: rest when prefix annonCompFieldName fid.fname -> begin
++ match unrollType fid.ftype with
++ TComp (ci, _) ->
++ let off = search ci.cfields in
++ if off = NoOffset then
++ search rest (* Continue searching *)
++ else
++ Field (fid, off)
++ | _ -> E.s (bug "unnamed field type is not a struct/union")
++ end
++ | _ :: rest -> search rest
++ in
++ let off = search fidlist in
++ if off = NoOffset then
++ E.s (error "Cannot find field %s" n);
++ off
++ in
++ try
++ match e with
++ | A.PAREN e -> E.s (bug "stripParen")
++ | A.NOTHING when what = ADrop -> finishExp empty (integer 0) intType
++ | A.NOTHING ->
++ let res = Const(CStr "exp_nothing") in
++ finishExp empty res (typeOf res)
++
++ (* Do the potential lvalues first *)
++ | A.VARIABLE n -> begin
++ (* Look up in the environment *)
++ try
++ let envdata = H.find env n in
++ match envdata with
++ EnvVar vi, _ ->
++ (* if isconst &&
++ not (isFunctionType vi.vtype) &&
++ not (isArrayType vi.vtype)then
++ E.s (error "variable appears in constant"); *)
++ finishExp empty (Lval(var vi)) vi.vtype
++ | EnvEnum (tag, typ), _ ->
++ if !Cil.lowerConstants then
++ finishExp empty tag typ
++ else begin
++ let ei =
++ match unrollType typ with
++ TEnum(ei, _) -> ei
++ | _ -> assert false
++ in
++ finishExp empty (Const (CEnum(tag, n, ei))) typ
++ end
++
++ | _ -> raise Not_found
++ with Not_found -> begin
++ if isOldStyleVarArgName n then
++ E.s (error "Cannot resolve variable %s. This could be a CIL bug due to the handling of old-style variable argument functions.\n" n)
++ else
++ E.s (error "Cannot resolve variable %s.\n" n)
++ end
++ end
++ | A.INDEX (e1, e2) -> begin
++ (* Recall that doExp turns arrays into StartOf pointers *)
++ let (se1, e1', t1) = doExp false e1 (AExp None) in
++ let (se2, e2', t2) = doExp false e2 (AExp None) in
++ let se = se1 @@ se2 in
++ let (e1'', t1, e2'', tresult) =
++ (* Either e1 or e2 can be the pointer *)
++ match unrollType t1, unrollType t2 with
++ TPtr(t1e,_), (TInt _|TEnum _) -> e1', t1, e2', t1e
++ | (TInt _|TEnum _), TPtr(t2e,_) -> e2', t2, e1', t2e
++ | _ ->
++ E.s (error
++ "Expecting a pointer type in index:@! t1=%a@!t2=%a@!"
++ d_plaintype t1 d_plaintype t2)
++ in
++ (* We have to distinguish the construction based on the type of e1'' *)
++ let res =
++ match e1'' with
++ StartOf array -> (* A real array indexing operation *)
++ addOffsetLval (Index(e2'', NoOffset)) array
++ | _ -> (* Turn into *(e1 + e2) *)
++ mkMem (BinOp(IndexPI, e1'', e2'', t1)) NoOffset
++ in
++ (* Do some optimization of StartOf *)
++ finishExp se (Lval res) tresult
++
++ end
++ | A.UNARY (A.MEMOF, e) ->
++ if asconst then
++ ignore (warn "MEMOF in constant");
++ let (se, e', t) = doExp false e (AExp None) in
++ let tresult =
++ match unrollType t with
++ | TPtr(te, _) -> te
++ | _ -> E.s (error "Expecting a pointer type in *. Got %a@!"
++ d_plaintype t)
++ in
++ finishExp se
++ (Lval (mkMem e' NoOffset))
++ tresult
++
++ (* e.str = (& e + off(str)). If e = (be + beoff) then e.str = (be
++ * + beoff + off(str)) *)
++ | A.MEMBEROF (e, str) ->
++ (* member of is actually allowed if we only take the address *)
++ (* if isconst then
++ E.s (error "MEMBEROF in constant"); *)
++ let (se, e', t') = doExp false e (AExp None) in
++ let lv =
++ match e' with
++ Lval x -> x
++ | CastE(_, Lval x) -> x
++ | _ -> E.s (error "Expected an lval in MEMBEROF (field %s)" str)
++ in
++ let field_offset =
++ match unrollType t' with
++ TComp (comp, _) -> findField str comp.cfields
++ | _ -> E.s (error "expecting a struct with field %s" str)
++ in
++ let lv' = Lval(addOffsetLval field_offset lv) in
++ let field_type = typeOf lv' in
++ finishExp se lv' field_type
++
++ (* e->str = * (e + off(str)) *)
++ | A.MEMBEROFPTR (e, str) ->
++ if asconst then
++ ignore (warn "MEMBEROFPTR in constant");
++ let (se, e', t') = doExp false e (AExp None) in
++ let pointedt =
++ match unrollType t' with
++ TPtr(t1, _) -> t1
++ | TArray(t1,_,_) -> t1
++ | _ -> E.s (error "expecting a pointer to a struct")
++ in
++ let field_offset =
++ match unrollType pointedt with
++ TComp (comp, _) -> findField str comp.cfields
++ | x ->
++ E.s (error
++ "expecting a struct with field %s. Found %a. t1 is %a"
++ str d_type x d_type t')
++ in
++ let lv' = Lval (mkMem e' field_offset) in
++ let field_type = typeOf lv' in
++ finishExp se lv' field_type
++
++ | A.CONSTANT ct -> begin
++ let hasSuffix str =
++ let l = String.length str in
++ fun s ->
++ let ls = String.length s in
++ l >= ls && s = String.uppercase (String.sub str (l - ls) ls)
++ in
++ match ct with
++ A.CONST_INT str -> begin
++ let res = parseInt str in
++ finishExp empty res (typeOf res)
++ end
++
++(*
++ | A.CONST_WSTRING wstr ->
++ let len = List.length wstr in
++ let wchar_t = !wcharType in
++ (* We will make an array big enough to contain the wide
++ * characters and the wide-null terminator *)
++ let ws_t = TArray(wchar_t, Some (integer len), []) in
++ let ws =
++ makeGlobalVar ("wide_string" ^ string_of_int !lastStructId)
++ ws_t
++ in
++ ws.vstorage <- Static;
++ incr lastStructId;
++ (* Make the initializer. Idx is a wide_char index. *)
++ let rec loop (idx: int) (s: int64 list) =
++ match s with
++ [] -> []
++ | wc::rest ->
++ let wc_cilexp = Const (CInt64(wc, IInt, None)) in
++ (Index(integer idx, NoOffset),
++ SingleInit (makeCast wc_cilexp wchar_t))
++ :: loop (idx + 1) rest
++ in
++ (* Add the definition for the array *)
++ cabsPushGlobal (GVar(ws,
++ {init = Some (CompoundInit(ws_t,
++ loop 0 wstr))},
++ !currentLoc));
++ finishExp empty (StartOf(Var ws, NoOffset))
++ (TPtr(wchar_t, []))
++ *)
++
++ | A.CONST_WSTRING (ws: int64 list) ->
++ let res = Const(CWStr ((* intlist_to_wstring *) ws)) in
++ finishExp empty res (typeOf res)
++
++ | A.CONST_STRING s ->
++ (* Maybe we burried __FUNCTION__ in there *)
++ let s' =
++ try
++ let start = String.index s (Char.chr 0) in
++ let l = String.length s in
++ let tofind = (String.make 1 (Char.chr 0)) ^ "__FUNCTION__" in
++ let past = start + String.length tofind in
++ if past <= l &&
++ String.sub s start (String.length tofind) = tofind then
++ (if start > 0 then String.sub s 0 start else "") ^
++ !currentFunctionFDEC.svar.vname ^
++ (if past < l then String.sub s past (l - past) else "")
++ else
++ s
++ with Not_found -> s
++ in
++ let res = Const(CStr s') in
++ finishExp empty res (typeOf res)
++
++ | A.CONST_CHAR char_list ->
++ let a, b = (interpret_character_constant char_list) in
++ finishExp empty (Const a) b
++
++ | A.CONST_WCHAR char_list ->
++ (* matth: I can't see a reason for a list of more than one char
++ * here, since the kinteger64 below will take only the lower 16
++ * bits of value. ('abc' makes sense, because CHAR constants have
++ * type int, and so more than one char may be needed to represent
++ * the value. But L'abc' has type wchar, and so is equivalent to
++ * L'c'). But gcc allows L'abc', so I'll leave this here in case
++ * I'm missing some architecture dependent behavior. *)
++ let value = reduce_multichar !wcharType char_list in
++ let result = kinteger64 !wcharKind value in
++ finishExp empty result (typeOf result)
++
++ | A.CONST_FLOAT str -> begin
++ (* Maybe it ends in U or UL. Strip those *)
++ let l = String.length str in
++ let hasSuffix = hasSuffix str in
++ let baseint, kind =
++ if hasSuffix "L" then
++ String.sub str 0 (l - 1), FLongDouble
++ else if hasSuffix "F" then
++ String.sub str 0 (l - 1), FFloat
++ else if hasSuffix "D" then
++ String.sub str 0 (l - 1), FDouble
++ else
++ str, FDouble
++ in
++ if kind = FLongDouble then
++ (* We only have 64-bit values in Ocaml *)
++ E.log "treating long double constant %s as double constant at %a.\n"
++ str d_loc !currentLoc;
++ try
++ finishExp empty
++ (Const(CReal(float_of_string baseint, kind,
++ Some str)))
++ (TFloat(kind,[]))
++ with e -> begin
++ ignore (E.log "float_of_string %s (%s)\n" str
++ (Printexc.to_string e));
++ E.hadErrors := true;
++ let res = Const(CStr "booo CONS_FLOAT") in
++ finishExp empty res (typeOf res)
++ end
++ end
++ end
++
++ | A.TYPE_SIZEOF (bt, dt) ->
++ let typ = doOnlyType bt dt in
++ finishExp empty (SizeOf(typ)) !typeOfSizeOf
++
++ (* Intercept the sizeof("string") *)
++ | A.EXPR_SIZEOF (A.CONSTANT (A.CONST_STRING s)) -> begin
++ (* Process the string first *)
++ match doExp asconst (A.CONSTANT (A.CONST_STRING s)) (AExp None) with
++ _, Const(CStr s), _ ->
++ finishExp empty (SizeOfStr s) !typeOfSizeOf
++ | _ -> E.s (bug "cabs2cil: sizeOfStr")
++ end
++
++ | A.EXPR_SIZEOF e ->
++ (* Allow non-constants in sizeof *)
++ (* Do not convert arrays and functions into pointers. *)
++ let (se, e', t) = doExp false e AExpLeaveArrayFun in
++(*
++ ignore (E.log "sizeof: %a e'=%a, t=%a\n"
++ d_loc !currentLoc d_plainexp e' d_type t);
++*)
++ (* !!!! The book says that the expression is not evaluated, so we
++ * drop the potential side-effects
++ if isNotEmpty se then
++ ignore (warn "Warning: Dropping side-effect in EXPR_SIZEOF\n");
++*)
++ let size =
++ match e' with (* If we are taking the sizeof an
++ * array we must drop the StartOf *)
++ StartOf(lv) -> SizeOfE (Lval(lv))
++
++ (* Maybe we are taking the sizeof for a CStr. In that case we
++ * mean the pointer to the start of the string *)
++ | Const(CStr _) -> SizeOf (charPtrType)
++
++ (* Maybe we are taking the sizeof a variable-sized array *)
++ | Lval (Var vi, NoOffset) -> begin
++ try
++ IH.find varSizeArrays vi.vid
++ with Not_found -> SizeOfE e'
++ end
++ | _ -> SizeOfE e'
++ in
++ finishExp empty size !typeOfSizeOf
++
++ | A.TYPE_ALIGNOF (bt, dt) ->
++ let typ = doOnlyType bt dt in
++ finishExp empty (AlignOf(typ)) !typeOfSizeOf
++
++ | A.EXPR_ALIGNOF e ->
++ let (se, e', t) = doExp false e AExpLeaveArrayFun in
++ (* !!!! The book says that the expression is not evaluated, so we
++ * drop the potential side-effects
++ if isNotEmpty se then
++ ignore (warn "Warning: Dropping side-effect in EXPR_ALIGNOF\n");
++*)
++ let e'' =
++ match e' with (* If we are taking the alignof an
++ * array we must drop the StartOf *)
++ StartOf(lv) -> Lval(lv)
++
++ | _ -> e'
++ in
++ finishExp empty (AlignOfE(e'')) !typeOfSizeOf
++
++ | A.CAST ((specs, dt), ie) ->
++ let s', dt', ie' = preprocessCast specs dt ie in
++ (* We know now that we can do s' and dt' many times *)
++ let typ = doOnlyType s' dt' in
++ let what' =
++ match what with
++ AExp (Some _) -> AExp (Some typ)
++ | AExp None -> what
++ | ADrop | AType | AExpLeaveArrayFun -> what
++ | ASet (lv, lvt) ->
++ (* If the cast from typ to lvt would be dropped, then we
++ * continue with a Set *)
++ if false && Util.equals (typeSig typ) (typeSig lvt) then
++ what
++ else
++ AExp None (* We'll create a temporary *)
++ in
++ (* Remember here if we have done the Set *)
++ let (se, e', t'), (needcast: bool) =
++ match ie' with
++ A.SINGLE_INIT e -> doExp asconst e what', true
++
++ | A.NO_INIT -> E.s (error "missing expression in cast")
++
++ | A.COMPOUND_INIT _ -> begin
++ (* Pretend that we are declaring and initializing a brand new
++ * variable *)
++ let newvar = "__constr_expr_" ^ string_of_int (!constrExprId) in
++ incr constrExprId;
++ let spec_res = doSpecList "" s' in
++ let se1 =
++ if !scopes == [] then begin
++ (* This is a global. Mark the new vars as static *)
++ let spec_res' =
++ let t, sto, inl, attrs = spec_res in
++ t, Static, inl, attrs
++ in
++ ignore (createGlobal spec_res'
++ ((newvar, dt', [], cabslu), ie'));
++ empty
++ end else
++ createLocal spec_res ((newvar, dt', [], cabslu), ie')
++ in
++ (* Now pretend that e is just a reference to the newly created
++ * variable *)
++ let se, e', t' = doExp asconst (A.VARIABLE newvar) what' in
++ (* If typ is an array then the doExp above has already added a
++ * StartOf. We must undo that now so that it is done once by
++ * the finishExp at the end of this case *)
++ let e2, t2 =
++ match unrollType typ, e' with
++ TArray _, StartOf lv -> Lval lv, typ
++ | _, _ -> e', t'
++ in
++ (* If we are here, then the type t2 is guaranteed to match the
++ * type of the expression e2, so we do not need a cast. We have
++ * to worry about this because otherwise, we might need to cast
++ * between arrays or structures. *)
++ (se1 @@ se, e2, t2), false
++ end
++ in
++ let (t'', e'') =
++ match typ with
++ TVoid _ when what' = ADrop -> (t', e') (* strange GNU thing *)
++ | _ ->
++ (* Do this to check the cast, unless we are sure that we do not
++ * need the check. *)
++ let newtyp, newexp =
++ if needcast then
++ castTo ~fromsource:true t' typ e'
++ else
++ t', e'
++ in
++ newtyp, newexp
++ in
++ finishExp se e'' t''
++
++ | A.UNARY(A.MINUS, e) ->
++ let (se, e', t) = doExp asconst e (AExp None) in
++ if isIntegralType t then
++ let tres = integralPromotion t in
++ let e'' =
++ match e' with
++ | Const(CInt64(i, ik, _)) -> kinteger64 ik (Int64.neg i)
++ | _ -> UnOp(Neg, makeCastT e' t tres, tres)
++ in
++ finishExp se e'' tres
++ else
++ if isArithmeticType t then
++ finishExp se (UnOp(Neg,e',t)) t
++ else
++ E.s (error "Unary - on a non-arithmetic type")
++
++ | A.UNARY(A.BNOT, e) ->
++ let (se, e', t) = doExp asconst e (AExp None) in
++ if isIntegralType t then
++ let tres = integralPromotion t in
++ let e'' = UnOp(BNot, makeCastT e' t tres, tres) in
++ finishExp se e'' tres
++ else
++ E.s (error "Unary ~ on a non-integral type")
++
++ | A.UNARY(A.PLUS, e) -> doExp asconst e what
++
++
++ | A.UNARY(A.ADDROF, e) -> begin
++ match e with
++ A.COMMA el -> (* GCC extension *)
++ doExp false
++ (A.COMMA (replaceLastInList el (fun e -> A.UNARY(A.ADDROF, e))))
++ what
++ | A.QUESTION (e1, e2, e3) -> (* GCC extension *)
++ doExp false
++ (A.QUESTION (e1, A.UNARY(A.ADDROF, e2), A.UNARY(A.ADDROF, e3)))
++ what
++ | A.PAREN e1 ->
++ doExp false (A.UNARY(A.ADDROF, e1)) what
++ | A.VARIABLE s when
++ isOldStyleVarArgName s
++ && (match !currentFunctionFDEC.svar.vtype with
++ TFun(_, _, true, _) -> true | _ -> false) ->
++ (* We are in an old-style variable argument function and we are
++ * taking the address of the argument that was removed while
++ * processing the function type. We compute the address based on
++ * the address of the last real argument *)
++ if !msvcMode then begin
++ let rec getLast = function
++ [] -> E.s (unimp "old-style variable argument function without real arguments")
++ | [a] -> a
++ | _ :: rest -> getLast rest
++ in
++ let last = getLast !currentFunctionFDEC.sformals in
++ let res = mkAddrOfAndMark (var last) in
++ let tres = typeOf res in
++ let tres', res' = castTo tres (TInt(IULong, [])) res in
++ (* Now we must add to this address to point to the next
++ * argument. Round up to a multiple of 4 *)
++ let sizeOfLast =
++ (((bitsSizeOf last.vtype) + 31) / 32) * 4
++ in
++ let res'' =
++ BinOp(PlusA, res', kinteger IULong sizeOfLast, tres')
++ in
++ finishExp empty res'' tres'
++ end else begin (* On GCC the only reliable way to do this is to
++ * call builtin_next_arg. If we take the address of
++ * a local we are going to get the address of a copy
++ * of the local ! *)
++
++ doExp asconst
++ (A.CALL (A.VARIABLE "__builtin_next_arg",
++ [A.CONSTANT (A.CONST_INT "0")]))
++ what
++ end
++
++ | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
++ A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ |
++ A.CAST (_, A.COMPOUND_INIT _)) -> begin
++ let (se, e', t) = doExp false e (AExp None) in
++ (* ignore (E.log "ADDROF on %a : %a\n" d_plainexp e'
++ d_plaintype t); *)
++ match e' with
++ ( Lval x | CastE(_, Lval x)) ->
++ finishExp se (mkAddrOfAndMark x) (TPtr(t, []))
++
++ | StartOf (lv) ->
++ let tres = TPtr(typeOfLval lv, []) in (* pointer to array *)
++ finishExp se (mkAddrOfAndMark lv) tres
++
++ (* Function names are converted into pointers to the function.
++ * Taking the address-of again does not change things *)
++ | AddrOf (Var v, NoOffset) when isFunctionType v.vtype ->
++ finishExp se e' t
++
++ | _ -> E.s (error "Expected lval for ADDROF. Got %a@!"
++ d_plainexp e')
++ end
++ | _ -> E.s (error "Unexpected operand for addrof")
++ end
++ | A.UNARY((A.PREINCR|A.PREDECR) as uop, e) -> begin
++ match e with
++ A.COMMA el -> (* GCC extension *)
++ doExp asconst
++ (A.COMMA (replaceLastInList el
++ (fun e -> A.UNARY(uop, e))))
++ what
++ | A.QUESTION (e1, e2q, e3q) -> (* GCC extension *)
++ doExp asconst
++ (A.QUESTION (e1, A.UNARY(uop, e2q),
++ A.UNARY(uop, e3q)))
++ what
++ | A.PAREN e1 ->
++ doExp asconst (A.UNARY(uop, e1)) what
++ | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
++ A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ |
++ A.CAST _ (* A GCC extension *)) -> begin
++ let uop' = if uop = A.PREINCR then PlusA else MinusA in
++ if asconst then
++ ignore (warn "PREINCR or PREDECR in constant");
++ let (se, e', t) = doExp false e (AExp None) in
++ let lv =
++ match e' with
++ Lval x -> x
++ | CastE (_, Lval x) -> x (* A GCC extension. The operation is
++ * done at the cast type. The result
++ * is also of the cast type *)
++ | _ -> E.s (error "Expected lval for ++ or --")
++ in
++ let tresult, result = doBinOp uop' e' t one intType in
++ finishExp (se +++ (Set(lv, makeCastT result tresult t,
++ !currentLoc)))
++ e'
++ tresult (* Should this be t instead ??? *)
++ end
++ | _ -> E.s (error "Unexpected operand for prefix -- or ++")
++ end
++
++ | A.UNARY((A.POSINCR|A.POSDECR) as uop, e) -> begin
++ match e with
++ A.COMMA el -> (* GCC extension *)
++ doExp asconst
++ (A.COMMA (replaceLastInList el
++ (fun e -> A.UNARY(uop, e))))
++ what
++ | A.QUESTION (e1, e2q, e3q) -> (* GCC extension *)
++ doExp asconst
++ (A.QUESTION (e1, A.UNARY(uop, e2q), A.UNARY(uop, e3q)))
++ what
++ | A.PAREN e1 -> doExp asconst (A.UNARY(uop,e1)) what
++ | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
++ A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ |
++ A.CAST _ (* A GCC extension *) ) -> begin
++ if asconst then
++ ignore (warn "POSTINCR or POSTDECR in constant");
++ (* If we do not drop the result then we must save the value *)
++ let uop' = if uop = A.POSINCR then PlusA else MinusA in
++ let (se, e', t) = doExp false e (AExp None) in
++ let lv =
++ match e' with
++ Lval x -> x
++ | CastE (_, Lval x) -> x (* GCC extension. The addition must
++ * be be done at the cast type. The
++ * result of this is also of the cast
++ * type *)
++ | _ -> E.s (error "Expected lval for ++ or --")
++ in
++ let tresult, opresult = doBinOp uop' e' t one intType in
++ let se', result =
++ if what <> ADrop && what <> AType then
++ let descr = (dd_exp () e')
++ ++ (if uop = A.POSINCR then text "++" else text "--") in
++ let tmp = newTempVar descr true t in
++ se +++ (Set(var tmp, e', !currentLoc)), Lval(var tmp)
++ else
++ se, e'
++ in
++ finishExp
++ (se' +++ (Set(lv, makeCastT opresult tresult (typeOfLval lv),
++ !currentLoc)))
++ result
++ tresult (* Should this be t instead ??? *)
++ end
++ | _ -> E.s (error "Unexpected operand for suffix ++ or --")
++ end
++
++ | A.BINARY(A.ASSIGN, e1, e2) -> begin
++ match e1 with
++ A.COMMA el -> (* GCC extension *)
++ doExp asconst
++ (A.COMMA (replaceLastInList el
++ (fun e -> A.BINARY(A.ASSIGN, e, e2))))
++ what
++ | A.QUESTION (e1, e2q, e3q) -> (* GCC extension *)
++ doExp asconst
++ (A.QUESTION (e1, A.BINARY(A.ASSIGN, e2q, e2),
++ A.BINARY(A.ASSIGN, e3q, e2)))
++ what
++ | A.CAST (t, A.SINGLE_INIT e) -> (* GCC extension *)
++ doExp asconst
++ (A.CAST (t,
++ A.SINGLE_INIT (A.BINARY(A.ASSIGN, e,
++ A.CAST (t, A.SINGLE_INIT e2)))))
++ what
++ | A.PAREN e1 -> doExp asconst (A.BINARY(A.ASSIGN,e1,e2)) what
++ | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
++ A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ ) -> begin
++ if asconst then ignore (warn "ASSIGN in constant");
++ let (se1, e1', lvt) = doExp false e1 (AExp None) in
++ let lv =
++ match e1' with
++ Lval x -> x
++ | _ -> E.s (error "Expected lval for assignment. Got %a\n"
++ d_plainexp e1')
++ in
++ (* Catch the case of an lval that might depend on itself,
++ e.g. p[p[0]] when p[0] == 0. We need to use a temporary
++ here if the result of the expression will be used:
++ tmp := e2; lv := tmp; use tmp as the result
++ Test: small1/assign.c *)
++ let needsTemp = match what, lv with
++ (ADrop|AType), _ -> false
++ | _, (Mem e, off) -> not (isConstant e)
++ || not (isConstantOffset off)
++ | _, (Var _, off) -> not (isConstantOffset off)
++ in
++ let tmplv, se3 =
++ if needsTemp then
++ let descr = (dd_lval () lv) in
++ let tmp = newTempVar descr true lvt in
++ var tmp, i2c (Set(lv, Lval(var tmp), !currentLoc))
++ else
++ lv, empty
++ in
++ let (se2, e'', t'') = doExp false e2 (ASet(tmplv, lvt)) in
++ finishExp (se1 @@ se2 @@ se3) (Lval tmplv) lvt
++ end
++ | _ -> E.s (error "Invalid left operand for ASSIGN")
++ end
++
++ | A.BINARY((A.ADD|A.SUB|A.MUL|A.DIV|A.MOD|A.BAND|A.BOR|A.XOR|
++ A.SHL|A.SHR|A.EQ|A.NE|A.LT|A.GT|A.GE|A.LE) as bop, e1, e2) ->
++ let bop' = convBinOp bop in
++ let (se1, e1', t1) = doExp asconst e1 (AExp None) in
++ let (se2, e2', t2) = doExp asconst e2 (AExp None) in
++ let tresult, result = doBinOp bop' e1' t1 e2' t2 in
++ finishExp (se1 @@ se2) result tresult
++
++ (* assignment operators *)
++ | A.BINARY((A.ADD_ASSIGN|A.SUB_ASSIGN|A.MUL_ASSIGN|A.DIV_ASSIGN|
++ A.MOD_ASSIGN|A.BAND_ASSIGN|A.BOR_ASSIGN|A.SHL_ASSIGN|
++ A.SHR_ASSIGN|A.XOR_ASSIGN) as bop, e1, e2) -> begin
++ match e1 with
++ A.COMMA el -> (* GCC extension *)
++ doExp asconst
++ (A.COMMA (replaceLastInList el
++ (fun e -> A.BINARY(bop, e, e2))))
++ what
++ | A.QUESTION (e1, e2q, e3q) -> (* GCC extension *)
++ doExp asconst
++ (A.QUESTION (e1, A.BINARY(bop, e2q, e2),
++ A.BINARY(bop, e3q, e2)))
++ what
++ | A.PAREN e1 -> doExp asconst (A.BINARY(bop,e1,e2)) what
++ | (A.VARIABLE _ | A.UNARY (A.MEMOF, _) | (* Regular lvalues *)
++ A.INDEX _ | A.MEMBEROF _ | A.MEMBEROFPTR _ |
++ A.CAST _ (* GCC extension *) ) -> begin
++ if asconst then
++ ignore (warn "op_ASSIGN in constant");
++ let bop' = match bop with
++ A.ADD_ASSIGN -> PlusA
++ | A.SUB_ASSIGN -> MinusA
++ | A.MUL_ASSIGN -> Mult
++ | A.DIV_ASSIGN -> Div
++ | A.MOD_ASSIGN -> Mod
++ | A.BAND_ASSIGN -> BAnd
++ | A.BOR_ASSIGN -> BOr
++ | A.XOR_ASSIGN -> BXor
++ | A.SHL_ASSIGN -> Shiftlt
++ | A.SHR_ASSIGN -> Shiftrt
++ | _ -> E.s (error "binary +=")
++ in
++ let (se1, e1', t1) = doExp false e1 (AExp None) in
++ let lv1 =
++ match e1' with
++ Lval x -> x
++ | CastE (_, Lval x) -> x (* GCC extension. The operation and
++ * the result are at the cast type *)
++ | _ -> E.s (error "Expected lval for assignment with arith")
++ in
++ let (se2, e2', t2) = doExp false e2 (AExp None) in
++ let tresult, result = doBinOp bop' e1' t1 e2' t2 in
++ (* We must cast the result to the type of the lv1, which may be
++ * different than t1 if lv1 was a Cast *)
++ let _, result' = castTo tresult (typeOfLval lv1) result in
++ (* The type of the result is the type of the left-hand side *)
++ finishExp (se1 @@ se2 +++
++ (Set(lv1, result', !currentLoc)))
++ e1'
++ t1
++ end
++ | _ -> E.s (error "Unexpected left operand for assignment with arith")
++ end
++
++
++ | A.BINARY((A.AND|A.OR), _, _) | A.UNARY(A.NOT, _) -> begin
++ let ce = doCondExp asconst e in
++ (* We must normalize the result to 0 or 1 *)
++ match ce with
++ CEExp (se, ((Const _) as c)) ->
++ finishExp se (if isConstTrue c then one else zero) intType
++ | CEExp (se, (UnOp(LNot, _, _) as e)) ->
++ (* already normalized to 0 or 1 *)
++ finishExp se e intType
++ | CEExp (se, e) ->
++ let e' =
++ let te = typeOf e in
++ let _, zte = castTo intType te zero in
++ BinOp(Ne, e, zte, te)
++ in
++ finishExp se e' intType
++ | _ ->
++ let tmp =
++ var (newTempVar (text "<boolean expression>") true intType)
++ in
++ finishExp (compileCondExp ce
++ (empty +++ (Set(tmp, integer 1,
++ !currentLoc)))
++ (empty +++ (Set(tmp, integer 0,
++ !currentLoc))))
++ (Lval tmp)
++ intType
++ end
++
++ | A.CALL(f, args) ->
++ if asconst then
++ ignore (warn "CALL in constant");
++ let (sf, f', ft') =
++ match f with (* Treat the VARIABLE case separate
++ * because we might be calling a
++ * function that does not have a
++ * prototype. In that case assume it
++ * takes INTs as arguments *)
++ A.VARIABLE n -> begin
++ try
++ let vi, _ = lookupVar n in
++ (empty, Lval(var vi), vi.vtype) (* Found. Do not use
++ * finishExp. Simulate what =
++ * AExp None *)
++ with Not_found -> begin
++ ignore (warnOpt "Calling function %s without prototype." n);
++ let ftype = TFun(intType, None, false,
++ [Attr("missingproto",[])]) in
++ (* Add a prototype to the environment *)
++ let proto, _ =
++ makeGlobalVarinfo false (makeGlobalVar n ftype) in
++ (* Make it EXTERN *)
++ proto.vstorage <- Extern;
++ IH.add noProtoFunctions proto.vid true;
++ (* Add it to the file as well *)
++ cabsPushGlobal (GVarDecl (proto, !currentLoc));
++ (empty, Lval(var proto), ftype)
++ end
++ end
++ | _ -> doExp false f (AExp None)
++ in
++ (* Get the result type and the argument types *)
++ let (resType, argTypes, isvar, f'') =
++ match unrollType ft' with
++ TFun(rt,at,isvar,a) -> (rt,at,isvar,f')
++ | TPtr (t, _) -> begin
++ match unrollType t with
++ TFun(rt,at,isvar,a) -> (* Make the function pointer
++ * explicit *)
++ let f'' =
++ match f' with
++ AddrOf lv -> Lval(lv)
++ | _ -> Lval(mkMem f' NoOffset)
++ in
++ (rt,at,isvar, f'')
++ | x ->
++ E.s (error "Unexpected type of the called function %a: %a"
++ d_exp f' d_type x)
++ end
++ | x -> E.s (error "Unexpected type of the called function %a: %a"
++ d_exp f' d_type x)
++ in
++ let argTypesList = argsToList argTypes in
++ (* Drop certain qualifiers from the result type *)
++ let resType' = typeRemoveAttributes ["warn_unused_result"] resType in
++ (* Before we do the arguments we try to intercept a few builtins. For
++ * these we have defined then with a different type, so we do not
++ * want to give warnings. We'll just leave the arguments of these
++ * functions alone*)
++ let isSpecialBuiltin =
++ match f'' with
++ Lval (Var fv, NoOffset) ->
++ fv.vname = "__builtin_stdarg_start" ||
++ fv.vname = "__builtin_va_arg" ||
++ fv.vname = "__builtin_va_start" ||
++ fv.vname = "__builtin_expect" ||
++ fv.vname = "__builtin_next_arg"
++ | _ -> false
++ in
++
++ (** If the "--forceRLArgEval" flag was used, make sure
++ we evaluate args right-to-left.
++ Added by Nathan Cooprider. **)
++ let force_right_to_left_evaluation (c, e, t) =
++ (* If chunk is empty then it is not already evaluated *)
++ (* constants don't need to be pulled out *)
++ if (!forceRLArgEval && (not (isConstant e)) &&
++ (not isSpecialBuiltin)) then
++ (* create a temporary *)
++ let tmp = newTempVar (dd_exp () e) true t in
++ (* create an instruction to give the e to the temporary *)
++ let i = Set(var tmp, e, !currentLoc) in
++ (* add the instruction to the chunk *)
++ (* change the expression to be the temporary *)
++ (c +++ i, (Lval(var tmp)), t)
++ else
++ (c, e, t)
++ in
++ (* Do the arguments. In REVERSE order !!! Both GCC and MSVC do this *)
++ let rec loopArgs
++ : (string * typ * attributes) list * A.expression list
++ -> (chunk * exp list) = function
++ | ([], []) -> (empty, [])
++
++ | args, [] ->
++ if not isSpecialBuiltin then
++ ignore (warnOpt
++ "Too few arguments in call to %a."
++ d_exp f');
++ (empty, [])
++
++ | ((_, at, _) :: atypes, a :: args) ->
++ let (ss, args') = loopArgs (atypes, args) in
++ (* Do not cast as part of translating the argument. We let
++ * the castTo do this work. This was necessary for
++ * test/small1/union5, in which a transparent union is passed
++ * as an argument *)
++ let (sa, a', att) = force_right_to_left_evaluation
++ (doExp false a (AExp None)) in
++ let (_, a'') = castTo att at a' in
++ (ss @@ sa, a'' :: args')
++
++ | ([], args) -> (* No more types *)
++ if not isvar && argTypes != None && not isSpecialBuiltin then
++ (* Do not give a warning for functions without a prototype*)
++ ignore (warnOpt "Too many arguments in call to %a" d_exp f');
++ let rec loop = function
++ [] -> (empty, [])
++ | a :: args ->
++ let (ss, args') = loop args in
++ let (sa, a', at) = force_right_to_left_evaluation
++ (doExp false a (AExp None)) in
++ (ss @@ sa, a' :: args')
++ in
++ loop args
++ in
++ let (sargs, args') = loopArgs (argTypesList, args) in
++ (* Setup some pointer to the elements of the call. We may change
++ * these below *)
++ let prechunk: chunk ref = ref (sf @@ sargs) in (* comes before *)
++
++ (* Do we actually have a call, or an expression? *)
++ let piscall: bool ref = ref true in
++
++ let pf: exp ref = ref f'' in (* function to call *)
++ let pargs: exp list ref = ref args' in (* arguments *)
++ let pis__builtin_va_arg: bool ref = ref false in
++ let pwhat: expAction ref = ref what in (* what to do with result *)
++
++ let pres: exp ref = ref zero in (* If we do not have a call, this is
++ * the result *)
++ let prestype: typ ref = ref intType in
++
++ let rec dropCasts = function CastE (_, e) -> dropCasts e | e -> e in
++ (* Get the name of the last formal *)
++ let getNameLastFormal () : string =
++ match !currentFunctionFDEC.svar.vtype with
++ TFun(_, Some args, true, _) -> begin
++ match List.rev args with
++ (last_par_name, _, _) :: _ -> last_par_name
++ | _ -> ""
++ end
++ | _ -> ""
++ in
++
++ (* Try to intercept some builtins *)
++ (match !pf with
++ Lval(Var fv, NoOffset) -> begin
++ if fv.vname = "__builtin_va_arg" then begin
++ match !pargs with
++ marker :: SizeOf resTyp :: _ -> begin
++ (* Make a variable of the desired type *)
++ let destlv, destlvtyp =
++ match !pwhat with
++ ASet (lv, lvt) -> lv, lvt
++ | _ -> var (newTempVar nil true resTyp), resTyp
++ in
++ pwhat := (ASet (destlv, destlvtyp));
++ pargs := [marker; SizeOf resTyp;
++ CastE(voidPtrType, AddrOf destlv)];
++ pis__builtin_va_arg := true;
++ end
++ | _ ->
++ ignore (warn "Invalid call to %s\n" fv.vname);
++ end else if fv.vname = "__builtin_stdarg_start" ||
++ fv.vname = "__builtin_va_start" then begin
++ match !pargs with
++ marker :: last :: [] -> begin
++ let isOk =
++ match dropCasts last with
++ Lval (Var lastv, NoOffset) ->
++ lastv.vname = getNameLastFormal ()
++ | _ -> false
++ in
++ if not isOk then
++ ignore (warn "The second argument in call to %s should be the last formal argument\n" fv.vname);
++
++ (* Check that "lastv" is indeed the last variable in the
++ * prototype and then drop it *)
++ pargs := [ marker ]
++ end
++ | _ ->
++ ignore (warn "Invalid call to %s\n" fv.vname);
++
++ (* We have to turn uses of __builtin_varargs_start into uses
++ * of __builtin_stdarg_start (because we have dropped the
++ * __builtin_va_alist argument from this function) *)
++
++ end else if fv.vname = "__builtin_varargs_start" then begin
++ (* Lookup the prototype for the replacement *)
++ let v, _ =
++ try lookupGlobalVar "__builtin_stdarg_start"
++ with Not_found -> E.s (bug "Cannot find __builtin_stdarg_start to replace %s\n" fv.vname)
++ in
++ pf := Lval (var v)
++ end else if fv.vname = "__builtin_next_arg" then begin
++ match !pargs with
++ last :: [] -> begin
++ let isOk =
++ match dropCasts last with
++ Lval (Var lastv, NoOffset) ->
++ lastv.vname = getNameLastFormal ()
++ | _ -> false
++ in
++ if not isOk then
++ ignore (warn "The argument in call to %s should be the last formal argument\n" fv.vname);
++
++ pargs := [ ]
++ end
++ | _ ->
++ ignore (warn "Invalid call to %s\n" fv.vname);
++ end else if fv.vname = "__builtin_constant_p" then begin
++ (* Drop the side-effects *)
++ prechunk := empty;
++
++ (* Constant-fold the argument and see if it is a constant *)
++ (match !pargs with
++ [ arg ] -> begin
++ match constFold true arg with
++ Const _ -> piscall := false;
++ pres := integer 1;
++ prestype := intType
++
++ | _ -> piscall := false;
++ pres := integer 0;
++ prestype := intType
++ end
++ | _ ->
++ ignore (warn "Invalid call to builtin_constant_p"));
++ end
++ end
++ | _ -> ());
++
++
++ (* Now we must finish the call *)
++ if !piscall then begin
++ let addCall (calldest: lval option) (res: exp) (t: typ) =
++ prechunk := !prechunk +++
++ (Call(calldest, !pf, !pargs, !currentLoc));
++ pres := res;
++ prestype := t
++ in
++ match !pwhat with
++ ADrop -> addCall None zero intType
++
++ | AType -> prestype := resType'
++
++ | ASet(lv, vtype) when !pis__builtin_va_arg ->
++ (* Make an exception here for __builtin_va_arg *)
++ addCall None (Lval(lv)) vtype
++
++ | ASet(lv, vtype) when !doCollapseCallCast ||
++ (Util.equals (typeSig vtype) (typeSig resType'))
++ ->
++ (* We can assign the result directly to lv *)
++ addCall (Some lv) (Lval(lv)) vtype
++
++ | _ -> begin
++ let restype'' =
++ match !pwhat with
++ AExp (Some t) when !doCollapseCallCast -> t
++ | _ -> resType'
++ in
++ let descr = dprintf "%a(%a)" dd_exp !pf
++ (docList ~sep:(text ", ") (dd_exp ())) !pargs in
++ let tmp = newTempVar descr false restype'' in
++ (* Remember that this variable has been created for this
++ * specific call. We will use this in collapseCallCast. *)
++ IH.add callTempVars tmp.vid ();
++ addCall (Some (var tmp)) (Lval(var tmp)) restype''
++ end
++ end;
++
++ finishExp !prechunk !pres !prestype
++
++
++ | A.COMMA el ->
++ if asconst then
++ ignore (warn "COMMA in constant");
++ let rec loop sofar = function
++ [e] ->
++ let (se, e', t') = doExp false e what in (* Pass on the action *)
++ (sofar @@ se, e', t')
++(*
++ finishExp (sofar @@ se) e' t' (* does not hurt to do it twice.
++ * GN: it seems it does *)
++*)
++ | e :: rest ->
++ let (se, _, _) = doExp false e ADrop in
++ loop (sofar @@ se) rest
++ | [] -> E.s (error "empty COMMA expression")
++ in
++ loop empty el
++
++ | A.QUESTION (e1,e2,e3) when what = ADrop ->
++ if asconst then
++ ignore (warn "QUESTION with ADrop in constant");
++ let (se3,_,_) = doExp false e3 ADrop in
++ let se2 =
++ match e2 with
++ A.NOTHING -> skipChunk
++ | _ -> let (se2,_,_) = doExp false e2 ADrop in se2
++ in
++ finishExp (doCondition asconst e1 se2 se3) zero intType
++
++ | A.QUESTION (e1, e2, e3) -> begin (* what is not ADrop *)
++ (* Compile the conditional expression *)
++ let ce1 = doCondExp asconst e1 in
++ (* Now we must find the type of both branches, in order to compute
++ * the type of the result *)
++ let se2, e2'o (* is an option. None means use e1 *), t2 =
++ match e2 with
++ A.NOTHING -> begin (* The same as the type of e1 *)
++ match ce1 with
++ CEExp (_, e1') -> empty, None, typeOf e1' (* Do not promote
++ to bool *)
++ | _ -> empty, None, intType
++ end
++ | _ ->
++ let se2, e2', t2 = doExp asconst e2 (AExp None) in
++ se2, Some e2', t2
++ in
++ (* Do e3 for real *)
++ let se3, e3', t3 = doExp asconst e3 (AExp None) in
++ (* Compute the type of the result *)
++ let tresult = conditionalConversion t2 t3 in
++ match ce1 with
++ CEExp (se1, e1') when isConstFalse e1' && canDrop se2 ->
++ finishExp (se1 @@ se3) (snd (castTo t3 tresult e3')) tresult
++ | CEExp (se1, e1') when isConstTrue e1' && canDrop se3 ->
++ begin
++ match e2'o with
++ None -> (* use e1' *)
++ finishExp (se1 @@ se2) (snd (castTo t2 tresult e1')) tresult
++ | Some e2' ->
++ finishExp (se1 @@ se2) (snd (castTo t2 tresult e2')) tresult
++ end
++
++ | _ -> (* Use a conditional *) begin
++ match e2'o with
++ None -> (* has form "e1 ? : e3" *)
++ let tmp = var (newTempVar nil true tresult) in
++ let (se1, _, _) = doExp asconst e1 (ASet(tmp, tresult)) in
++ let (se3, _, _) = finishExp ~newWhat:(ASet(tmp, tresult))
++ se3 e3' t3 in
++ finishExp (se1 @@ ifChunk (Lval(tmp)) !currentLoc
++ skipChunk se3)
++ (Lval(tmp))
++ tresult
++ | Some e2' ->
++ let lv, lvt =
++ match what with
++ | ASet (lv, lvt) -> lv, lvt
++ | _ ->
++ let tmp = newTempVar nil true tresult in
++ var tmp, tresult
++ in
++ (* Now add the stmts lv:=e2 and lv:=e3 to se2 and se3 *)
++ let (se2, _, _) = finishExp ~newWhat:(ASet(lv,lvt))
++ se2 e2' t2 in
++ let (se3, _, _) = finishExp ~newWhat:(ASet(lv,lvt))
++ se3 e3' t3 in
++ finishExp (doCondition asconst e1 se2 se3) (Lval(lv)) tresult
++ end
++
++(*
++ (* Do these only to collect the types *)
++ let se2, e2', t2' =
++ match e2 with
++ A.NOTHING -> (* A GNU thing. Use e1 as e2 *)
++ doExp isconst e1 (AExp None)
++ | _ -> doExp isconst e2 (AExp None) in
++ (* Do e3 for real *)
++ let se3, e3', t3' = doExp isconst e3 (AExp None) in
++ (* Compute the type of the result *)
++ let tresult = conditionalConversion e2' t2' e3' t3' in
++ if (isEmpty se2 || e2 = A.NOTHING)
++ && isEmpty se3 && isconst then begin
++ (* Use the Question. This allows Question in initializers without
++ * having to do constant folding *)
++ let se1, e1', t1 = doExp isconst e1 (AExp None) in
++ ignore (checkBool t1 e1');
++ let e2'' =
++ if e2 = A.NOTHING then
++ makeCastT e1' t1 tresult
++ else makeCastT e2' t2' tresult (* We know se2 is empty *)
++ in
++ let e3'' = makeCastT e3' t3' tresult in
++ let resexp =
++ match e1' with
++ Const(CInt64(i, _, _)) when i <> Int64.zero -> e2''
++ | Const(CInt64(z, _, _)) when z = Int64.zero -> e3''
++ | _ -> Question(e1', e2'', e3'')
++ in
++ finishExp se1 resexp tresult
++ end else begin (* Now use a conditional *)
++ match e2 with
++ A.NOTHING ->
++ let tmp = var (newTempVar tresult) in
++ let (se1, _, _) = doExp isconst e1 (ASet(tmp, tresult)) in
++ let (se3, _, _) = doExp isconst e3 (ASet(tmp, tresult)) in
++ finishExp (se1 @@ ifChunk (Lval(tmp)) lu
++ skipChunk se3)
++ (Lval(tmp))
++ tresult
++ | _ ->
++ let lv, lvt =
++ match what with
++ | ASet (lv, lvt) -> lv, lvt
++ | _ ->
++ let tmp = newTempVar tresult in
++ var tmp, tresult
++ in
++ (* Now do e2 and e3 for real *)
++ let (se2, _, _) = doExp isconst e2 (ASet(lv, lvt)) in
++ let (se3, _, _) = doExp isconst e3 (ASet(lv, lvt)) in
++ finishExp (doCondition isconst e1 se2 se3) (Lval(lv)) tresult
++ end
++*)
++ end
++
++ | A.GNU_BODY b -> begin
++ (* Find the last A.COMPUTATION and remember it. This one is invoked
++ * on the reversed list of statements. *)
++ let rec findLastComputation = function
++ s :: _ ->
++ let rec findLast = function
++ A.SEQUENCE (_, s, loc) -> findLast s
++ | CASE (_, s, _) -> findLast s
++ | CASERANGE (_, _, s, _) -> findLast s
++ | LABEL (_, s, _) -> findLast s
++ | (A.COMPUTATION _) as s -> s
++ | _ -> raise Not_found
++ in
++ findLast s
++ | [] -> raise Not_found
++ in
++ (* Save the previous data *)
++ let old_gnu = ! gnu_body_result in
++ let lastComp, isvoidbody =
++ match what with
++ ADrop -> (* We are dropping the result *)
++ A.NOP cabslu, true
++ | _ ->
++ try findLastComputation (List.rev b.A.bstmts), false
++ with Not_found ->
++ E.s (error "Cannot find COMPUTATION in GNU.body")
++ (* A.NOP cabslu, true *)
++ in
++ (* Prepare some data to be filled by doExp *)
++ let data : (exp * typ) option ref = ref None in
++ gnu_body_result := (lastComp, data);
++
++ let se = doBody b in
++
++ gnu_body_result := old_gnu;
++ match !data with
++ None when isvoidbody -> finishExp se zero voidType
++ | None -> E.s (bug "Cannot find COMPUTATION in GNU.body")
++ | Some (e, t) -> finishExp se e t
++ end
++
++ | A.LABELADDR l -> begin (* GCC's taking the address of a label *)
++ let l = lookupLabel l in (* To support locallly declared labels *)
++ let addrval =
++ try H.find gotoTargetHash l
++ with Not_found -> begin
++ let res = !gotoTargetNextAddr in
++ incr gotoTargetNextAddr;
++ H.add gotoTargetHash l res;
++ res
++ end
++ in
++ finishExp empty (makeCast (integer addrval) voidPtrType) voidPtrType
++ end
++
++ | A.EXPR_PATTERN _ -> E.s (E.bug "EXPR_PATTERN in cabs2cil input")
++
++ with e when continueOnError -> begin
++ ignore (E.log "error in doExp (%s)@!" (Printexc.to_string e));
++ E.hadErrors := true;
++ (i2c (dInstr (dprintf "booo_exp(%t)" d_thisloc) !currentLoc),
++ integer 0, intType)
++ end
++
++(* bop is always the arithmetic version. Change it to the appropriate pointer
++ * version if necessary *)
++and doBinOp (bop: binop) (e1: exp) (t1: typ) (e2: exp) (t2: typ) : typ * exp =
++ let doArithmetic () =
++ let tres = arithmeticConversion t1 t2 in
++ (* Keep the operator since it is arithmetic *)
++ tres,
++ optConstFoldBinOp false bop (makeCastT e1 t1 tres) (makeCastT e2 t2 tres) tres
++ in
++ let doArithmeticComp () =
++ let tres = arithmeticConversion t1 t2 in
++ (* Keep the operator since it is arithemtic *)
++ intType,
++ optConstFoldBinOp false bop
++ (makeCastT e1 t1 tres) (makeCastT e2 t2 tres) intType
++ in
++ let doIntegralArithmetic () =
++ let tres = unrollType (arithmeticConversion t1 t2) in
++ match tres with
++ TInt _ ->
++ tres,
++ optConstFoldBinOp false bop
++ (makeCastT e1 t1 tres) (makeCastT e2 t2 tres) tres
++ | _ -> E.s (error "%a operator on a non-integer type" d_binop bop)
++ in
++ let pointerComparison e1 t1 e2 t2 =
++ (* Cast both sides to an integer *)
++ let commontype = !upointType in
++ intType,
++ optConstFoldBinOp false bop (makeCastT e1 t1 commontype)
++ (makeCastT e2 t2 commontype) intType
++ in
++
++ match bop with
++ (Mult|Div) -> doArithmetic ()
++ | (Mod|BAnd|BOr|BXor) -> doIntegralArithmetic ()
++ | (Shiftlt|Shiftrt) -> (* ISO 6.5.7. Only integral promotions. The result
++ * has the same type as the left hand side *)
++ if !msvcMode then
++ (* MSVC has a bug. We duplicate it here *)
++ doIntegralArithmetic ()
++ else
++ let t1' = integralPromotion t1 in
++ let t2' = integralPromotion t2 in
++ t1',
++ optConstFoldBinOp false bop (makeCastT e1 t1 t1') (makeCastT e2 t2 t2') t1'
++
++ | (PlusA|MinusA)
++ when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic ()
++ | (Eq|Ne|Lt|Le|Ge|Gt)
++ when isArithmeticType t1 && isArithmeticType t2 ->
++ doArithmeticComp ()
++ | PlusA when isPointerType t1 && isIntegralType t2 ->
++ t1,
++ optConstFoldBinOp false PlusPI e1
++ (makeCastT e2 t2 (integralPromotion t2)) t1
++ | PlusA when isIntegralType t1 && isPointerType t2 ->
++ t2,
++ optConstFoldBinOp false PlusPI e2
++ (makeCastT e1 t1 (integralPromotion t1)) t2
++ | MinusA when isPointerType t1 && isIntegralType t2 ->
++ t1,
++ optConstFoldBinOp false MinusPI e1
++ (makeCastT e2 t2 (integralPromotion t2)) t1
++ | MinusA when isPointerType t1 && isPointerType t2 ->
++ let commontype = t1 in
++ intType,
++ optConstFoldBinOp false MinusPP (makeCastT e1 t1 commontype)
++ (makeCastT e2 t2 commontype) intType
++ | (Le|Lt|Ge|Gt|Eq|Ne) when isPointerType t1 && isPointerType t2 ->
++ pointerComparison e1 t1 e2 t2
++ | (Eq|Ne) when isPointerType t1 && isZero e2 ->
++ pointerComparison e1 t1 (makeCastT zero !upointType t1) t1
++ | (Eq|Ne) when isPointerType t2 && isZero e1 ->
++ pointerComparison (makeCastT zero !upointType t2) t2 e2 t2
++
++ | (Eq|Ne) when isVariadicListType t1 && isZero e2 ->
++ ignore (warnOpt "Comparison of va_list and zero");
++ pointerComparison e1 t1 (makeCastT zero !upointType t1) t1
++ | (Eq|Ne) when isVariadicListType t2 && isZero e1 ->
++ ignore (warnOpt "Comparison of zero and va_list");
++ pointerComparison (makeCastT zero !upointType t2) t2 e2 t2
++
++ | (Eq|Ne|Le|Lt|Ge|Gt) when isPointerType t1 && isArithmeticType t2 ->
++ ignore (warnOpt "Comparison of pointer and non-pointer");
++ (* Cast both values to upointType *)
++ doBinOp bop (makeCastT e1 t1 !upointType) !upointType
++ (makeCastT e2 t2 !upointType) !upointType
++ | (Eq|Ne|Le|Lt|Ge|Gt) when isArithmeticType t1 && isPointerType t2 ->
++ ignore (warnOpt "Comparison of pointer and non-pointer");
++ (* Cast both values to upointType *)
++ doBinOp bop (makeCastT e1 t1 !upointType) !upointType
++ (makeCastT e2 t2 !upointType) !upointType
++
++ | _ -> E.s (error "Invalid operands to binary operator: %a\n" d_plainexp (BinOp(bop,e1,e2,intType)))
++
++(* Constant fold a conditional. This is because we want to avoid having
++ * conditionals in the initializers. So, we try very hard to avoid creating
++ * new statements. *)
++and doCondExp (asconst: bool) (** Try to evaluate the conditional expression
++ * to TRUE or FALSE, because it occurs in a
++ * constant *)
++ (e: A.expression) : condExpRes =
++ let rec addChunkBeforeCE (c0: chunk) = function
++ CEExp (c, e) -> CEExp (c0 @@ c, e)
++ | CEAnd (ce1, ce2) -> CEAnd (addChunkBeforeCE c0 ce1, ce2)
++ | CEOr (ce1, ce2) -> CEOr (addChunkBeforeCE c0 ce1, ce2)
++ | CENot ce1 -> CENot (addChunkBeforeCE c0 ce1)
++ in
++ let rec canDropCE = function
++ CEExp (c, e) -> canDrop c
++ | CEAnd (ce1, ce2) | CEOr (ce1, ce2) -> canDropCE ce1 && canDropCE ce2
++ | CENot (ce1) -> canDropCE ce1
++ in
++ match e with
++ A.BINARY (A.AND, e1, e2) -> begin
++ let ce1 = doCondExp asconst e1 in
++ let ce2 = doCondExp asconst e2 in
++ match ce1, ce2 with
++ CEExp (se1, ((Const _) as ci1)), _ ->
++ if isConstTrue ci1 then
++ addChunkBeforeCE se1 ce2
++ else
++ (* se2 might contain labels so we cannot always drop it *)
++ if canDropCE ce2 then
++ ce1
++ else
++ CEAnd (ce1, ce2)
++ | CEExp(se1, e1'), CEExp (se2, e2') when
++ !useLogicalOperators && isEmpty se1 && isEmpty se2 ->
++ CEExp (empty, BinOp(LAnd,
++ makeCast e1' intType,
++ makeCast e2' intType, intType))
++ | _ -> CEAnd (ce1, ce2)
++ end
++
++ | A.BINARY (A.OR, e1, e2) -> begin
++ let ce1 = doCondExp asconst e1 in
++ let ce2 = doCondExp asconst e2 in
++ match ce1, ce2 with
++ CEExp (se1, (Const(CInt64 _) as ci1)), _ ->
++ if isConstFalse ci1 then
++ addChunkBeforeCE se1 ce2
++ else
++ (* se2 might contain labels so we cannot drop it *)
++ if canDropCE ce2 then
++ ce1
++ else
++ CEOr (ce1, ce2)
++
++ | CEExp (se1, e1'), CEExp (se2, e2') when
++ !useLogicalOperators && isEmpty se1 && isEmpty se2 ->
++ CEExp (empty, BinOp(LOr, makeCast e1' intType,
++ makeCast e2' intType, intType))
++ | _ -> CEOr (ce1, ce2)
++ end
++
++ | A.UNARY(A.NOT, e1) -> begin
++ match doCondExp asconst e1 with
++ CEExp (se1, (Const _ as ci1)) ->
++ if isConstFalse ci1 then
++ CEExp (se1, one)
++ else
++ CEExp (se1, zero)
++ | CEExp (se1, e) when isEmpty se1 ->
++ let t = typeOf e in
++ if not ((isPointerType t) || (isArithmeticType t))then
++ E.s (error "Bad operand to !");
++ CEExp (empty, UnOp(LNot, e, intType))
++
++ | ce1 -> CENot ce1
++ end
++
++ | _ ->
++ let (se, e, t) = doExp asconst e (AExp None) in
++ ignore (checkBool t e);
++ CEExp (se, if !lowerConstants then constFold asconst e else e)
++
++and compileCondExp (ce: condExpRes) (st: chunk) (sf: chunk) : chunk =
++ match ce with
++ | CEAnd (ce1, ce2) ->
++ let (sf1, sf2) =
++ (* If sf is small then will copy it *)
++ try (sf, duplicateChunk sf)
++ with Failure _ ->
++ let lab = newLabelName "_L" in
++ (gotoChunk lab lu, consLabel lab sf !currentLoc false)
++ in
++ let st' = compileCondExp ce2 st sf1 in
++ let sf' = sf2 in
++ compileCondExp ce1 st' sf'
++
++ | CEOr (ce1, ce2) ->
++ let (st1, st2) =
++ (* If st is small then will copy it *)
++ try (st, duplicateChunk st)
++ with Failure _ ->
++ let lab = newLabelName "_L" in
++ (gotoChunk lab lu, consLabel lab st !currentLoc false)
++ in
++ let st' = st1 in
++ let sf' = compileCondExp ce2 st2 sf in
++ compileCondExp ce1 st' sf'
++
++ | CENot ce1 -> compileCondExp ce1 sf st
++
++ | CEExp (se, e) -> begin
++ match e with
++ Const(CInt64(i,_,_)) when i <> Int64.zero && canDrop sf -> se @@ st
++ | Const(CInt64(z,_,_)) when z = Int64.zero && canDrop st -> se @@ sf
++ | _ -> se @@ ifChunk e !currentLoc st sf
++ end
++
++
++(* A special case for conditionals *)
++and doCondition (isconst: bool) (* If we are in constants, we do our best to
++ * eliminate the conditional *)
++ (e: A.expression)
++ (st: chunk)
++ (sf: chunk) : chunk =
++ compileCondExp (doCondExp isconst e) st sf
++
++
++and doPureExp (e : A.expression) : exp =
++ let (se, e', _) = doExp true e (AExp None) in
++ if isNotEmpty se then
++ E.s (error "doPureExp: not pure");
++ e'
++
++and doInitializer
++ (vi: varinfo)
++ (inite: A.init_expression)
++ (* Return the accumulated chunk, the initializer and the new type (might be
++ * different for arrays) *)
++ : chunk * init * typ =
++
++ (* Setup the pre-initializer *)
++ let topPreInit = ref NoInitPre in
++ if debugInit then
++ ignore (E.log "\nStarting a new initializer for %s : %a\n"
++ vi.vname d_type vi.vtype);
++ let topSetupInit (o: offset) (e: exp) =
++ if debugInit then
++ ignore (E.log " set %a := %a\n" d_lval (Var vi, o) d_exp e);
++ let newinit = setOneInit !topPreInit o e in
++ if newinit != !topPreInit then topPreInit := newinit
++ in
++ let acc, restl =
++ let so = makeSubobj vi vi.vtype NoOffset in
++ doInit vi.vglob topSetupInit so empty [ (A.NEXT_INIT, inite) ]
++ in
++ if restl <> [] then
++ ignore (warn "Ignoring some initializers");
++ (* sm: we used to do array-size fixups here, but they only worked
++ * for toplevel array types; now, collectInitializer does the job,
++ * including for nested array types *)
++ let typ' = unrollType vi.vtype in
++ if debugInit then
++ ignore (E.log "Collecting the initializer for %s\n" vi.vname);
++ let (init, typ'') = collectInitializer !topPreInit typ' in
++ if debugInit then
++ ignore (E.log "Finished the initializer for %s\n init=%a\n typ=%a\n acc=%a\n"
++ vi.vname d_init init d_type typ' d_chunk acc);
++ acc, init, typ''
++
++
++
++(* Consume some initializers. Watch out here. Make sure we use only
++ * tail-recursion because these things can be big. *)
++and doInit
++ (isconst: bool)
++ (setone: offset -> exp -> unit) (* Use to announce an intializer *)
++ (so: subobj)
++ (acc: chunk)
++ (initl: (A.initwhat * A.init_expression) list)
++
++ (* Return the resulting chunk along with some unused initializers *)
++ : chunk * (A.initwhat * A.init_expression) list =
++
++ let whoami () = d_lval () (Var so.host, so.soOff) in
++
++ let initl1 =
++ match initl with
++ | (A.NEXT_INIT,
++ A.SINGLE_INIT (A.CAST ((s, dt), ie))) :: rest ->
++ let s', dt', ie' = preprocessCast s dt ie in
++ (A.NEXT_INIT, A.SINGLE_INIT (A.CAST ((s', dt'), ie'))) :: rest
++ | _ -> initl
++ in
++ (* Sometimes we have a cast in front of a compound (in GCC). This
++ * appears as a single initializer. Ignore the cast *)
++ let initl2 =
++ match initl1 with
++ (what,
++ A.SINGLE_INIT (A.CAST ((specs, dt), A.COMPOUND_INIT ci))) :: rest ->
++ let s', dt', ie' = preprocessCast specs dt (A.COMPOUND_INIT ci) in
++ let typ = doOnlyType s' dt' in
++ if (typeSigNoAttrs typ) = (typeSigNoAttrs so.soTyp) then
++ (* Drop the cast *)
++ (what, A.COMPOUND_INIT ci) :: rest
++ else
++ (* Keep the cast. A new var will be created to hold
++ the intermediate value. *)
++ initl1
++ | _ -> initl1
++ in
++ let allinitl = initl2 in
++
++ if debugInit then begin
++ ignore (E.log "doInit for %t %s (current %a). Looking at: " whoami
++ (if so.eof then "(eof)" else "")
++ d_lval (Var so.host, so.curOff));
++ (match allinitl with
++ [] -> ignore (E.log "[]")
++ | (what, ie) :: _ ->
++ withCprint
++ Cprint.print_init_expression (A.COMPOUND_INIT [(what, ie)]));
++ ignore (E.log "\n");
++ end;
++ match unrollType so.soTyp, allinitl with
++ _, [] -> acc, [] (* No more initializers return *)
++
++ (* No more subobjects *)
++ | _, (A.NEXT_INIT, _) :: _ when so.eof -> acc, allinitl
++
++
++ (* If we are at an array of characters and the initializer is a
++ * string literal (optionally enclosed in braces) then explode the
++ * string into characters *)
++ | TArray(bt, leno, _),
++ (A.NEXT_INIT,
++ (A.SINGLE_INIT(A.CONSTANT (A.CONST_STRING s))|
++ A.COMPOUND_INIT
++ [(A.NEXT_INIT,
++ A.SINGLE_INIT(A.CONSTANT
++ (A.CONST_STRING s)))])) :: restil
++ when (match unrollType bt with
++ TInt((IChar|IUChar|ISChar), _) -> true
++ | TInt _ ->
++ (*Base type is a scalar other than char. Maybe a wchar_t?*)
++ E.s (error "Using a string literal to initialize something other than a character array.\n")
++ | _ -> false (* OK, this is probably an array of strings. Handle *)
++ ) (* it with the other arrays below.*)
++ ->
++ let charinits =
++ let init c = A.NEXT_INIT, A.SINGLE_INIT(A.CONSTANT (A.CONST_CHAR [c]))
++ in
++ let collector =
++ (* ISO 6.7.8 para 14: final NUL added only if no size specified, or
++ * if there is room for it; btw, we can't rely on zero-init of
++ * globals, since this array might be a local variable *)
++ if ((isNone leno) or ((String.length s) < (integerArrayLength leno)))
++ then ref [init Int64.zero]
++ else ref []
++ in
++ for pos = String.length s - 1 downto 0 do
++ collector := init (Int64.of_int (Char.code (s.[pos]))) :: !collector
++ done;
++ !collector
++ in
++ (* Create a separate object for the array *)
++ let so' = makeSubobj so.host so.soTyp so.soOff in
++ (* Go inside the array *)
++ let leno = integerArrayLength leno in
++ so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
++ normalSubobj so';
++ let acc', initl' = doInit isconst setone so' acc charinits in
++ if initl' <> [] then
++ ignore (warn "Too many initializers for character array %t" whoami);
++ (* Advance past the array *)
++ advanceSubobj so;
++ (* Continue *)
++ let res = doInit isconst setone so acc' restil in
++ res
++
++ (* If we are at an array of WIDE characters and the initializer is a
++ * WIDE string literal (optionally enclosed in braces) then explore
++ * the WIDE string into characters *)
++ (* [weimer] Wed Jan 30 15:38:05 PST 2002
++ * Despite what the compiler says, this match case is used and it is
++ * important. *)
++ | TArray(bt, leno, _),
++ (A.NEXT_INIT,
++ (A.SINGLE_INIT(A.CONSTANT (A.CONST_WSTRING s)) |
++ A.COMPOUND_INIT
++ [(A.NEXT_INIT,
++ A.SINGLE_INIT(A.CONSTANT
++ (A.CONST_WSTRING s)))])) :: restil
++ when(let bt' = unrollType bt in
++ match bt' with
++ (* compare bt to wchar_t, ignoring signed vs. unsigned *)
++ TInt _ when (bitsSizeOf bt') = (bitsSizeOf !wcharType) -> true
++ | TInt _ ->
++ (*Base type is a scalar other than wchar_t. Maybe a char?*)
++ E.s (error "Using a wide string literal to initialize something other than a wchar_t array.\n")
++ | _ -> false (* OK, this is probably an array of strings. Handle *)
++ ) (* it with the other arrays below.*)
++ ->
++ let maxWChar = (* (2**(bitsSizeOf !wcharType)) - 1 *)
++ Int64.sub (Int64.shift_left Int64.one (bitsSizeOf !wcharType))
++ Int64.one in
++ let charinits =
++ let init c =
++ if (compare c maxWChar > 0) then (* if c > maxWChar *)
++ E.s (error "cab2cil:doInit:character 0x%Lx too big." c);
++ A.NEXT_INIT,
++ A.SINGLE_INIT(A.CONSTANT (A.CONST_INT (Int64.to_string c)))
++ in
++ (List.map init s) @
++ (
++ (* ISO 6.7.8 para 14: final NUL added only if no size specified, or
++ * if there is room for it; btw, we can't rely on zero-init of
++ * globals, since this array might be a local variable *)
++ if ((isNone leno) or ((List.length s) < (integerArrayLength leno)))
++ then [init Int64.zero]
++ else [])
++(*
++ List.map
++ (fun c ->
++ if (compare c maxWChar > 0) then (* if c > maxWChar *)
++ E.s (error "cab2cil:doInit:character 0x%Lx too big." c)
++ else
++ (A.NEXT_INIT,
++ A.SINGLE_INIT(A.CONSTANT (A.CONST_INT (Int64.to_string c)))))
++ s
++*)
++ in
++ (* Create a separate object for the array *)
++ let so' = makeSubobj so.host so.soTyp so.soOff in
++ (* Go inside the array *)
++ let leno = integerArrayLength leno in
++ so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
++ normalSubobj so';
++ let acc', initl' = doInit isconst setone so' acc charinits in
++ if initl' <> [] then
++ (* sm: see above regarding ISO 6.7.8 para 14, which is not implemented
++ * for wchar_t because, as far as I can tell, we don't even put in
++ * the automatic NUL (!) *)
++ ignore (warn "Too many initializers for wchar_t array %t" whoami);
++ (* Advance past the array *)
++ advanceSubobj so;
++ (* Continue *)
++ doInit isconst setone so acc' restil
++
++ (* If we are at an array and we see a single initializer then it must
++ * be one for the first element *)
++ | TArray(bt, leno, al), (A.NEXT_INIT, A.SINGLE_INIT oneinit) :: restil ->
++ (* Grab the length if there is one *)
++ let leno = integerArrayLength leno in
++ so.stack <- InArray(so.soOff, bt, leno, ref 0) :: so.stack;
++ normalSubobj so;
++ (* Start over with the fields *)
++ doInit isconst setone so acc allinitl
++
++ (* If we are at a composite and we see a single initializer of the same
++ * type as the composite then grab it all. If the type is not the same
++ * then we must go on and try to initialize the fields *)
++ | TComp (comp, _), (A.NEXT_INIT, A.SINGLE_INIT oneinit) :: restil ->
++ let se, oneinit', t' = doExp isconst oneinit (AExp None) in
++ if (match unrollType t' with
++ TComp (comp', _) when comp'.ckey = comp.ckey -> true
++ | _ -> false)
++ then begin
++ (* Initialize the whole struct *)
++ setone so.soOff oneinit';
++ (* Advance to the next subobject *)
++ advanceSubobj so;
++ doInit isconst setone so (acc @@ se) restil
++ end else begin (* Try to initialize fields *)
++ let toinit = fieldsToInit comp None in
++ so.stack <- InComp(so.soOff, comp, toinit) :: so.stack;
++ normalSubobj so;
++ doInit isconst setone so acc allinitl
++ end
++
++ (* A scalar with a single initializer *)
++ | _, (A.NEXT_INIT, A.SINGLE_INIT oneinit) :: restil ->
++ let se, oneinit', t' = doExp isconst oneinit (AExp(Some so.soTyp)) in
++(*
++ ignore (E.log "oneinit'=%a, t'=%a, so.soTyp=%a\n"
++ d_exp oneinit' d_type t' d_type so.soTyp);
++*)
++ setone so.soOff (if !insertImplicitCasts then
++ makeCastT oneinit' t' so.soTyp
++ else oneinit');
++ (* Move on *)
++ advanceSubobj so;
++ doInit isconst setone so (acc @@ se) restil
++
++
++ (* An array with a compound initializer. The initializer is for the
++ * array elements *)
++ | TArray (bt, leno, _), (A.NEXT_INIT, A.COMPOUND_INIT initl) :: restil ->
++ (* Create a separate object for the array *)
++ let so' = makeSubobj so.host so.soTyp so.soOff in
++ (* Go inside the array *)
++ let leno = integerArrayLength leno in
++ so'.stack <- [InArray(so'.curOff, bt, leno, ref 0)];
++ normalSubobj so';
++ let acc', initl' = doInit isconst setone so' acc initl in
++ if initl' <> [] then
++ ignore (warn "Too many initializers for array %t" whoami);
++ (* Advance past the array *)
++ advanceSubobj so;
++ (* Continue *)
++ let res = doInit isconst setone so acc' restil in
++ res
++
++ (* We have a designator that tells us to select the matching union field.
++ * This is to support a GCC extension *)
++ | TComp(ci, _), [(A.NEXT_INIT,
++ A.COMPOUND_INIT [(A.INFIELD_INIT ("___matching_field",
++ A.NEXT_INIT),
++ A.SINGLE_INIT oneinit)])]
++ when not ci.cstruct ->
++ (* Do the expression to find its type *)
++ let _, _, t' = doExp isconst oneinit (AExp None) in
++ let tsig = typeSigNoAttrs t' in
++ let rec findField = function
++ [] -> E.s (error "Cannot find matching union field in cast")
++ | fi :: rest
++ when Util.equals (typeSigNoAttrs fi.ftype) tsig
++ -> fi
++ | _ :: rest -> findField rest
++ in
++ let fi = findField ci.cfields in
++ (* Change the designator and redo *)
++ doInit isconst setone so acc [(A.INFIELD_INIT (fi.fname, A.NEXT_INIT),
++ A.SINGLE_INIT oneinit)]
++
++
++ (* A structure with a composite initializer. We initialize the fields*)
++ | TComp (comp, _), (A.NEXT_INIT, A.COMPOUND_INIT initl) :: restil ->
++ (* Create a separate subobject iterator *)
++ let so' = makeSubobj so.host so.soTyp so.soOff in
++ (* Go inside the comp *)
++ so'.stack <- [InComp(so'.curOff, comp, fieldsToInit comp None)];
++ normalSubobj so';
++ let acc', initl' = doInit isconst setone so' acc initl in
++ if initl' <> [] then
++ ignore (warn "Too many initializers for structure");
++ (* Advance past the structure *)
++ advanceSubobj so;
++ (* Continue *)
++ doInit isconst setone so acc' restil
++
++ (* A scalar with a initializer surrounded by braces *)
++ | _, (A.NEXT_INIT, A.COMPOUND_INIT [(A.NEXT_INIT,
++ A.SINGLE_INIT oneinit)]) :: restil ->
++ let se, oneinit', t' = doExp isconst oneinit (AExp(Some so.soTyp)) in
++ setone so.soOff (makeCastT oneinit' t' so.soTyp);
++ (* Move on *)
++ advanceSubobj so;
++ doInit isconst setone so (acc @@ se) restil
++
++ | t, (A.NEXT_INIT, _) :: _ ->
++ E.s (unimp "doInit: unexpected NEXT_INIT for %a\n" d_type t);
++
++ (* We have a designator *)
++ | _, (what, ie) :: restil when what != A.NEXT_INIT ->
++ (* Process a designator and position to the designated subobject *)
++ let rec addressSubobj
++ (so: subobj)
++ (what: A.initwhat)
++ (acc: chunk) : chunk =
++ (* Always start from the current element *)
++ so.stack <- []; so.eof <- false;
++ normalSubobj so;
++ let rec address (what: A.initwhat) (acc: chunk) : chunk =
++ match what with
++ A.NEXT_INIT -> acc
++ | A.INFIELD_INIT (fn, whatnext) -> begin
++ match unrollType so.soTyp with
++ TComp (comp, _) ->
++ let toinit = fieldsToInit comp (Some fn) in
++ so.stack <- InComp(so.soOff, comp, toinit) :: so.stack;
++ normalSubobj so;
++ address whatnext acc
++
++ | _ -> E.s (error "Field designator %s not in a struct " fn)
++ end
++
++ | A.ATINDEX_INIT(idx, whatnext) -> begin
++ match unrollType so.soTyp with
++ TArray (bt, leno, _) ->
++ let ilen = integerArrayLength leno in
++ let nextidx', doidx =
++ let (doidx, idxe', _) =
++ doExp true idx (AExp(Some intType)) in
++ match constFold true idxe', isNotEmpty doidx with
++ Const(CInt64(x, _, _)), false -> i64_to_int x, doidx
++ | _ -> E.s (error
++ "INDEX initialization designator is not a constant")
++ in
++ if nextidx' < 0 || nextidx' >= ilen then
++ E.s (error "INDEX designator is outside bounds");
++ so.stack <-
++ InArray(so.soOff, bt, ilen, ref nextidx') :: so.stack;
++ normalSubobj so;
++ address whatnext (acc @@ doidx)
++
++ | _ -> E.s (error "INDEX designator for a non-array")
++ end
++
++ | A.ATINDEXRANGE_INIT _ ->
++ E.s (bug "addressSubobj: INDEXRANGE")
++ in
++ address what acc
++ in
++ (* First expand the INDEXRANGE by making copies *)
++ let rec expandRange (top: A.initwhat -> A.initwhat) = function
++ | A.INFIELD_INIT (fn, whatnext) ->
++ expandRange (fun what -> top (A.INFIELD_INIT(fn, what))) whatnext
++ | A.ATINDEX_INIT (idx, whatnext) ->
++ expandRange (fun what -> top (A.ATINDEX_INIT(idx, what))) whatnext
++
++ | A.ATINDEXRANGE_INIT (idxs, idxe) ->
++ let (doidxs, idxs', _) =
++ doExp true idxs (AExp(Some intType)) in
++ let (doidxe, idxe', _) =
++ doExp true idxe (AExp(Some intType)) in
++ if isNotEmpty doidxs || isNotEmpty doidxe then
++ E.s (error "Range designators are not constants\n");
++ let first, last =
++ match constFold true idxs', constFold true idxe' with
++ Const(CInt64(s, _, _)),
++ Const(CInt64(e, _, _)) ->
++ i64_to_int s, i64_to_int e
++ | _ -> E.s (error
++ "INDEX_RANGE initialization designator is not a constant")
++ in
++ if first < 0 || first > last then
++ E.s (error
++ "start index larger than end index in range initializer");
++ let rec loop (i: int) =
++ if i > last then restil
++ else
++ (top (A.ATINDEX_INIT(A.CONSTANT(A.CONST_INT(string_of_int i)),
++ A.NEXT_INIT)), ie)
++ :: loop (i + 1)
++ in
++ doInit isconst setone so acc (loop first)
++
++ | A.NEXT_INIT -> (* We have not found any RANGE *)
++ let acc' = addressSubobj so what acc in
++ doInit isconst setone so acc'
++ ((A.NEXT_INIT, ie) :: restil)
++ in
++ expandRange (fun x -> x) what
++
++ | t, (what, ie) :: _ ->
++ E.s (bug "doInit: cases for t=%a" d_type t)
++
++
++(* Create and add to the file (if not already added) a global. Return the
++ * varinfo *)
++and createGlobal (specs : (typ * storage * bool * A.attribute list))
++ (((n,ndt,a,cloc), inite) : A.init_name) : varinfo =
++ try
++ if debugGlobal then
++ ignore (E.log "createGlobal: %s\n" n);
++ (* Make a first version of the varinfo *)
++ let vi = makeVarInfoCabs ~isformal:false
++ ~isglobal:true (convLoc cloc) specs (n,ndt,a) in
++ (* Add the variable to the environment before doing the initializer
++ * because it might refer to the variable itself *)
++ if isFunctionType vi.vtype then begin
++ if inite != A.NO_INIT then
++ E.s (error "Function declaration with initializer (%s)\n"
++ vi.vname);
++ (* sm: if it's a function prototype, and the storage class *)
++ (* isn't specified, make it 'extern'; this fixes a problem *)
++ (* with no-storage prototype and static definition *)
++ if vi.vstorage = NoStorage then
++ (*(trace "sm" (dprintf "adding extern to prototype of %s\n" n));*)
++ vi.vstorage <- Extern;
++ end;
++ let vi, alreadyInEnv = makeGlobalVarinfo (inite != A.NO_INIT) vi in
++(*
++ ignore (E.log "createGlobal %a: %s type=%a\n"
++ d_loc (convLoc cloc) vi.vname d_plaintype vi.vtype);
++*)
++ (* Do the initializer and complete the array type if necessary *)
++ let init : init option =
++ if inite = A.NO_INIT then
++ None
++ else
++ let se, ie', et = doInitializer vi inite in
++ (* Maybe we now have a better type? Use the type of the
++ * initializer only if it really differs from the type of
++ * the variable. *)
++ if unrollType vi.vtype != unrollType et then
++ vi.vtype <- et;
++ if isNotEmpty se then
++ E.s (error "global initializer");
++ Some ie'
++ in
++
++ try
++ let oldloc = H.find alreadyDefined vi.vname in
++ if init != None then begin
++ E.s (error "Global %s was already defined at %a\n"
++ vi.vname d_loc oldloc);
++ end;
++ if debugGlobal then
++ ignore (E.log " global %s was already defined\n" vi.vname);
++ (* Do not declare it again *)
++ vi
++ with Not_found -> begin
++ (* Not already defined *)
++ if debugGlobal then
++ ignore (E.log " first definition for %s\n" vi.vname);
++ if init != None then begin
++ (* weimer: Sat Dec 8 17:43:34 2001
++ * MSVC NT Kernel headers include this lovely line:
++ * extern const GUID __declspec(selectany) \
++ * MOUNTDEV_MOUNTED_DEVICE_GUID = { 0x53f5630d, 0xb6bf, 0x11d0, { \
++ * 0x94, 0xf2, 0x00, 0xa0, 0xc9, 0x1e, 0xfb, 0x8b } };
++ * So we allow "extern" + "initializer" if "const" is
++ * around. *)
++ (* sm: As I read the ISO spec, in particular 6.9.2 and 6.7.8,
++ * "extern int foo = 3" is exactly equivalent to "int foo = 3";
++ * that is, if you put an initializer, then it is a definition,
++ * and "extern" is redundantly giving the name external linkage.
++ * gcc emits a warning, I guess because it is contrary to
++ * usual practice, but I think CIL warnings should be about
++ * semantic rather than stylistic issues, so I see no reason to
++ * even emit a warning. *)
++ if vi.vstorage = Extern then
++ vi.vstorage <- NoStorage; (* equivalent and canonical *)
++
++ H.add alreadyDefined vi.vname !currentLoc;
++ IH.remove mustTurnIntoDef vi.vid;
++ cabsPushGlobal (GVar(vi, {init = init}, !currentLoc));
++ vi
++ end else begin
++ if not (isFunctionType vi.vtype)
++ && not (IH.mem mustTurnIntoDef vi.vid) then
++ begin
++ IH.add mustTurnIntoDef vi.vid true
++ end;
++ if not alreadyInEnv then begin (* Only one declaration *)
++ (* If it has function type it is a prototype *)
++ cabsPushGlobal (GVarDecl (vi, !currentLoc));
++ vi
++ end else begin
++ if debugGlobal then
++ ignore (E.log " already in env %s\n" vi.vname);
++ vi
++ end
++ end
++ end
++ with e when continueOnError -> begin
++ ignore (E.log "error in createGlobal(%s: %a): %s\n" n
++ d_loc !currentLoc
++ (Printexc.to_string e));
++ cabsPushGlobal (dGlobal (dprintf "booo - error in global %s (%t)"
++ n d_thisloc) !currentLoc);
++ dummyFunDec.svar
++ end
++(*
++ ignore (E.log "Env after processing global %s is:@!%t@!"
++ n docEnv);
++ ignore (E.log "Alpha after processing global %s is:@!%t@!"
++ n docAlphaTable)
++*)
++
++(* Must catch the Static local variables. Make them global *)
++and createLocal ((_, sto, _, _) as specs)
++ ((((n, ndt, a, cloc) : A.name),
++ (inite: A.init_expression)) as init_name)
++ : chunk =
++ let loc = convLoc cloc in
++ (* Check if we are declaring a function *)
++ let rec isProto (dt: decl_type) : bool =
++ match dt with
++ | PROTO (JUSTBASE, _, _) -> true
++ | PROTO (x, _, _) -> isProto x
++ | PARENTYPE (_, x, _) -> isProto x
++ | ARRAY (x, _, _) -> isProto x
++ | PTR (_, x) -> isProto x
++ | _ -> false
++ in
++ match ndt with
++ (* Maybe we have a function prototype in local scope. Make it global. We
++ * do this even if the storage is Static *)
++ | _ when isProto ndt ->
++ let vi = createGlobal specs init_name in
++ (* Add it to the environment to shadow previous decls *)
++ addLocalToEnv n (EnvVar vi);
++ empty
++
++ | _ when sto = Static ->
++ if debugGlobal then
++ ignore (E.log "createGlobal (local static): %s\n" n);
++
++
++ (* Now alpha convert it to make sure that it does not conflict with
++ * existing globals or locals from this function. *)
++ let newname, _ = newAlphaName true "" n in
++ (* Make it global *)
++ let vi = makeVarInfoCabs ~isformal:false
++ ~isglobal:true
++ loc specs (newname, ndt, a) in
++ (* However, we have a problem if a real global appears later with the
++ * name that we have happened to choose for this one. Remember these names
++ * for later. *)
++ H.add staticLocals vi.vname vi;
++ (* Add it to the environment as a local so that the name goes out of
++ * scope properly *)
++ addLocalToEnv n (EnvVar vi);
++
++ (* Maybe this is an array whose length depends on something with local
++ scope, e.g. "static char device[ sizeof(local) ]".
++ Const-fold the type to fix this. *)
++ vi.vtype <- constFoldType vi.vtype;
++
++ let init : init option =
++ if inite = A.NO_INIT then
++ None
++ else begin
++ let se, ie', et = doInitializer vi inite in
++ (* Maybe we now have a better type? Use the type of the
++ * initializer only if it really differs from the type of
++ * the variable. *)
++ if unrollType vi.vtype != unrollType et then
++ vi.vtype <- et;
++ if isNotEmpty se then
++ E.s (error "global static initializer");
++ (* Maybe the initializer refers to the function itself.
++ Push a prototype for the function, just in case. Hopefully,
++ if does not refer to the locals *)
++ cabsPushGlobal (GVarDecl (!currentFunctionFDEC.svar, !currentLoc));
++ Some ie'
++ end
++ in
++ cabsPushGlobal (GVar(vi, {init = init}, !currentLoc));
++ empty
++
++ (* Maybe we have an extern declaration. Make it a global *)
++ | _ when sto = Extern ->
++ let vi = createGlobal specs init_name in
++ (* Add it to the local environment to ensure that it shadows previous
++ * local variables *)
++ addLocalToEnv n (EnvVar vi);
++ empty
++
++ | _ ->
++ (* Make a variable of potentially variable size. If se0 <> empty then
++ * it is a variable size variable *)
++ let vi,se0,len,isvarsize =
++ makeVarSizeVarInfo loc specs (n, ndt, a) in
++
++ let vi = alphaConvertVarAndAddToEnv true vi in (* Replace vi *)
++ let se1 =
++ if isvarsize then begin (* Variable-sized array *)
++ ignore (warn "Variable-sized local variable %s" vi.vname);
++ (* Make a local variable to keep the length *)
++ let savelen =
++ makeVarInfoCabs
++ ~isformal:false
++ ~isglobal:false
++ loc
++ (!typeOfSizeOf, NoStorage, false, [])
++ ("__lengthof" ^ vi.vname,JUSTBASE, [])
++ in
++ (* Register it *)
++ let savelen = alphaConvertVarAndAddToEnv true savelen in
++ (* Compute the sizeof *)
++ let sizeof =
++ BinOp(Mult,
++ SizeOfE (Lval(Mem(Lval(var vi)), NoOffset)),
++ Lval (var savelen), !typeOfSizeOf) in
++ (* Register the length *)
++ IH.add varSizeArrays vi.vid sizeof;
++ (* There can be no initializer for this *)
++ if inite != A.NO_INIT then
++ E.s (error "Variable-sized array cannot have initializer");
++ let setlen = se0 +++
++ (Set(var savelen, makeCast len savelen.vtype, !currentLoc)) in
++ (* Initialize the variable *)
++ let alloca: varinfo = allocaFun () in
++ if !doCollapseCallCast then
++ (* do it in one step *)
++ setlen +++ (Call(Some(var vi), Lval(var alloca),
++ [ sizeof ], !currentLoc))
++ else begin
++ (* do it in two *)
++ let rt, _, _, _ = splitFunctionType alloca.vtype in
++ let tmp = newTempVar (dprintf "alloca(%a)" d_exp sizeof) false rt in
++ setlen
++ +++ (Call(Some(var tmp), Lval(var alloca),
++ [ sizeof ], !currentLoc))
++ +++ (Set((var vi),
++ makeCast (Lval(var tmp)) vi.vtype, !currentLoc))
++ end
++ end else empty
++ in
++ if inite = A.NO_INIT then
++ se1 (* skipChunk *)
++ else begin
++ let se4, ie', et = doInitializer vi inite in
++ (* Fix the length *)
++ (match vi.vtype, ie', et with
++ (* We have a length now *)
++ TArray(_,None, _), _, TArray(_, Some _, _) -> vi.vtype <- et
++ (* Initializing a local array *)
++ | TArray(TInt((IChar|IUChar|ISChar), _) as bt, None, a),
++ SingleInit(Const(CStr s)), _ ->
++ vi.vtype <- TArray(bt,
++ Some (integer (String.length s + 1)),
++ a)
++ | _, _, _ -> ());
++
++ (* Now create assignments instead of the initialization *)
++ se1 @@ se4 @@ (assignInit (Var vi, NoOffset) ie' et empty)
++ end
++
++and doAliasFun vtype (thisname:string) (othername:string)
++ (sname:single_name) (loc: cabsloc) : unit =
++ (* This prototype declares that name is an alias for
++ othername, which must be defined in this file *)
++(* E.log "%s is alias for %s at %a\n" thisname othername *)
++(* d_loc !currentLoc; *)
++ let rt, formals, isva, _ = splitFunctionType vtype in
++ if isva then E.s (error "%a: alias unsupported with varargs."
++ d_loc !currentLoc);
++ let args = List.map
++ (fun (n,_,_) -> A.VARIABLE n)
++ (argsToList formals) in
++ let call = A.CALL (A.VARIABLE othername, args) in
++ let stmt = if isVoidType rt then A.COMPUTATION(call, loc)
++ else A.RETURN(call, loc)
++ in
++ let body = { A.blabels = []; A.battrs = []; A.bstmts = [stmt] } in
++ let fdef = A.FUNDEF (sname, body, loc, loc) in
++ ignore (doDecl true fdef);
++ (* get the new function *)
++ let v,_ = try lookupGlobalVar thisname
++ with Not_found -> E.s (bug "error in doDecl") in
++ v.vattr <- dropAttribute "alias" v.vattr
++
++
++(* Do one declaration *)
++and doDecl (isglobal: bool) : A.definition -> chunk = function
++ | A.DECDEF ((s, nl), loc) ->
++ currentLoc := convLoc(loc);
++ (* Do the specifiers exactly once *)
++ let sugg =
++ match nl with
++ [] -> ""
++ | ((n, _, _, _), _) :: _ -> n
++ in
++ let spec_res = doSpecList sugg s in
++ (* Do all the variables and concatenate the resulting statements *)
++ let doOneDeclarator (acc: chunk) (name: init_name) =
++ let (n,ndt,a,l),_ = name in
++ if isglobal then begin
++ let bt,_,_,attrs = spec_res in
++ let vtype, nattr =
++ doType (AttrName false) bt (A.PARENTYPE(attrs, ndt, a)) in
++ (match filterAttributes "alias" nattr with
++ [] -> (* ordinary prototype. *)
++ ignore (createGlobal spec_res name)
++ (* E.log "%s is not aliased\n" name *)
++ | [Attr("alias", [AStr othername])] ->
++ if not (isFunctionType vtype) then begin
++ ignore (warn
++ "%a: CIL only supports attribute((alias)) for functions.\n"
++ d_loc !currentLoc);
++ ignore (createGlobal spec_res name)
++ end else
++ doAliasFun vtype n othername (s, (n,ndt,a,l)) loc
++ | _ -> E.s (error "Bad alias attribute at %a" d_loc !currentLoc));
++ acc
++ end else
++ acc @@ createLocal spec_res name
++ in
++ let res = List.fold_left doOneDeclarator empty nl in
++(*
++ ignore (E.log "after doDecl %a: res=%a\n"
++ d_loc !currentLoc d_chunk res);
++*)
++ res
++
++
++
++ | A.TYPEDEF (ng, loc) ->
++ currentLoc := convLoc(loc);
++ doTypedef ng; empty
++
++ | A.ONLYTYPEDEF (s, loc) ->
++ currentLoc := convLoc(loc);
++ doOnlyTypedef s; empty
++
++ | A.GLOBASM (s,loc) when isglobal ->
++ currentLoc := convLoc(loc);
++ cabsPushGlobal (GAsm (s, !currentLoc));
++ empty
++
++ | A.PRAGMA (a, loc) when isglobal -> begin
++ currentLoc := convLoc(loc);
++ match doAttr ("dummy", [a]) with
++ [Attr("dummy", [a'])] ->
++ let a'' =
++ match a' with
++ | ACons (s, args) -> Attr (s, args)
++ | _ -> E.s (error "Unexpected attribute in #pragma")
++ in
++ cabsPushGlobal (GPragma (a'', !currentLoc));
++ empty
++
++ | _ -> E.s (error "Too many attributes in pragma")
++ end
++ | A.TRANSFORMER (_, _, _) -> E.s (E.bug "TRANSFORMER in cabs2cil input")
++ | A.EXPRTRANSFORMER (_, _, _) ->
++ E.s (E.bug "EXPRTRANSFORMER in cabs2cil input")
++
++ (* If there are multiple definitions of extern inline, turn all but the
++ * first into a prototype *)
++ | A.FUNDEF (((specs,(n,dt,a,loc')) : A.single_name),
++ (body : A.block), loc, _)
++ when isglobal && isExtern specs && isInline specs
++ && (H.mem genv (n ^ "__extinline")) ->
++ currentLoc := convLoc(loc);
++ let othervi, _ = lookupVar (n ^ "__extinline") in
++ if othervi.vname = n then
++ (* The previous entry in the env is also an extern inline version
++ of n. *)
++ ignore (warn "Duplicate extern inline definition for %s ignored" n)
++ else begin
++ (* Otherwise, the previous entry is an ordinary function that
++ happens to be named __extinline. Renaming n to n__extinline
++ would confict with other, so report an error. *)
++ E.s (unimp("Trying to rename %s to\n %s__extinline, but %s__extinline"
++ ^^ " already exists in the env.\n \"__extinline\" is"
++ ^^ " reserved for CIL.\n") n n n)
++ end;
++ (* Treat it as a prototype *)
++ doDecl isglobal (A.DECDEF ((specs, [((n,dt,a,loc'), A.NO_INIT)]), loc))
++
++ | A.FUNDEF (((specs,(n,dt,a, _)) : A.single_name),
++ (body : A.block), loc1, loc2) when isglobal ->
++ begin
++ let funloc = convLoc loc1 in
++ let endloc = convLoc loc2 in
++(* ignore (E.log "Definition of %s at %a\n" n d_loc funloc); *)
++ currentLoc := funloc;
++ E.withContext
++ (fun _ -> dprintf "2cil: %s" n)
++ (fun _ ->
++ try
++ IH.clear callTempVars;
++
++ (* Make the fundec right away, and we'll populate it later. We
++ * need this throughout the code to create temporaries. *)
++ currentFunctionFDEC :=
++ { svar = makeGlobalVar "@tempname@" voidType;
++ slocals = []; (* For now we'll put here both the locals and
++ * the formals. Then "endFunction" will
++ * separate them *)
++ sformals = []; (* Not final yet *)
++ smaxid = 0;
++ sbody = dummyFunDec.sbody; (* Not final yet *)
++ smaxstmtid = None;
++ sallstmts = [];
++ };
++ !currentFunctionFDEC.svar.vdecl <- funloc;
++
++ constrExprId := 0;
++ (* Setup the environment. Add the formals to the locals. Maybe
++ * they need alpha-conv *)
++ enterScope (); (* Start the scope *)
++
++ IH.clear varSizeArrays;
++
++ (* Do not process transparent unions in function definitions.
++ * We'll do it later *)
++ transparentUnionArgs := [];
++
++ (* Fix the NAME and the STORAGE *)
++ let _ =
++ let bt,sto,inl,attrs = doSpecList n specs in
++ !currentFunctionFDEC.svar.vinline <- inl;
++
++ let ftyp, funattr =
++ doType (AttrName false) bt (A.PARENTYPE(attrs, dt, a)) in
++ !currentFunctionFDEC.svar.vtype <- ftyp;
++ !currentFunctionFDEC.svar.vattr <- funattr;
++
++ (* If this is the definition of an extern inline then we change
++ * its name, by adding the suffix __extinline. We also make it
++ * static *)
++ let n', sto' =
++ let n' = n ^ "__extinline" in
++ if inl && sto = Extern then begin
++ n', Static
++ end else begin
++ (* Maybe this is the body of a previous extern inline. Then
++ * we must take that one out of the environment because it
++ * is not used from here on. This will also ensure that
++ * then we make this functions' varinfo we will not think
++ * it is a duplicate definition *)
++ (try
++ ignore (lookupVar n'); (* if this succeeds, n' is defined*)
++ let oldvi, _ = lookupVar n in
++ if oldvi.vname = n' then begin
++ (* oldvi is an extern inline function that has been
++ renamed to n ^ "__extinline". Remove it from the
++ environment. *)
++ H.remove env n; H.remove genv n;
++ H.remove env n'; H.remove genv n'
++ end
++ else
++ (* oldvi is not a renamed extern inline function, and
++ we should do nothing. The reason the lookup
++ of n' succeeded is probably because there's
++ an ordinary function that happens to be named,
++ n ^ "__extinline", probably as a result of a previous
++ pass through CIL. See small2/extinline.c*)
++ ()
++ with Not_found -> ());
++ n, sto
++ end
++ in
++ (* Now we have the name and the storage *)
++ !currentFunctionFDEC.svar.vname <- n';
++ !currentFunctionFDEC.svar.vstorage <- sto'
++ in
++
++ (* Add the function itself to the environment. Add it before
++ * you do the body because the function might be recursive. Add
++ * it also before you add the formals to the environment
++ * because there might be a formal with the same name as the
++ * function and we want it to take precedence. *)
++ (* Make a variable out of it and put it in the environment *)
++ !currentFunctionFDEC.svar <-
++ fst (makeGlobalVarinfo true !currentFunctionFDEC.svar);
++
++ (* If it is extern inline then we add it to the global
++ * environment for the original name as well. This will ensure
++ * that all uses of this function will refer to the renamed
++ * function *)
++ addGlobalToEnv n (EnvVar !currentFunctionFDEC.svar);
++
++ if H.mem alreadyDefined !currentFunctionFDEC.svar.vname then
++ E.s (error "There is a definition already for %s" n);
++
++ H.add alreadyDefined !currentFunctionFDEC.svar.vname funloc;
++
++
++(*
++ ignore (E.log "makefunvar:%s@! type=%a@! vattr=%a@!"
++ n d_type thisFunctionVI.vtype
++ d_attrlist thisFunctionVI.vattr);
++*)
++
++ (* makeGlobalVarinfo might have changed the type of the function
++ * (when combining it with the type of the prototype). So get the
++ * type only now. *)
++
++ (**** Process the TYPE and the FORMALS ***)
++ let _ =
++ let (returnType, formals_t, isvararg, funta) =
++ splitFunctionTypeVI !currentFunctionFDEC.svar
++ in
++ (* Record the returnType for doStatement *)
++ currentReturnType := returnType;
++
++
++ (* Create the formals and add them to the environment. *)
++ (* sfg: extract locations for the formals from dt *)
++ let doFormal (loc : location) (fn, ft, fa) =
++ let f = makeVarinfo false fn ft in
++ (f.vdecl <- loc;
++ f.vattr <- fa;
++ alphaConvertVarAndAddToEnv true f)
++ in
++ let rec doFormals fl' ll' =
++ begin
++ match (fl', ll') with
++ | [], _ -> []
++
++ | fl, [] -> (* no more locs available *)
++ List.map (doFormal !currentLoc) fl
++
++ | f::fl, (_,(_,_,_,l))::ll ->
++ (* sfg: these lets seem to be necessary to
++ * force the right order of evaluation *)
++ let f' = doFormal (convLoc l) f in
++ let fl' = doFormals fl ll in
++ f' :: fl'
++ end
++ in
++ let fmlocs = (match dt with PROTO(_, fml, _) -> fml | _ -> []) in
++ let formals = doFormals (argsToList formals_t) fmlocs in
++
++ (* Recreate the type based on the formals. *)
++ let ftype = TFun(returnType,
++ Some (List.map (fun f -> (f.vname,
++ f.vtype,
++ f.vattr)) formals),
++ isvararg, funta) in
++ (*
++ ignore (E.log "Funtype of %s: %a\n" n' d_type ftype);
++ *)
++ (* Now fix the names of the formals in the type of the function
++ * as well *)
++ !currentFunctionFDEC.svar.vtype <- ftype;
++ !currentFunctionFDEC.sformals <- formals;
++ in
++ (* Now change the type of transparent union args back to what it
++ * was so that the body type checks. We must do it this late
++ * because makeGlobalVarinfo from above might choke if we give
++ * the function a type containing transparent unions *)
++ let _ =
++ let rec fixbackFormals (idx: int) (args: varinfo list) : unit=
++ match args with
++ [] -> ()
++ | a :: args' ->
++ (* Fix the type back to a transparent union type *)
++ (try
++ let origtype = List.assq idx !transparentUnionArgs in
++ a.vtype <- origtype;
++ with Not_found -> ());
++ fixbackFormals (idx + 1) args'
++ in
++ fixbackFormals 0 !currentFunctionFDEC.sformals;
++ transparentUnionArgs := [];
++ in
++
++ (********** Now do the BODY *************)
++ let _ =
++ let stmts = doBody body in
++ (* Finish everything *)
++ exitScope ();
++
++ (* Now fill in the computed goto statement with cases. Do this
++ * before mkFunctionbody which resolves the gotos *)
++ (match !gotoTargetData with
++ Some (switchv, switch) ->
++ let switche, l =
++ match switch.skind with
++ Switch (switche, _, _, l) -> switche, l
++ | _ -> E.s(bug "the computed goto statement not a switch")
++ in
++ (* Build a default chunk that segfaults *)
++ let default =
++ defaultChunk
++ l
++ (i2c (Set ((Mem (makeCast (integer 0) intPtrType),
++ NoOffset),
++ integer 0, l)))
++ in
++ let bodychunk = ref default in
++ H.iter (fun lname laddr ->
++ bodychunk :=
++ caseRangeChunk
++ [integer laddr] l
++ (gotoChunk lname l @@ !bodychunk))
++ gotoTargetHash;
++ (* Now recreate the switch *)
++ let newswitch = switchChunk switche !bodychunk l in
++ (* We must still share the old switch statement since we
++ * have already inserted the goto's *)
++ let newswitchkind =
++ match newswitch.stmts with
++ [ s]
++ when newswitch.postins == [] && newswitch.cases == []->
++ s.skind
++ | _ -> E.s (bug "Unexpected result from switchChunk")
++ in
++ switch.skind <- newswitchkind
++
++ | None -> ());
++ (* Now finish the body and store it *)
++ !currentFunctionFDEC.sbody <- mkFunctionBody stmts;
++ (* Reset the global parameters *)
++ gotoTargetData := None;
++ H.clear gotoTargetHash;
++ gotoTargetNextAddr := 0;
++ in
++
++
++
++(*
++ ignore (E.log "endFunction %s at %t:@! sformals=%a@! slocals=%a@!"
++ !currentFunctionFDEC.svar.vname d_thisloc
++ (docList ~sep:(chr ',') (fun v -> text v.vname))
++ !currentFunctionFDEC.sformals
++ (docList ~sep:(chr ',') (fun v -> text v.vname))
++ !currentFunctionFDEC.slocals);
++*)
++
++ let rec dropFormals formals locals =
++ match formals, locals with
++ [], l -> l
++ | f :: formals, l :: locals ->
++ if f != l then
++ E.s (bug "formal %s is not in locals (found instead %s)"
++ f.vname l.vname);
++ dropFormals formals locals
++ | _ -> E.s (bug "Too few locals")
++ in
++ !currentFunctionFDEC.slocals
++ <- dropFormals !currentFunctionFDEC.sformals
++ (List.rev !currentFunctionFDEC.slocals);
++ setMaxId !currentFunctionFDEC;
++
++ (* Now go over the types of the formals and pull out the formals
++ * with transparent union type. Replace them with some shadow
++ * parameters and then add assignments *)
++ let _ =
++ let newformals, newbody =
++ List.fold_right (* So that the formals come out in order *)
++ (fun f (accform, accbody) ->
++ match isTransparentUnion f.vtype with
++ None -> (f :: accform, accbody)
++ | Some fstfield ->
++ (* A new shadow to be placed in the formals. Use
++ * makeTempVar to update smaxid and all others. *)
++ let shadow =
++ makeTempVar !currentFunctionFDEC fstfield.ftype in
++ (* Now take it out of the locals and replace it with
++ * the current formal. It is not worth optimizing this
++ * one. *)
++ !currentFunctionFDEC.slocals <-
++ f ::
++ (List.filter (fun x -> x.vid <> shadow.vid)
++ !currentFunctionFDEC.slocals);
++ (shadow :: accform,
++ mkStmt (Instr [Set ((Var f, Field(fstfield,
++ NoOffset)),
++ Lval (var shadow),
++ !currentLoc)]) :: accbody))
++ !currentFunctionFDEC.sformals
++ ([], !currentFunctionFDEC.sbody.bstmts)
++ in
++ !currentFunctionFDEC.sbody.bstmts <- newbody;
++ (* To make sure sharing with the type is proper *)
++ setFormals !currentFunctionFDEC newformals;
++ in
++
++ (* Now see whether we can fall through to the end of the function
++ * *)
++ (* weimer: Sat Dec 8 17:30:47 2001 MSVC NT kernel headers include
++ * functions like long convert(x) { __asm { mov eax, x \n cdq } }
++ * That set a return value via an ASM statement. As a result, I
++ * am changing this so a final ASM statement does not count as
++ * "fall through" for the purposes of this warning. *)
++ (* matth: But it's better to assume assembly will fall through,
++ * since most such blocks do. It's probably better to print an
++ * unnecessary warning than to break CIL's invariant that
++ * return statements are inserted properly. *)
++ let instrFallsThrough (i : instr) = match i with
++ Set _ -> true
++ | Call (None, Lval (Var e, NoOffset), _, _) ->
++ (* See if this is exit, or if it has the noreturn attribute *)
++ if e.vname = "exit" then false
++ else if hasAttribute "noreturn" e.vattr then false
++ else true
++ | Call _ -> true
++ | Asm _ -> true
++ in
++ let rec stmtFallsThrough (s: stmt) : bool =
++ match s.skind with
++ Instr(il) ->
++ List.fold_left (fun acc elt ->
++ acc && instrFallsThrough elt) true il
++ | Return _ | Break _ | Continue _ -> false
++ | Goto _ -> false
++ | If (_, b1, b2, _) ->
++ blockFallsThrough b1 || blockFallsThrough b2
++ | Switch (e, b, targets, _) ->
++ (* See if there is a "default" case *)
++ if not
++ (List.exists (fun s ->
++ List.exists (function Default _ -> true | _ -> false)
++ s.labels)
++ targets) then begin
++(*
++ ignore (E.log "Switch falls through because no default");
++
++*) true (* We fall through because there is no default *)
++ end else begin
++ (* We must examine all cases. If any falls through,
++ * then the switch falls through. *)
++ blockFallsThrough b || blockCanBreak b
++ end
++ | Loop (b, _, _, _) ->
++ (* A loop falls through if it can break. *)
++ blockCanBreak b
++ | Block b -> blockFallsThrough b
++ | TryFinally (b, h, _) -> blockFallsThrough h
++ | TryExcept (b, _, h, _) -> true (* Conservative *)
++ and blockFallsThrough b =
++ let rec fall = function
++ [] -> true
++ | s :: rest ->
++ if stmtFallsThrough s then begin
++(*
++ ignore (E.log "Stmt %a falls through\n" d_stmt s);
++*)
++ fall rest
++ end else begin
++(*
++ ignore (E.log "Stmt %a DOES NOT fall through\n"
++ d_stmt s);
++*)
++ (* If we are not falling thorough then maybe there
++ * are labels who are *)
++ labels rest
++ end
++ and labels = function
++ [] -> false
++ (* We have a label, perhaps we can jump here *)
++ | s :: rest when s.labels <> [] ->
++(*
++ ignore (E.log "invoking fall %a: %a\n"
++ d_loc !currentLoc d_stmt s);
++*)
++ fall (s :: rest)
++ | _ :: rest -> labels rest
++ in
++ let res = fall b.bstmts in
++(*
++ ignore (E.log "blockFallsThrough=%b %a\n" res d_block b);
++*)
++ res
++ (* will we leave this statement or block with a break command? *)
++ and stmtCanBreak (s: stmt) : bool =
++ match s.skind with
++ Instr _ | Return _ | Continue _ | Goto _ -> false
++ | Break _ -> true
++ | If (_, b1, b2, _) ->
++ blockCanBreak b1 || blockCanBreak b2
++ | Switch _ | Loop _ ->
++ (* switches and loops catch any breaks in their bodies *)
++ false
++ | Block b -> blockCanBreak b
++ | TryFinally (b, h, _) -> blockCanBreak b || blockCanBreak h
++ | TryExcept (b, _, h, _) -> blockCanBreak b || blockCanBreak h
++ and blockCanBreak b =
++ List.exists stmtCanBreak b.bstmts
++ in
++ if blockFallsThrough !currentFunctionFDEC.sbody then begin
++ let retval =
++ match unrollType !currentReturnType with
++ TVoid _ -> None
++ | (TInt _ | TEnum _ | TFloat _ | TPtr _) as rt ->
++ ignore (warn "Body of function %s falls-through. Adding a return statement\n" !currentFunctionFDEC.svar.vname);
++ Some (makeCastT zero intType rt)
++ | _ ->
++ ignore (warn "Body of function %s falls-through and cannot find an appropriate return value\n" !currentFunctionFDEC.svar.vname);
++ None
++ in
++ if not (hasAttribute "noreturn"
++ !currentFunctionFDEC.svar.vattr) then
++ !currentFunctionFDEC.sbody.bstmts <-
++ !currentFunctionFDEC.sbody.bstmts
++ @ [mkStmt (Return(retval, endloc))]
++ end;
++
++ (* ignore (E.log "The env after finishing the body of %s:\n%t\n"
++ n docEnv); *)
++ cabsPushGlobal (GFun (!currentFunctionFDEC, funloc));
++ empty
++ with e when continueOnError -> begin
++ ignore (E.log "error in collectFunction %s: %s\n"
++ n (Printexc.to_string e));
++ cabsPushGlobal (GAsm("error in function " ^ n, !currentLoc));
++ empty
++ end)
++ () (* argument of E.withContext *)
++ end (* FUNDEF *)
++
++ | LINKAGE (n, loc, dl) ->
++ currentLoc := convLoc loc;
++ if n <> "C" then
++ ignore (warn "Encountered linkage specification \"%s\"" n);
++ if not isglobal then
++ E.s (error "Encountered linkage specification in local scope");
++ (* For now drop the linkage on the floor !!! *)
++ List.iter
++ (fun d ->
++ let s = doDecl isglobal d in
++ if isNotEmpty s then
++ E.s (bug "doDecl returns non-empty statement for global"))
++ dl;
++ empty
++
++ | _ -> E.s (error "unexpected form of declaration")
++
++and doTypedef ((specs, nl): A.name_group) =
++ try
++ (* Do the specifiers exactly once *)
++ let bt, sto, inl, attrs = doSpecList (suggestAnonName nl) specs in
++ if sto <> NoStorage || inl then
++ E.s (error "Storage or inline specifier not allowed in typedef");
++ let createTypedef ((n,ndt,a,loc) : A.name) =
++ (* E.s (error "doTypeDef") *)
++ try
++ let newTyp, tattr =
++ doType AttrType bt (A.PARENTYPE(attrs, ndt, a)) in
++ let newTyp' = cabsTypeAddAttributes tattr newTyp in
++ (* Create a new name for the type. Use the same name space as that of
++ * variables to avoid confusion between variable names and types. This
++ * is actually necessary in some cases. *)
++ let n', _ = newAlphaName true "" n in
++ let ti = { tname = n'; ttype = newTyp'; treferenced = false } in
++ (* Since we use the same name space, we might later hit a global with
++ * the same name and we would want to change the name of the global.
++ * It is better to change the name of the type instead. So, remember
++ * all types whose names have changed *)
++ H.add typedefs n' ti;
++ let namedTyp = TNamed(ti, []) in
++ (* Register the type. register it as local because we might be in a
++ * local context *)
++ addLocalToEnv (kindPlusName "type" n) (EnvTyp namedTyp);
++ cabsPushGlobal (GType (ti, !currentLoc))
++ with e -> begin
++ ignore (E.log "Error on A.TYPEDEF (%s)\n"
++ (Printexc.to_string e));
++ cabsPushGlobal (GAsm ("booo_typedef:" ^ n, !currentLoc))
++ end
++ in
++ List.iter createTypedef nl
++ with e -> begin
++ ignore (E.log "Error on A.TYPEDEF (%s)\n"
++ (Printexc.to_string e));
++ let fstname =
++ match nl with
++ [] -> "<missing name>"
++ | (n, _, _, _) :: _ -> n
++ in
++ cabsPushGlobal (GAsm ("booo_typedef: " ^ fstname, !currentLoc))
++ end
++
++and doOnlyTypedef (specs: A.spec_elem list) : unit =
++ try
++ let bt, sto, inl, attrs = doSpecList "" specs in
++ if sto <> NoStorage || inl then
++ E.s (error "Storage or inline specifier not allowed in typedef");
++ let restyp, nattr = doType AttrType bt (A.PARENTYPE(attrs,
++ A.JUSTBASE, [])) in
++ if nattr <> [] then
++ ignore (warn "Ignoring identifier attribute");
++ (* doSpec will register the type. *)
++ (* See if we are defining a composite or enumeration type, and in that
++ * case move the attributes from the defined type into the composite type
++ * *)
++ let isadef =
++ List.exists
++ (function
++ A.SpecType(A.Tstruct(_, Some _, _)) -> true
++ | A.SpecType(A.Tunion(_, Some _, _)) -> true
++ | A.SpecType(A.Tenum(_, Some _, _)) -> true
++ | _ -> false) specs
++ in
++ match restyp with
++ TComp(ci, al) ->
++ if isadef then begin
++ ci.cattr <- cabsAddAttributes ci.cattr al;
++ (* The GCompTag was already added *)
++ end else (* Add a GCompTagDecl *)
++ cabsPushGlobal (GCompTagDecl(ci, !currentLoc))
++ | TEnum(ei, al) ->
++ if isadef then begin
++ ei.eattr <- cabsAddAttributes ei.eattr al;
++ end else
++ cabsPushGlobal (GEnumTagDecl(ei, !currentLoc))
++ | _ ->
++ ignore (warn "Ignoring un-named typedef that does not introduce a struct or enumeration type\n")
++
++ with e -> begin
++ ignore (E.log "Error on A.ONLYTYPEDEF (%s)\n"
++ (Printexc.to_string e));
++ cabsPushGlobal (GAsm ("booo_typedef", !currentLoc))
++ end
++
++and assignInit (lv: lval)
++ (ie: init)
++ (iet: typ)
++ (acc: chunk) : chunk =
++ match ie with
++ SingleInit e ->
++ let (_, e'') = castTo iet (typeOfLval lv) e in
++ acc +++ (Set(lv, e'', !currentLoc))
++ | CompoundInit (t, initl) ->
++ foldLeftCompound
++ ~implicit:false
++ ~doinit:(fun off i it acc ->
++ assignInit (addOffsetLval off lv) i it acc)
++ ~ct:t
++ ~initl:initl
++ ~acc:acc
++
++ (* Now define the processors for body and statement *)
++and doBody (blk: A.block) : chunk =
++ enterScope ();
++ (* Rename the labels and add them to the environment *)
++ List.iter (fun l -> ignore (genNewLocalLabel l)) blk.blabels;
++ (* See if we have some attributes *)
++ let battrs = doAttributes blk.A.battrs in
++
++ let bodychunk =
++ afterConversion
++ (List.fold_left (* !!! @ evaluates its arguments backwards *)
++ (fun prev s -> let res = doStatement s in
++ prev @@ res)
++ empty
++ blk.A.bstmts)
++ in
++ exitScope ();
++
++
++ if battrs == [] then
++ bodychunk
++ else begin
++ let b = c2block bodychunk in
++ b.battrs <- battrs;
++ s2c (mkStmt (Block b))
++ end
++
++and doStatement (s : A.statement) : chunk =
++ try
++ match s with
++ A.NOP _ -> skipChunk
++ | A.COMPUTATION (e, loc) ->
++ currentLoc := convLoc loc;
++ let (lasts, data) = !gnu_body_result in
++ if lasts == s then begin (* This is the last in a GNU_BODY *)
++ let (s', e', t') = doExp false e (AExp None) in
++ data := Some (e', t'); (* Record the result *)
++ s'
++ end else
++ let (s', _, _) = doExp false e ADrop in
++ (* drop the side-effect free expression *)
++ (* And now do some peep-hole optimizations *)
++ s'
++
++ | A.BLOCK (b, loc) ->
++ currentLoc := convLoc loc;
++ doBody b
++
++ | A.SEQUENCE (s1, s2, loc) ->
++ (doStatement s1) @@ (doStatement s2)
++
++ | A.IF(e,st,sf,loc) ->
++ let st' = doStatement st in
++ let sf' = doStatement sf in
++ currentLoc := convLoc loc;
++ doCondition false e st' sf'
++
++ | A.WHILE(e,s,loc) ->
++ startLoop true;
++ let s' = doStatement s in
++ exitLoop ();
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ loopChunk ((doCondition false e skipChunk
++ (breakChunk loc'))
++ @@ s')
++
++ | A.DOWHILE(e,s,loc) ->
++ startLoop false;
++ let s' = doStatement s in
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ let s'' =
++ consLabContinue (doCondition false e skipChunk (breakChunk loc'))
++ in
++ exitLoop ();
++ loopChunk (s' @@ s'')
++
++ | A.FOR(fc1,e2,e3,s,loc) -> begin
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ enterScope (); (* Just in case we have a declaration *)
++ let (se1, _, _) =
++ match fc1 with
++ FC_EXP e1 -> doExp false e1 ADrop
++ | FC_DECL d1 -> (doDecl false d1, zero, voidType)
++ in
++ let (se3, _, _) = doExp false e3 ADrop in
++ startLoop false;
++ let s' = doStatement s in
++ currentLoc := loc';
++ let s'' = consLabContinue se3 in
++ exitLoop ();
++ let res =
++ match e2 with
++ A.NOTHING -> (* This means true *)
++ se1 @@ loopChunk (s' @@ s'')
++ | _ ->
++ se1 @@ loopChunk ((doCondition false e2 skipChunk (breakChunk loc'))
++ @@ s' @@ s'')
++ in
++ exitScope ();
++ res
++ end
++ | A.BREAK loc ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ breakChunk loc'
++
++ | A.CONTINUE loc ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ continueOrLabelChunk loc'
++
++ | A.RETURN (A.NOTHING, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ if not (isVoidType !currentReturnType) then
++ ignore (warn "Return statement without a value in function returning %a\n" d_type !currentReturnType);
++ returnChunk None loc'
++
++ | A.RETURN (e, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ (* Sometimes we return the result of a void function call *)
++ if isVoidType !currentReturnType then begin
++ ignore (warn "Return statement with a value in function returning void");
++ let (se, _, _) = doExp false e ADrop in
++ se @@ returnChunk None loc'
++ end else begin
++ let rt =
++ typeRemoveAttributes ["warn_unused_result"] !currentReturnType
++ in
++ let (se, e', et) = doExp false e (AExp (Some rt)) in
++ let (et'', e'') = castTo et rt e' in
++ se @@ (returnChunk (Some e'') loc')
++ end
++
++ | A.SWITCH (e, s, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ let (se, e', et) = doExp false e (AExp (Some intType)) in
++ let (et'', e'') = castTo et intType e' in
++ let s' = doStatement s in
++ se @@ (switchChunk e'' s' loc')
++
++ | A.CASE (e, s, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ let (se, e', et) = doExp true e (AExp None) in
++ if isNotEmpty se then
++ E.s (error "Case statement with a non-constant");
++ caseRangeChunk [if !lowerConstants then constFold false e' else e']
++ loc' (doStatement s)
++
++ | A.CASERANGE (el, eh, s, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ let (sel, el', etl) = doExp false el (AExp None) in
++ let (seh, eh', etl) = doExp false eh (AExp None) in
++ if isNotEmpty sel || isNotEmpty seh then
++ E.s (error "Case statement with a non-constant");
++ let il, ih =
++ match constFold true el', constFold true eh' with
++ Const(CInt64(il, _, _)), Const(CInt64(ih, _, _)) ->
++ i64_to_int il, i64_to_int ih
++ | _ -> E.s (unimp "Cannot understand the constants in case range")
++ in
++ if il > ih then
++ E.s (error "Empty case range");
++ let rec mkAll (i: int) =
++ if i > ih then [] else integer i :: mkAll (i + 1)
++ in
++ caseRangeChunk (mkAll il) loc' (doStatement s)
++
++
++ | A.DEFAULT (s, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ defaultChunk loc' (doStatement s)
++
++ | A.LABEL (l, s, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ (* Lookup the label because it might have been locally defined *)
++ consLabel (lookupLabel l) (doStatement s) loc' true
++
++ | A.GOTO (l, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ (* Maybe we need to rename this label *)
++ gotoChunk (lookupLabel l) loc'
++
++ | A.COMPGOTO (e, loc) -> begin
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ (* Do the expression *)
++ let se, e', t' = doExp false e (AExp (Some voidPtrType)) in
++ match !gotoTargetData with
++ Some (switchv, switch) -> (* We have already generated this one *)
++ se
++ @@ i2c(Set (var switchv, makeCast e' intType, loc'))
++ @@ s2c(mkStmt(Goto (ref switch, loc')))
++
++ | None -> begin
++ (* Make a temporary variable *)
++ let vchunk = createLocal
++ (intType, NoStorage, false, [])
++ (("__compgoto", A.JUSTBASE, [], loc), A.NO_INIT)
++ in
++ if not (isEmpty vchunk) then
++ E.s (unimp "Non-empty chunk in creating temporary for goto *");
++ let switchv, _ =
++ try lookupVar "__compgoto"
++ with Not_found -> E.s (bug "Cannot find temporary for goto *");
++ in
++ (* Make a switch statement. We'll fill in the statements at the
++ * end of the function *)
++ let switch = mkStmt (Switch (Lval(var switchv),
++ mkBlock [], [], loc')) in
++ (* And make a label for it since we'll goto it *)
++ switch.labels <- [Label ("__docompgoto", loc', false)];
++ gotoTargetData := Some (switchv, switch);
++ se @@ i2c (Set(var switchv, makeCast e' intType, loc')) @@
++ s2c switch
++ end
++ end
++
++ | A.DEFINITION d ->
++ let s = doDecl false d in
++(*
++ ignore (E.log "Def at %a: %a\n" d_loc !currentLoc d_chunk s);
++*)
++ s
++
++
++
++ | A.ASM (asmattr, tmpls, details, loc) ->
++ (* Make sure all the outs are variables *)
++ let loc' = convLoc loc in
++ let attr' = doAttributes asmattr in
++ currentLoc := loc';
++ let stmts : chunk ref = ref empty in
++ let (tmpls', outs', ins', clobs') =
++ match details with
++ | None ->
++ let tmpls' =
++ if !msvcMode then
++ tmpls
++ else
++ let pattern = Str.regexp "%" in
++ let escape = Str.global_replace pattern "%%" in
++ List.map escape tmpls
++ in
++ (tmpls', [], [], [])
++ | Some { aoutputs = outs; ainputs = ins; aclobbers = clobs } ->
++ let outs' =
++ List.map
++ (fun (id, c, e) ->
++ let (se, e', t) = doExp false e (AExp None) in
++ let lv =
++ match e' with
++ | Lval lval
++ | StartOf lval -> lval
++ | _ -> E.s (error "Expected lval for ASM outputs")
++ in
++ stmts := !stmts @@ se;
++ (id, c, lv)) outs
++ in
++ (* Get the side-effects out of expressions *)
++ let ins' =
++ List.map
++ (fun (id, c, e) ->
++ let (se, e', et) = doExp false e (AExp None) in
++ stmts := !stmts @@ se;
++ (id, c, e'))
++ ins
++ in
++ (tmpls, outs', ins', clobs)
++ in
++ !stmts @@
++ (i2c (Asm(attr', tmpls', outs', ins', clobs', loc')))
++
++ | TRY_FINALLY (b, h, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ let b': chunk = doBody b in
++ let h': chunk = doBody h in
++ if b'.cases <> [] || h'.cases <> [] then
++ E.s (error "Try statements cannot contain switch cases");
++
++ s2c (mkStmt (TryFinally (c2block b', c2block h', loc')))
++
++ | TRY_EXCEPT (b, e, h, loc) ->
++ let loc' = convLoc loc in
++ currentLoc := loc';
++ let b': chunk = doBody b in
++ (* Now do e *)
++ let ((se: chunk), e', t') = doExp false e (AExp None) in
++ let h': chunk = doBody h in
++ if b'.cases <> [] || h'.cases <> [] || se.cases <> [] then
++ E.s (error "Try statements cannot contain switch cases");
++ (* Now take se and try to convert it to a list of instructions. This
++ * might not be always possible *)
++ let il' =
++ match compactStmts se.stmts with
++ [] -> se.postins
++ | [ s ] -> begin
++ match s.skind with
++ Instr il -> il @ se.postins
++ | _ -> E.s (error "Except expression contains unexpected statement")
++ end
++ | _ -> E.s (error "Except expression contains too many statements")
++ in
++ s2c (mkStmt (TryExcept (c2block b', (il', e'), c2block h', loc')))
++
++ with e when continueOnError -> begin
++ (ignore (E.log "Error in doStatement (%s)\n" (Printexc.to_string e)));
++ E.hadErrors := true;
++ consLabel "booo_statement" empty (convLoc (C.get_statementloc s)) false
++ end
++
++
++let rec stripParenLocal e = match e with
++ | A.PAREN e2 -> stripParenLocal e2
++ | _ -> e
++
++class stripParenClass : V.cabsVisitor = object (self)
++ inherit V.nopCabsVisitor as super
++
++ method vexpr e = match e with
++ | A.PAREN e2 ->
++ V.ChangeDoChildrenPost (stripParenLocal e2,stripParenLocal)
++ | _ -> V.DoChildren
++end
++
++let stripParenFile file = V.visitCabsFile (new stripParenClass) file
++
++
++(* Translate a file *)
++let convFile (f : A.file) : Cil.file =
++ Cil.initCIL (); (* make sure we have initialized CIL *)
++
++ (* remove parentheses from the Cabs *)
++ let fname,dl = stripParenFile f 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");
++ (* Setup the built-ins, but do not add their prototypes to the file *)
++ let setupBuiltin name (resTyp, argTypes, isva) =
++ let v =
++ makeGlobalVar name (TFun(resTyp,
++ Some (List.map (fun at -> ("", at, []))
++ argTypes),
++ isva, [])) in
++ ignore (alphaConvertVarAndAddToEnv true v);
++ (* Add it to the file as well *)
++ cabsPushGlobal (GVarDecl (v, Cil.builtinLoc))
++ in
++ H.iter setupBuiltin Cil.builtinFunctions;
++
++ let globalidx = ref 0 in
++ let doOneGlobal (d: A.definition) =
++ let s = doDecl true d in
++ if isNotEmpty s then
++ E.s (bug "doDecl returns non-empty statement for global");
++ (* See if this is one of the globals which we can leave alone. Increment
++ * globalidx and see if we must leave this alone. *)
++ if
++ (match d with
++ A.DECDEF _ -> true
++ | A.FUNDEF _ -> true
++ | _ -> false) && (incr globalidx; !globalidx = !nocil) then begin
++ (* Create a file where we put the CABS output *)
++ let temp_cabs_name = "__temp_cabs" in
++ let temp_cabs = open_out temp_cabs_name in
++ (* Now print the CABS in there *)
++ Cprint.commit (); Cprint.flush ();
++ let old = !Cprint.out in (* Save the old output channel *)
++ Cprint.out := temp_cabs;
++ Cprint.print_def d;
++ Cprint.commit (); Cprint.flush ();
++ flush !Cprint.out;
++ Cprint.out := old;
++ close_out temp_cabs;
++ (* Now read everythign in *and create a GText from it *)
++ let temp_cabs = open_in temp_cabs_name in
++ let buff = Buffer.create 1024 in
++ Buffer.add_string buff "// Start of CABS form\n";
++ Buffer.add_channel buff temp_cabs (in_channel_length temp_cabs);
++ Buffer.add_string buff "// End of CABS form\n";
++ close_in temp_cabs;
++ (* Try to pop the last thing in the file *)
++ (match !theFile with
++ _ :: rest -> theFile := rest
++ | _ -> ());
++ (* Insert in the file a GText *)
++ cabsPushGlobal (GText(Buffer.contents buff))
++ end
++ in
++ List.iter doOneGlobal dl;
++ let globals = ref (popGlobals ()) 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;
++
++ if false then ignore (E.log "Cabs2cil converted %d globals\n" !globalidx);
++ (* We are done *)
++ { fileName = fname;
++ globals = !globals;
++ globinit = None;
++ globinitcalled = false;
++ }
++
++
++
++
+diff -urN deputy-tinyos-1.1.orig/lib/Deputy.pm deputy-tinyos-1.1/lib/Deputy.pm
+--- deputy-tinyos-1.1.orig/lib/Deputy.pm 2008-08-07 08:25:12.000000000 -0600
++++ deputy-tinyos-1.1/lib/Deputy.pm 2008-08-27 08:41:22.000000000 -0600
+@@ -48,6 +48,19 @@
+ sub new {
+ my ($proto, @args) = @_;
+ my $class = ref($proto) || $proto;
++
++ #set up deputy target stuff
++ {
++ my @args1 = ();
++ foreach my $arg (@args) {
++ if($arg =~ m|--gcc=(.+)$|) {
++ $::cc = $1;
++ } else {
++ push @args1, $arg;
++ }
++ }
++ @args = @args1;
++ }
+ my $self = Cilly->new(@args);
+
+ # Select the directory containing Deputy's executables. We look in
+@@ -70,9 +83,10 @@
+ my $mtime_asm = int((stat("$bin/deputy.asm.exe"))[9]);
+ my $mtime_byte = int((stat("$bin/deputy.byte.exe"))[9]);
+ my $use_debug =
+- grep(/--bytecode/, @args) ||
+- grep(/--ocamldebug/, @args) ||
+- ($mtime_asm < $mtime_byte);
++ (-x "$bin/deputy.byte.exe") &&
++ (grep(/--bytecode/, @args) ||
++ grep(/--ocamldebug/, @args) ||
++ ($mtime_asm < $mtime_byte));
+ if ($use_debug) {
+ $ENV{"OCAMLRUNPARAM"} = "b" . $ENV{"OCAMLRUNPARAM"}; # Print back trace
+ }
+@@ -117,6 +131,12 @@
+ my $res = 1;
+ if ($self->compilerArgument($self->{OPTIONS}, $arg, $pargs)) {
+ # do nothing
++ } elsif ($arg eq "--param") {
++ my $more = $self->fetchNextArg($pargs);
++ push @{$self->{CCARGS}}, $arg;
++ push @{$self->{CCARGS}}, $more;
++ } elsif ($arg =~ m|-B(.+)$|) {
++ push @{$self->{CCARGS}}, $arg;
+ } elsif ($arg eq "--help" || $arg eq "-help") {
+ $self->printVersion();
+ $self->printHelp();
+@@ -144,7 +164,7 @@
+ } elsif ($arg =~ m|^--out=(\S+)$|) {
+ # Intercept the --out argument
+ $self->{CILLY_OUT} = $1;
+- push @{$self->{CILARGS}}, "--out", $1;
++ #push @{$self->{CILARGS}}, "--out", $1;
+ } elsif ($arg eq "--instrument") {
+ $self->{INSTRUMENT} = 1;
+ push @{$self->{CILARGS}}, "--instrument";
+@@ -248,6 +268,9 @@
+
+ my @cmd = ($self->{COMPILER});
+ my $aftercil = $self->cilOutputFile($dest, 'cil.c');
++ if( defined $self->{CILLY_OUT}) {
++ $aftercil->{filename} = $self->{CILLY_OUT};
++ }
+ return ($aftercil, @cmd, '--out', $aftercil);
+ }
+
+diff -urN deputy-tinyos-1.1.orig/Makefile.in deputy-tinyos-1.1/Makefile.in
+--- deputy-tinyos-1.1.orig/Makefile.in 2008-08-07 08:25:12.000000000 -0600
++++ deputy-tinyos-1.1/Makefile.in 2008-08-27 08:41:22.000000000 -0600
+@@ -123,6 +123,7 @@
+ dloopoptim dcheckstrengthen dcheckhoister dfailfinder\
+ oct doctanalysis dnonnullfinder xML xHTML dfdatbrowser\
+ doptimmain dglobinit dlocals dpoly dcheck \
++ dtinyOS \
+ dtaint dinstrumenter dinfer main
+
+ COMPILEFLAGS = -I cil/obj/$(ARCHOS)
+diff -urN deputy-tinyos-1.1.orig/src/dinfer.ml deputy-tinyos-1.1/src/dinfer.ml
+--- deputy-tinyos-1.1.orig/src/dinfer.ml 2008-08-07 08:25:12.000000000 -0600
++++ deputy-tinyos-1.1/src/dinfer.ml 2008-08-27 08:41:22.000000000 -0600
+@@ -46,6 +46,7 @@
+ module E = Errormsg
+ module DC = Dcheck
+ module DO = Doptimmain
++module DT = DtinyOS
+ module S = Stats
+ module N = Ptrnode
+ module H = Hashtbl
+@@ -1717,4 +1718,5 @@
+ E.s(error "Check.checkFile failed!");*)
+ (* this is done in main.ml:
+ if !Doptions.stats then S.print stdout "optimizer-stats:" *)
++ if (!insertFLIDs <> "") then DT.insert_flids f;
+ ()
+diff -urN deputy-tinyos-1.1.orig/src/doptions.ml deputy-tinyos-1.1/src/doptions.ml
+--- deputy-tinyos-1.1.orig/src/doptions.ml 2008-08-07 08:25:12.000000000 -0600
++++ deputy-tinyos-1.1/src/doptions.ml 2008-08-27 08:41:22.000000000 -0600
+@@ -50,6 +50,7 @@
+ let assumeString : bool ref = ref false
+ let alwaysStopOnError : bool ref = ref false
+ let fastChecks : bool ref = ref false
++let insertFLIDs : string ref = ref ""
+ let multipleErrors : bool ref = ref false
+ let inferKinds: bool ref = ref true
+ let saturnLogicPath : string ref = ref ""
+@@ -152,6 +153,19 @@
+ "--fast-checks", Arg.Set fastChecks,
+ ("Optimize checks assuming that we stop on error without printing " ^
+ "specifics about the failure");
++ "--FLIDs", Arg.Set_string insertFLIDs,
++ ("Store verbose failure information in file and replace with fault " ^
++ "location identifier (FLID)");
++ "--envmachine", Arg.Unit (fun _ ->
++ try
++ let machineModel = Sys.getenv "CIL_MACHINE" in
++ Cil.envMachine := Some (Machdepenv.modelParse machineModel);
++ with
++ Not_found ->
++ ignore (Errormsg.error "CIL_MACHINE environment variable is not set")
++ | Failure msg ->
++ ignore (Errormsg.error "CIL_MACHINE machine model is invalid: %s" msg)),
++ ("Use machine model specified in CIL_MACHIINE environment variable");
+ "--zrapp",
+ Arg.Unit (fun n -> C.lineDirectiveStyle := None;
+ C.printerForMaincil := Z.zraCilPrinter;
+diff -urN deputy-tinyos-1.1.orig/src/doptions.mli deputy-tinyos-1.1/src/doptions.mli
+--- deputy-tinyos-1.1.orig/src/doptions.mli 2008-08-07 08:25:12.000000000 -0600
++++ deputy-tinyos-1.1/src/doptions.mli 2008-08-27 08:41:22.000000000 -0600
+@@ -46,6 +46,7 @@
+ val assumeString : bool ref
+ val alwaysStopOnError : bool ref
+ val fastChecks : bool ref
++val insertFLIDs : string ref
+ val multipleErrors : bool ref
+ val inferKinds : bool ref
+ val saturnLogicPath : string ref
+diff -urN deputy-tinyos-1.1.orig/src/dtinyOS.ml deputy-tinyos-1.1/src/dtinyOS.ml
+--- deputy-tinyos-1.1.orig/src/dtinyOS.ml 1969-12-31 17:00:00.000000000 -0700
++++ deputy-tinyos-1.1/src/dtinyOS.ml 2008-08-27 08:41:22.000000000 -0600
+@@ -0,0 +1,230 @@
++open Cil
++open Doptions
++
++(* Module for taking deputized code and replacing verbose error information
++ * with FLIDs *)
++
++(* Nathan Cooprider coop@cs.utah.edu *)
++
++
++(* Things we've added to CIL not in there right now *)
++
++let rec find_unsigned_bitsize ui acc =
++ let rec pow a b =
++ if b <= 0 then 1 else a * (pow a (b-1))
++ in
++ if (ui < (pow 2 acc)) then acc
++ else find_unsigned_bitsize ui (acc+1)
++
++let rec ui_to_hex_string i num =
++ if num <= 0 then
++ "0x"
++ else begin
++ let mask = (1 lsl 4) - 1 in
++ let digit = mask land i in
++ let character =
++ match digit with
++ 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 ->
++ string_of_int digit
++ | 10 -> "A" | 11 -> "B" | 12 -> "C" | 13 -> "D"
++ | 14 -> "E" | 15 -> "F"
++ | _ -> "X"
++ in
++ (ui_to_hex_string (i lsr 4) (num - 4)) ^ character
++ end
++
++let isStringType tp =
++ match tp with
++ TPtr(TInt(IChar, atts),_) when hasAttribute "const" atts -> true
++ | _ -> false
++
++(* End of things we've added to CIL but aren't in CIL *)
++
++
++(* Still need to hexify things *)
++
++let function_list =
++ [
++ "deputy_fail_mayreturn" ;
++ "deputy_fail_noreturn" ;
++ "deputy_fail_noreturn_fast" ;
++ "CNonNull" ;
++ "CEq";
++ "CMult";
++ "CPtrArith";
++ "CPtrArithNT" ;
++ "CPtrArithAccess" ;
++ "CLessInt" ;
++ "CLeqInt" ;
++ "CLeq" ;
++ "CLeqNT" ;
++ "CNullOrLeq" ;
++ "CNullOrLeqNT" ;
++ "CWriteNT" ;
++ "CNullUnionOrSelected" ;
++ "CSelected" ;
++ "CNotSelected"
++ ]
++
++let exists_in_function_list str =
++ List.exists
++ (fun name ->
++ try
++ if (name = str) ||
++ (String.sub str 2 ((String.length str)-2) = name) then
++ true
++ else
++ false
++ with Invalid_argument e ->
++ false
++ )
++ function_list
++
++(* Goes through file and:
++ - replaces strings in list with ""
++ - replaces uses of the line location with the FLID
++ - deals with casts *)
++class fixingFormalsVisitor line str_list flid = object (self)
++ inherit nopCilVisitor
++
++ method vexpr e =
++ match e with
++ Lval(Var v, NoOffset) when List.mem v str_list ->
++ ChangeTo(mkString "")
++ | Lval(Var v, NoOffset) when compare v line = 0 ->
++ ChangeTo(Lval (Var flid, NoOffset))
++ | CastE(tp,x) ->
++ ChangeDoChildrenPost(x,
++ (fun y -> if (Expcompare.compareExp y x) then e
++ else y))
++ | _ ->
++ DoChildren
++
++end
++
++class parameterVisitor oc = object (self)
++ inherit nopCilVisitor
++
++ val mutable count = 33 (* Sanity check, some random number to start *)
++ val mutable string_count = 0
++ val mutable current_func = dummyFunDec
++
++(* The plain Deputy executable does not insert these *)
++ method vvdec v =
++ if (v.vstorage = Extern) && (exists_in_function_list v.vname) then
++ match v.vtype with
++ TFun(tp,Some (args),b,atts) ->
++ let flid = "__FLID_int", intType, [] in
++ let nolocationargs = List.tl (List.rev args) in
++ let rec strip_string_arguments args =
++ match args with
++ (str,tp,atts) :: tl when isStringType tp ->
++ strip_string_arguments tl
++ | _ -> args
++ in
++ let deputy_args = strip_string_arguments nolocationargs in
++
++ let new_args =
++ List.rev
++ (flid :: deputy_args)
++ in
++ v.vtype <- TFun(tp,Some(new_args),b, atts);
++ SkipChildren
++ | _ ->
++ SkipChildren
++ else
++ DoChildren
++
++(* Not necessary if using our own checks.h file *)
++ method vfunc f =
++ current_func <- f;
++ if (exists_in_function_list f.svar.vname) then
++ match (List.rev f.sformals) with
++ i1 :: nolocationargs ->
++ let add_name, add_type = "__FLID_int", intType in
++ let flid = makeVarinfo false add_name add_type in
++ let rec strip_string_arguments args acc=
++ match args with
++ v :: tl when isStringType v.vtype ->
++ strip_string_arguments tl (v::acc)
++ | _ -> args, acc
++ in
++ let deputy_args, dep_list =
++ strip_string_arguments nolocationargs []
++ in
++
++ f.sformals <- List.rev (flid :: deputy_args);
++
++ ignore (visitCilFunction
++ (new fixingFormalsVisitor
++ i1 dep_list flid) f);
++ DoChildren
++ | _ -> DoChildren
++ else
++ DoChildren
++
++ method vinst i =
++ match i with
++ Call (olv, Lval(Var(vi),NoOffset), exl, l)
++ when exists_in_function_list vi.vname ->
++ let new_list =
++ match (List.rev exl) with
++ (** ****************************************************************)
++ i1 :: nolocationargs ->
++
++ if (exists_in_function_list current_func.svar.vname) then
++ (* Not a starting point, so not a new FLID *)
++ let rec strip_string_arguments args =
++ match args with
++ e :: tl when isStringType (typeOf e) ->
++ strip_string_arguments tl
++ | _ -> args
++ in
++ let deputy_args = strip_string_arguments nolocationargs in
++ (* Just use existing int for FLID *)
++ List.rev (i1 :: deputy_args)
++
++ (* *************************************************************)
++ else begin
++ (* Starting point, need a new FLID *)
++
++ ignore (Pretty.fprintf oc "0x%x ### %s ### " count vi.vname);
++ let rec strip_string_arguments args =
++ match args with
++ e :: tl when isStringType (typeOf e) ->
++ ignore (Pretty.fprintf oc "%a ### " d_exp e);
++ strip_string_arguments tl
++ | _ -> args
++ in
++ let deputy_args = strip_string_arguments nolocationargs in
++
++ ignore (Pretty.fprintf oc " %a ### %s \n"
++ d_loc l current_func.svar.vname);
++
++ let flid =
++ let bitsize = find_unsigned_bitsize count 1 in
++ let hex_count = ui_to_hex_string count bitsize in
++ let mint = integer count in
++ match mint with
++ Const (CInt64(sf,ik,so)) ->
++ Const(CInt64(sf,ik,Some(hex_count)))
++ | _ -> mint (* shouldn't happen *)
++ in
++ count <- count + 20 + (Random.int 20);
++ List.rev (flid :: deputy_args)
++ end
++
++ (** ****************************************************************)
++ | _ -> exl
++
++ in
++ ChangeTo [Call (olv,Lval(Var(vi),NoOffset),new_list,l)]
++ | _ -> SkipChildren
++end
++
++let insert_flids f =
++ Random.init 42;
++ let oc = open_out (!insertFLIDs) in
++ visitCilFileSameGlobals (new parameterVisitor oc) f;
++ close_out oc
++
projects / deputy-tinyos.git / commitdiff