diff options
Diffstat (limited to 'cil/src/check.ml')
| -rw-r--r-- | cil/src/check.ml | 1017 |
1 files changed, 0 insertions, 1017 deletions
diff --git a/cil/src/check.ml b/cil/src/check.ml deleted file mode 100644 index 4dc8850..0000000 --- a/cil/src/check.ml +++ /dev/null @@ -1,1017 +0,0 @@ -(* MODIF: Loop constructor replaced by 3 constructors: While, DoWhile, For. *) - -(* - * - * 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. - * - *) - -(* A consistency checker for CIL *) -open Cil -module E = Errormsg -module H = Hashtbl -open Pretty - - -(* A few parameters to customize the checking *) -type checkFlags = - NoCheckGlobalIds (* Do not check that the global ids have the proper - * hash value *) - -let checkGlobalIds = ref true - - (* Attributes must be sorted *) -type ctxAttr = - CALocal (* Attribute of a local variable *) - | CAGlobal (* Attribute of a global variable *) - | CAType (* Attribute of a type *) - -let valid = ref true - -let warn fmt = - valid := false; - Cil.warn fmt - -let warnContext fmt = - valid := false; - Cil.warnContext fmt - -let checkAttributes (attrs: attribute list) : unit = - let rec loop lastname = function - [] -> () - | Attr(an, _) :: resta -> - if an < lastname then - ignore (warn "Attributes not sorted"); - loop an resta - in - loop "" attrs - - - (* Keep track of defined types *) -let typeDefs : (string, typ) H.t = H.create 117 - - - (* Keep track of all variables names, enum tags and type names *) -let varNamesEnv : (string, unit) H.t = H.create 117 - - (* We also keep a map of variables indexed by id, to ensure that only one - * varinfo has a given id *) -let varIdsEnv: (int, varinfo) H.t = H.create 117 - - (* And keep track of all varinfo's to check the uniqueness of the - * identifiers *) -let allVarIds: (int, varinfo) H.t = H.create 117 - - (* Also keep a list of environments. We place an empty string in the list to - * mark the start of a local environment (i.e. a function) *) -let varNamesList : (string * int) list ref = ref [] -let defineName s = - if s = "" then - E.s (bug "Empty name\n"); - if H.mem varNamesEnv s then - ignore (warn "Multiple definitions for %s\n" s); - H.add varNamesEnv s () - -let defineVariable vi = - defineName vi.vname; - varNamesList := (vi.vname, vi.vid) :: !varNamesList; - (* Check the id *) - if H.mem allVarIds vi.vid then - ignore (warn "Id %d is already defined (%s)\n" vi.vid vi.vname); - H.add allVarIds vi.vid vi; - (* And register it in the current scope also *) - H.add varIdsEnv vi.vid vi - -(* Check that a varinfo has already been registered *) -let checkVariable vi = - try - (* Check in the current scope only *) - if vi != H.find varIdsEnv vi.vid then - ignore (warnContext "varinfos for %s not shared\n" vi.vname); - with Not_found -> - ignore (warn "Unknown id (%d) for %s\n" vi.vid vi.vname) - - -let startEnv () = - varNamesList := ("", -1) :: !varNamesList - -let endEnv () = - let rec loop = function - [] -> E.s (bug "Cannot find start of env") - | ("", _) :: rest -> varNamesList := rest - | (s, id) :: rest -> begin - H.remove varNamesEnv s; - H.remove varIdsEnv id; - loop rest - end - in - loop !varNamesList - - - -(* The current function being checked *) -let currentReturnType : typ ref = ref voidType - -(* A map of labels in the current function *) -let labels: (string, unit) H.t = H.create 17 - -(* A list of statements seen in the current function *) -let statements: stmt list ref = ref [] - -(* A list of the targets of Gotos *) -let gotoTargets: (string * stmt) list ref = ref [] - -(*** TYPES ***) -(* Cetain types can only occur in some contexts, so keep a list of context *) -type ctxType = - CTStruct (* In a composite type *) - | CTUnion - | CTFArg (* In a function argument type *) - | CTFRes (* In a function result type *) - | CTArray (* In an array type *) - | CTPtr (* In a pointer type *) - | CTExp (* In an expression, as the type of - * the result of binary operators, or - * in a cast *) - | CTSizeof (* In a sizeof *) - | CTDecl (* In a typedef, or a declaration *) - -let d_context () = function - CTStruct -> text "CTStruct" - | CTUnion -> text "CTUnion" - | CTFArg -> text "CTFArg" - | CTFRes -> text "CTFRes" - | CTArray -> text "CTArray" - | CTPtr -> text "CTPtr" - | CTExp -> text "CTExp" - | CTSizeof -> text "CTSizeof" - | CTDecl -> text "CTDecl" - - -(* Keep track of all tags that we use. For each tag remember also the info - * structure and a flag whether it was actually defined or just used. A - * forward declaration acts as a definition. *) -type defuse = - Defined (* We actually have seen a definition of this tag *) - | Forward (* We have seen a forward declaration for it. This is done using - * a GType with an empty type name *) - | Used (* Only uses *) -let compUsed : (int, compinfo * defuse ref) H.t = H.create 117 -let enumUsed : (string, enuminfo * defuse ref) H.t = H.create 117 -let typUsed : (string, typeinfo * defuse ref) H.t = H.create 117 - -(* For composite types we also check that the names are unique *) -let compNames : (string, unit) H.t = H.create 17 - - - (* Check a type *) -let rec checkType (t: typ) (ctx: ctxType) = - (* Check that it appears in the right context *) - let rec checkContext = function - TVoid _ -> ctx = CTPtr || ctx = CTFRes || ctx = CTDecl - | TNamed (ti, a) -> checkContext ti.ttype - | TArray _ -> - (ctx = CTStruct || ctx = CTUnion - || ctx = CTSizeof || ctx = CTDecl || ctx = CTArray || ctx = CTPtr) - | TComp _ -> ctx <> CTExp - | _ -> true - in - if not (checkContext t) then - ignore (warn "Type (%a) used in wrong context. Expected context: %a" - d_plaintype t d_context ctx); - match t with - (TVoid a | TBuiltin_va_list a) -> checkAttributes a - | TInt (ik, a) -> checkAttributes a - | TFloat (_, a) -> checkAttributes a - | TPtr (t, a) -> checkAttributes a; checkType t CTPtr - - | TNamed (ti, a) -> - checkAttributes a; - if ti.tname = "" then - ignore (warnContext "Using a typeinfo for an empty-named type\n"); - checkTypeInfo Used ti - - | TComp (comp, a) -> - checkAttributes a; - (* Mark it as a forward. We'll check it later. If we try to check it - * now we might encounter undefined types *) - checkCompInfo Used comp - - - | TEnum (enum, a) -> begin - checkAttributes a; - checkEnumInfo Used enum - end - - | TArray(bt, len, a) -> - checkAttributes a; - checkType bt CTArray; - (match len with - None -> () - | Some l -> begin - let t = checkExp true l in - match t with - TInt((IInt|IUInt), _) -> () - | _ -> E.s (bug "Type of array length is not integer") - end) - - | TFun (rt, targs, isva, a) -> - checkAttributes a; - checkType rt CTFRes; - List.iter - (fun (an, at, aa) -> - checkType at CTFArg; - checkAttributes aa) (argsToList targs) - -(* Check that a type is a promoted integral type *) -and checkIntegralType (t: typ) = - checkType t CTExp; - match unrollType t with - TInt _ -> () - | _ -> ignore (warn "Non-integral type") - -(* Check that a type is a promoted arithmetic type *) -and checkArithmeticType (t: typ) = - checkType t CTExp; - match unrollType t with - TInt _ | TFloat _ -> () - | _ -> ignore (warn "Non-arithmetic type") - -(* Check that a type is a promoted boolean type *) -and checkBooleanType (t: typ) = - checkType t CTExp; - match unrollType t with - TInt _ | TFloat _ | TPtr _ -> () - | _ -> ignore (warn "Non-boolean type") - - -(* Check that a type is a pointer type *) -and checkPointerType (t: typ) = - checkType t CTExp; - match unrollType t with - TPtr _ -> () - | _ -> ignore (warn "Non-pointer type") - - -and typeMatch (t1: typ) (t2: typ) = - if typeSig t1 <> typeSig t2 then - match unrollType t1, unrollType t2 with - (* Allow free interchange of TInt and TEnum *) - TInt (IInt, _), TEnum _ -> () - | TEnum _, TInt (IInt, _) -> () - - | _, _ -> ignore (warn "Type mismatch:@! %a@!and %a@!" - d_type t1 d_type t2) - -and checkCompInfo (isadef: defuse) comp = - let fullname = compFullName comp in - try - let oldci, olddef = H.find compUsed comp.ckey in - (* Check that it is the same *) - if oldci != comp then - ignore (warnContext "compinfo for %s not shared\n" fullname); - (match !olddef, isadef with - | Defined, Defined -> - ignore (warnContext "Multiple definition of %s\n" fullname) - | _, Defined -> olddef := Defined - | Defined, _ -> () - | _, Forward -> olddef := Forward - | _, _ -> ()) - with Not_found -> begin (* This is the first time we see it *) - (* Check that the name is not empty *) - if comp.cname = "" then - E.s (bug "Compinfo with empty name"); - (* Check that the name is unique *) - if H.mem compNames fullname then - ignore (warn "Duplicate name %s" fullname); - (* Add it to the map before we go on *) - H.add compUsed comp.ckey (comp, ref isadef); - H.add compNames fullname (); - (* Do not check the compinfo unless this is a definition. Otherwise you - * might run into undefined types. *) - if isadef = Defined then begin - checkAttributes comp.cattr; - let fctx = if comp.cstruct then CTStruct else CTUnion in - let rec checkField f = - if not - (f.fcomp == comp && (* Each field must share the self cell of - * the host *) - f.fname <> "") then - ignore (warn "Self pointer not set in field %s of %s" - f.fname fullname); - checkType f.ftype fctx; - (* Check the bitfields *) - (match unrollType f.ftype, f.fbitfield with - | TInt (ik, a), Some w -> - checkAttributes a; - if w < 0 || w >= bitsSizeOf (TInt(ik, a)) then - ignore (warn "Wrong width (%d) in bitfield" w) - | _, Some w -> - ignore (E.error "Bitfield on a non integer type\n") - | _ -> ()); - checkAttributes f.fattr - in - List.iter checkField comp.cfields - end - end - - -and checkEnumInfo (isadef: defuse) enum = - if enum.ename = "" then - E.s (bug "Enuminfo with empty name"); - try - let oldei, olddef = H.find enumUsed enum.ename in - (* Check that it is the same *) - if oldei != enum then - ignore (warnContext "enuminfo for %s not shared\n" enum.ename); - (match !olddef, isadef with - Defined, Defined -> - ignore (warnContext "Multiple definition of enum %s\n" enum.ename) - | _, Defined -> olddef := Defined - | Defined, _ -> () - | _, Forward -> olddef := Forward - | _, _ -> ()) - with Not_found -> begin (* This is the first time we see it *) - (* Add it to the map before we go on *) - H.add enumUsed enum.ename (enum, ref isadef); - checkAttributes enum.eattr; - List.iter (fun (tn, _, _) -> defineName tn) enum.eitems; - end - -and checkTypeInfo (isadef: defuse) ti = - try - let oldti, olddef = H.find typUsed ti.tname in - (* Check that it is the same *) - if oldti != ti then - ignore (warnContext "typeinfo for %s not shared\n" ti.tname); - (match !olddef, isadef with - Defined, Defined -> - ignore (warnContext "Multiple definition of type %s\n" ti.tname) - | Defined, Used -> () - | Used, Defined -> - ignore (warnContext "Use of type %s before its definition\n" ti.tname) - | _, _ -> - ignore (warnContext "Bug in checkTypeInfo for %s\n" ti.tname)) - with Not_found -> begin (* This is the first time we see it *) - if ti.tname = "" then - ignore (warnContext "typeinfo with empty name"); - checkType ti.ttype CTDecl; - (* Add it to the map before we go on *) - H.add typUsed ti.tname (ti, ref isadef); - end - -(* Check an lvalue. If isconst then the lvalue appears in a context where - * only a compile-time constant can appear. Return the type of the lvalue. - * See the typing rule from cil.mli *) -and checkLval (isconst: bool) (lv: lval) : typ = - match lv with - Var vi, off -> - checkVariable vi; - checkOffset vi.vtype off - - | Mem addr, off -> begin - if isconst then - ignore (warn "Memory operation in constant"); - let ta = checkExp false addr in - match unrollType ta with - TPtr (t, _) -> checkOffset t off - | _ -> E.s (bug "Mem on a non-pointer") - end - -(* Check an offset. The basetype is the type of the object referenced by the - * base. Return the type of the lvalue constructed from a base value of right - * type and the offset. See the typing rules from cil.mli *) -and checkOffset basetyp : offset -> typ = function - NoOffset -> basetyp - | Index (ei, o) -> - checkExpType false ei intType; - begin - match unrollType basetyp with - TArray (t, _, _) -> checkOffset t o - | t -> E.s (bug "typeOffset: Index on a non-array: %a" d_plaintype t) - end - - | Field (fi, o) -> - (* Now check that the host is shared propertly *) - checkCompInfo Used fi.fcomp; - (* Check that this exact field is part of the host *) - if not (List.exists (fun f -> f == fi) fi.fcomp.cfields) then - ignore (warn "Field %s not part of %s" - fi.fname (compFullName fi.fcomp)); - checkOffset fi.ftype o - -and checkExpType (isconst: bool) (e: exp) (t: typ) = - let t' = checkExp isconst e in (* compute the type *) - if isconst then begin (* For initializers allow a string to initialize an - * array of characters *) - if typeSig t' <> typeSig t then - match e, t with - | _ -> typeMatch t' t - end else - typeMatch t' t - -(* Check an expression. isconst specifies if the expression occurs in a - * context where only a compile-time constant can occur. Return the computed - * type of the expression *) -and checkExp (isconst: bool) (e: exp) : typ = - E.withContext - (fun _ -> dprintf "check%s: %a" - (if isconst then "Const" else "Exp") d_exp e) - (fun _ -> - match e with - | Const(CInt64 (_, ik, _)) -> TInt(ik, []) - | Const(CChr _) -> charType - | Const(CStr s) -> charPtrType - | Const(CWStr s) -> TPtr(!wcharType,[]) - | Const(CReal (_, fk, _)) -> TFloat(fk, []) - | Const(CEnum (_, _, ei)) -> TEnum(ei, []) - | Lval(lv) -> - if isconst then - ignore (warn "Lval in constant"); - checkLval isconst lv - - | SizeOf(t) -> begin - (* Sizeof cannot be applied to certain types *) - checkType t CTSizeof; - (match unrollType t with - (TFun _ | TVoid _) -> - ignore (warn "Invalid operand for sizeof") - | _ ->()); - uintType - end - | SizeOfE(e) -> - (* The expression in a sizeof can be anything *) - let te = checkExp false e in - checkExp isconst (SizeOf(te)) - - | SizeOfStr s -> uintType - - | AlignOf(t) -> begin - (* Sizeof cannot be applied to certain types *) - checkType t CTSizeof; - (match unrollType t with - (TFun _ | TVoid _) -> - ignore (warn "Invalid operand for sizeof") - | _ ->()); - uintType - end - | AlignOfE(e) -> - (* The expression in an AlignOfE can be anything *) - let te = checkExp false e in - checkExp isconst (AlignOf(te)) - - | UnOp (Neg, e, tres) -> - checkArithmeticType tres; checkExpType isconst e tres; tres - - | UnOp (BNot, e, tres) -> - checkIntegralType tres; checkExpType isconst e tres; tres - - | UnOp (LNot, e, tres) -> - let te = checkExp isconst e in - checkBooleanType te; - checkIntegralType tres; (* Must check that t is well-formed *) - typeMatch tres intType; - tres - - | BinOp (bop, e1, e2, tres) -> begin - let t1 = checkExp isconst e1 in - let t2 = checkExp isconst e2 in - match bop with - (Mult | Div) -> - typeMatch t1 t2; checkArithmeticType tres; - typeMatch t1 tres; tres - | (Eq|Ne|Lt|Le|Ge|Gt) -> - typeMatch t1 t2; checkArithmeticType t1; - typeMatch tres intType; tres - | Mod|BAnd|BOr|BXor -> - typeMatch t1 t2; checkIntegralType tres; - typeMatch t1 tres; tres - | LAnd | LOr -> - typeMatch t1 t2; checkBooleanType tres; - typeMatch t1 tres; tres - | Shiftlt | Shiftrt -> - typeMatch t1 tres; checkIntegralType t1; - checkIntegralType t2; tres - | (PlusA | MinusA) -> - typeMatch t1 t2; typeMatch t1 tres; - checkArithmeticType tres; tres - | (PlusPI | MinusPI | IndexPI) -> - checkPointerType tres; - typeMatch t1 tres; - checkIntegralType t2; - tres - | MinusPP -> - checkPointerType t1; checkPointerType t2; - typeMatch t1 t2; - typeMatch tres intType; - tres - end - | AddrOf (lv) -> begin - let tlv = checkLval isconst lv in - (* Only certain types can be in AddrOf *) - match unrollType tlv with - | TVoid _ -> - E.s (bug "AddrOf on improper type"); - - | (TInt _ | TFloat _ | TPtr _ | TComp _ | TFun _ | TArray _ ) -> - TPtr(tlv, []) - - | TEnum _ -> intPtrType - | _ -> E.s (bug "AddrOf on unknown type") - end - - | StartOf lv -> begin - let tlv = checkLval isconst lv in - match unrollType tlv with - TArray (t,_, _) -> TPtr(t, []) - | _ -> E.s (bug "StartOf on a non-array") - end - - | CastE (tres, e) -> begin - let et = checkExp isconst e in - checkType tres CTExp; - (* Not all types can be cast *) - match unrollType et with - TArray _ -> E.s (bug "Cast of an array type") - | TFun _ -> E.s (bug "Cast of a function type") - | TComp _ -> E.s (bug "Cast of a composite type") - | TVoid _ -> E.s (bug "Cast of a void type") - | _ -> tres - end) - () (* The argument of withContext *) - -and checkInit (i: init) : typ = - E.withContext - (fun _ -> dprintf "checkInit: %a" d_init i) - (fun _ -> - match i with - SingleInit e -> checkExp true e -(* - | ArrayInit (bt, len, initl) -> begin - checkType bt CTSizeof; - if List.length initl > len then - ignore (warn "Too many initializers in array"); - List.iter (fun i -> checkInitType i bt) initl; - TArray(bt, Some (integer len), []) - end -*) - | CompoundInit (ct, initl) -> begin - checkType ct CTSizeof; - (match unrollType ct with - TArray(bt, Some (Const(CInt64(len, _, _))), _) -> - let rec loopIndex i = function - [] -> - if i <> len then - ignore (warn "Wrong number of initializers in array") - - | (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest -> - if i' <> i then - ignore (warn "Initializer for index %s when %s was expected\n" - (Int64.format "%d" i') (Int64.format "%d" i)); - checkInitType ei bt; - loopIndex (Int64.succ i) rest - | _ :: rest -> - ignore (warn "Malformed initializer for array element") - in - loopIndex Int64.zero initl - | TArray(_, _, _) -> - ignore (warn "Malformed initializer for array") - | TComp (comp, _) -> - if comp.cstruct then - let rec loopFields - (nextflds: fieldinfo list) - (initl: (offset * init) list) : unit = - match nextflds, initl with - [], [] -> () (* We are done *) - | f :: restf, (Field(f', NoOffset), i) :: resti -> - if f.fname <> f'.fname then - ignore (warn "Expected initializer for field %s and found one for %s\n" f.fname f'.fname); - checkInitType i f.ftype; - loopFields restf resti - | [], _ :: _ -> - ignore (warn "Too many initializers for struct") - | _ :: _, [] -> - ignore (warn "Too few initializers for struct") - | _, _ -> - ignore (warn "Malformed initializer for struct") - in - loopFields - (List.filter (fun f -> f.fname <> missingFieldName) - comp.cfields) - initl - - else (* UNION *) - if comp.cfields == [] then begin - if initl != [] then - ignore (warn "Initializer for empty union not empty"); - end else begin - match initl with - [(Field(f, NoOffset), ei)] -> - if f.fcomp != comp then - ignore (bug "Wrong designator for union initializer"); - if !msvcMode && f != List.hd comp.cfields then - ignore (warn "On MSVC you can only initialize the first field of a union"); - checkInitType ei f.ftype - - | _ -> - ignore (warn "Malformed initializer for union") - end - | _ -> - E.s (warn "Type of Compound is not array or struct or union")); - ct - end) - () (* The arguments of withContext *) - - -and checkInitType (i: init) (t: typ) : unit = - let it = checkInit i in - typeMatch it t - -and checkStmt (s: stmt) = - E.withContext - (fun _ -> - (* Print context only for certain small statements *) - match s.skind with - (*Loop _*) While _ | DoWhile _ | For _ | If _ | Switch _ -> nil - | _ -> dprintf "checkStmt: %a" d_stmt s) - (fun _ -> - (* Check the labels *) - let checkLabel = function - Label (ln, l, _) -> - if H.mem labels ln then - ignore (warn "Multiply defined label %s" ln); - H.add labels ln () - | Case (e, _) -> checkExpType true e intType - | _ -> () (* Not yet implemented *) - in - List.iter checkLabel s.labels; - (* See if we have seen this statement before *) - if List.memq s !statements then - ignore (warn "Statement is shared"); - (* Remember that we have seen this one *) - statements := s :: !statements; - match s.skind with - Break _ | Continue _ -> () - | Goto (gref, l) -> - currentLoc := l; - (* Find a label *) - let lab = - match List.filter (function Label _ -> true | _ -> false) - !gref.labels with - Label (lab, _, _) :: _ -> lab - | _ -> - ignore (warn "Goto to block without a label\n"); - "<missing label>" - in - (* Remember it as a target *) - gotoTargets := (lab, !gref) :: !gotoTargets - - - | Return (re,l) -> begin - currentLoc := l; - match re, !currentReturnType with - None, TVoid _ -> () - | _, TVoid _ -> ignore (warn "Invalid return value") - | None, _ -> ignore (warn "Invalid return value") - | Some re', rt' -> checkExpType false re' rt' - end -(* - | Loop (b, l, _, _) -> checkBlock b -*) - | While (e, b, l) -> - currentLoc := l; - let te = checkExp false e in - checkBooleanType te; - checkBlock b; - | DoWhile (e, b, l) -> - currentLoc := l; - let te = checkExp false e in - checkBooleanType te; - checkBlock b; - | For (bInit, e, bIter, b, l) -> - currentLoc := l; - checkBlock bInit; - let te = checkExp false e in - checkBooleanType te; - checkBlock bIter; - checkBlock b; - | Block b -> checkBlock b - | If (e, bt, bf, l) -> - currentLoc := l; - let te = checkExp false e in - checkBooleanType te; - checkBlock bt; - checkBlock bf - | Switch (e, b, cases, l) -> - currentLoc := l; - checkExpType false e intType; - (* Remember the statements so far *) - let prevStatements = !statements in - checkBlock b; - (* Now make sure that all the cases do occur in that block *) - List.iter - (fun c -> - if not (List.exists (function Case _ -> true | _ -> false) - c.labels) then - ignore (warn "Case in switch statment without a \"case\"\n"); - (* Make sure it is in there *) - let rec findCase = function - | l when l == prevStatements -> (* Not found *) - ignore (warnContext - "Cannot find target of switch statement") - | [] -> E.s (E.bug "Check: findCase") - | c' :: rest when c == c' -> () (* Found *) - | _ :: rest -> findCase rest - in - findCase !statements) - cases; - | TryFinally (b, h, l) -> - currentLoc := l; - checkBlock b; - checkBlock h - - | TryExcept (b, (il, e), h, l) -> - currentLoc := l; - checkBlock b; - List.iter checkInstr il; - checkExpType false e intType; - checkBlock h - - | Instr il -> List.iter checkInstr il) - () (* argument of withContext *) - -and checkBlock (b: block) : unit = - List.iter checkStmt b.bstmts - - -and checkInstr (i: instr) = - match i with - | Set (dest, e, l) -> - currentLoc := l; - let t = checkLval false dest in - (* Not all types can be assigned to *) - (match unrollType t with - TFun _ -> ignore (warn "Assignment to a function type") - | TArray _ -> ignore (warn "Assignment to an array type") - | TVoid _ -> ignore (warn "Assignment to a void type") - | _ -> ()); - checkExpType false e t - - | Call(dest, what, args, l) -> - currentLoc := l; - let (rt, formals, isva) = - match checkExp false what with - TFun(rt, formals, isva, _) -> rt, formals, isva - | _ -> E.s (bug "Call to a non-function") - in - (* Now check the return value*) - (match dest, unrollType rt with - None, TVoid _ -> () - | Some _, TVoid _ -> ignore (warn "void value is assigned") - | None, _ -> () (* "Call of function is not assigned" *) - | Some destlv, rt' -> - let desttyp = checkLval false destlv in - if typeSig desttyp <> typeSig rt then begin - (* Not all types can be assigned to *) - (match unrollType desttyp with - TFun _ -> ignore (warn "Assignment to a function type") - | TArray _ -> ignore (warn "Assignment to an array type") - | TVoid _ -> ignore (warn "Assignment to a void type") - | _ -> ()); - (* Not all types can be cast *) - (match rt' with - TArray _ -> ignore (warn "Cast of an array type") - | TFun _ -> ignore (warn "Cast of a function type") - | TComp _ -> ignore (warn "Cast of a composite type") - | TVoid _ -> ignore (warn "Cast of a void type") - - | _ -> ()) - end); - (* Now check the arguments *) - let rec loopArgs formals args = - match formals, args with - [], _ when (isva || args = []) -> () - | (fn,ft,_) :: formals, a :: args -> - checkExpType false a ft; - loopArgs formals args - | _, _ -> ignore (warn "Not enough arguments") - in - if formals = None then - ignore (warn "Call to function without prototype\n") - else - loopArgs (argsToList formals) args - - | Asm _ -> () (* Not yet implemented *) - -let rec checkGlobal = function - GAsm _ -> () - | GPragma _ -> () - | GText _ -> () - | GType (ti, l) -> - currentLoc := l; - E.withContext (fun _ -> dprintf "GType(%s)" ti.tname) - (fun _ -> - checkTypeInfo Defined ti; - if ti.tname <> "" then defineName ti.tname) - () - - | GCompTag (comp, l) -> - currentLoc := l; - checkCompInfo Defined comp; - - | GCompTagDecl (comp, l) -> - currentLoc := l; - checkCompInfo Forward comp; - - | GEnumTag (enum, l) -> - currentLoc := l; - checkEnumInfo Defined enum - - | GEnumTagDecl (enum, l) -> - currentLoc := l; - checkEnumInfo Forward enum - - | GVarDecl (vi, l) -> - currentLoc := l; - (* We might have seen it already *) - E.withContext (fun _ -> dprintf "GVarDecl(%s)" vi.vname) - (fun _ -> - (* If we have seen this vid already then it must be for the exact - * same varinfo *) - if H.mem varIdsEnv vi.vid then - checkVariable vi - else begin - defineVariable vi; - checkAttributes vi.vattr; - checkType vi.vtype CTDecl; - if not (vi.vglob && - vi.vstorage <> Register) then - E.s (bug "Invalid declaration of %s" vi.vname) - end) - () - - | GVar (vi, init, l) -> - currentLoc := l; - (* Maybe this is the first occurrence *) - E.withContext (fun _ -> dprintf "GVar(%s)" vi.vname) - (fun _ -> - checkGlobal (GVarDecl (vi, l)); - (* Check the initializer *) - begin match init.init with - None -> () - | Some i -> ignore (checkInitType i vi.vtype) - end; - (* Cannot be a function *) - if isFunctionType vi.vtype then - E.s (bug "GVar for a function (%s)\n" vi.vname); - ) - () - - - | GFun (fd, l) -> begin - currentLoc := l; - (* Check if this is the first occurrence *) - let vi = fd.svar in - let fname = vi.vname in - E.withContext (fun _ -> dprintf "GFun(%s)" fname) - (fun _ -> - checkGlobal (GVarDecl (vi, l)); - (* Check that the argument types in the type are identical to the - * formals *) - let rec loopArgs targs formals = - match targs, formals with - [], [] -> () - | (fn, ft, fa) :: targs, fo :: formals -> - if fn <> fo.vname || ft != fo.vtype || fa != fo.vattr then - ignore (warnContext - "Formal %s not shared (type + locals) in %s" - fo.vname fname); - loopArgs targs formals - - | _ -> - E.s (bug "Type has different number of formals for %s" - fname) - in - begin match vi.vtype with - TFun (rt, args, isva, a) -> begin - currentReturnType := rt; - loopArgs (argsToList args) fd.sformals - end - | _ -> E.s (bug "Function %s does not have a function type" - fname) - end; - ignore (fd.smaxid >= 0 || E.s (bug "smaxid < 0 for %s" fname)); - (* Now start a new environment, in a finally clause *) - begin try - startEnv (); - (* Do the locals *) - let doLocal tctx v = - if v.vglob then - ignore (warnContext - "Local %s has the vglob flag set" v.vname); - if v.vstorage <> NoStorage && v.vstorage <> Register then - ignore (warnContext - "Local %s has storage %a\n" v.vname - d_storage v.vstorage); - checkType v.vtype tctx; - checkAttributes v.vattr; - defineVariable v - in - List.iter (doLocal CTFArg) fd.sformals; - List.iter (doLocal CTDecl) fd.slocals; - statements := []; - gotoTargets := []; - checkBlock fd.sbody; - H.clear labels; - (* Now verify that we have scanned all targets *) - List.iter - (fun (lab, t) -> if not (List.memq t !statements) then - ignore (warnContext - "Target of \"goto %s\" statement does not appear in function body" lab)) - !gotoTargets; - statements := []; - gotoTargets := []; - (* Done *) - endEnv () - with e -> - endEnv (); - raise e - end; - ()) - () (* final argument of withContext *) - end - - -let checkFile flags fl = - if !E.verboseFlag then ignore (E.log "Checking file %s\n" fl.fileName); - valid := true; - List.iter - (function - NoCheckGlobalIds -> checkGlobalIds := false) - flags; - iterGlobals fl (fun g -> try checkGlobal g with _ -> ()); - (* Check that for all struct/union tags there is a definition *) - H.iter - (fun k (comp, isadef) -> - if !isadef = Used then - begin - valid := false; - ignore (E.warn "Compinfo %s is referenced but not defined" - (compFullName comp)) - end) - compUsed; - (* Check that for all enum tags there is a definition *) - H.iter - (fun k (enum, isadef) -> - if !isadef = Used then - begin - valid := false; - ignore (E.warn "Enuminfo %s is referenced but not defined" - enum.ename) - end) - enumUsed; - (* Clean the hashes to let the GC do its job *) - H.clear typeDefs; - H.clear varNamesEnv; - H.clear varIdsEnv; - H.clear allVarIds; - H.clear compNames; - H.clear compUsed; - H.clear enumUsed; - H.clear typUsed; - varNamesList := []; - if !E.verboseFlag then - ignore (E.log "Finished checking file %s\n" fl.fileName); - !valid - |