(* * * Copyright (c) 2001-2002, * George C. Necula * Scott McPeak * Wes Weimer * 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 *) | IgnoreInstructions of (instr -> bool) (* Ignore the specified instructions *) let checkGlobalIds = ref true let ignoreInstr = ref (fun i -> false) (* 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 ("CIL invariant broken: "^^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 = (* E.log "saw %s: %d\n" vi.vname vi.vid; *) 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 *) let old = H.find varIdsEnv vi.vid in if vi != old then begin if vi.vname = old.vname then ignore (warnContext "varinfos for %s not shared\n" vi.vname) else ignore (warnContext "variables %s and %s share id %d\n" vi.vname old.vname vi.vid ) end 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 let typeSigIgnoreConst (t : typ) : typsig = let attrFilter (attr : attribute) : bool = match attr with | Attr ("const", []) -> false | _ -> true in typeSigWithAttrs (List.filter attrFilter) t (* 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 || ctx = CTSizeof | TNamed (ti, a) -> checkContext ti.ttype | TArray _ -> (ctx = CTStruct || ctx = CTUnion || ctx = CTSizeof || ctx = CTDecl || ctx = CTArray || ctx = CTPtr) | TFun _ -> if ctx = CTSizeof && !msvcMode then (ignore(warn "sizeof(function) is not defined in MSVC."); false) else ctx = CTPtr || ctx = CTDecl || ctx = CTSizeof | _ -> 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 if not (isIntegralType t) then 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; if not (isIntegralType t) then ignore (warn "Non-integral type") (* Check that a type is a promoted arithmetic type *) and checkArithmeticType (t: typ) = checkType t CTExp; if not (isArithmeticType t) then 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 _ | TEnum _ | TFloat _ | TPtr _ -> () | _ -> ignore (warn "Non-boolean type") (* Check that a type is a pointer type *) and checkPointerType (t: typ) = checkType t CTExp; if not (isPointerType t) then ignore (warn "Non-pointer type") and typeMatch (t1: typ) (t2: typ) = if !Cil.insertImplicitCasts then begin (* Allow mismatches in const-ness, so that string literals can be used as char*s *) if typeSigIgnoreConst t1 <> typeSigIgnoreConst 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) end else begin (* Many casts are missing. For now, just skip this check. *) end 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) (forAddrof: bool) (lv: lval) : typ = match lv with Var vi, off -> checkVariable vi; checkOffset vi.vtype off | Mem addr, off -> begin if isconst && not forAddrof 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) -> checkIntegralType (checkExp false ei); 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 *) (* ignore(E.log "checkType %a %a\n" d_plainexp e d_plaintype t); *) 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(_) -> typeOf e | Lval(lv) -> if isconst then ignore (warn "Lval in constant"); checkLval isconst false lv | SizeOf(t) -> begin (* Sizeof cannot be applied to certain types *) checkType t CTSizeof; (match unrollType t with (TFun _ ) -> ignore (warn "Invalid operand for sizeof") | _ ->()); typeOf e end | SizeOfE(e') -> (* The expression in a sizeof can be anything *) let te = checkExp false e' in checkType te CTSizeof; typeOf e | SizeOfStr s -> typeOf e | AlignOf(t) -> begin (* Sizeof cannot be applied to certain types *) checkType t CTSizeof; typeOf e end | AlignOfE(e') -> (* The expression in an AlignOfE can be anything *) let te = checkExp false e' in checkType te CTSizeof; typeOf e | 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 true 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 true 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") (* A TComp cast that changes the attributes is okay. *) (* | 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 elen, _) -> ignore (checkExp true elen); let len = match isInteger (constFold true elen) with Some len -> len | None -> ignore (warn "Array length is not a constant"); 0L in 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(_, None, _) -> 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 _ | 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"); "" 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 | 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, and that no case is listed twice. *) let casesVisited : stmt list ref = ref [] in List.iter (fun c -> (if List.memq c !casesVisited then ignore (warnContext "Duplicate stmt in \"cases\" list of Switch.") else casesVisited := c::!casesVisited); (* 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) = if !ignoreInstr i then () else match i with | Set (dest, e, l) -> currentLoc := l; let t = checkLval false 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, fnAttrs) = match unrollType (checkExp false what) with TFun(rt, formals, isva, fnAttrs) -> rt, formals, isva, fnAttrs | _ -> 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 false destlv in if typeSig desttyp <> typeSig rt then begin if not !Cabs2cil.doCollapseCallCast then ignore (warn "Destination of Call does not match the return type."); (* 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 unrollType 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 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 then ignore (warnContext "Formal %s not shared (expecting name %s) in %s" fo.vname fn fname); E.withContext (fun () -> text "formal "++ text fo.vname) (fun () -> typeMatch ft fo.vtype) (); if fa != fo.vattr then ignore (warnContext "Formal %s not shared (different attrs) in %s" fo.vname fname); loopArgs targs formals | _ -> E.s (bug "Type has different number of formals for %s" fname) in begin match unrollType 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 | IgnoreInstructions f -> ignoreInstr := f ) 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