Source file check.ml

(*

   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 *)
    | IgnoreInstructions of (instr -> bool) (* Ignore the specified instructions *)

let checkGlobalIds = ref true
let ignoreInstr = ref (fun i -> false)

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 (* TODO: unused *)


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

let fundecForVarIds: (int,unit) 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" 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)" 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" vi.vname)
      else
        ignore (warnContext "variables %s and %s share id %d"
                  vi.vname old.vname vi.vid )
    end
  with Not_found ->
    ignore (warn "Unknown id (%d) for %s" 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 ***)
(* Certain 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 *)
  | CTNumeric                           (* As an argument to __real__ or __imag__ *)

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"
  | CTNumeric -> text "CTNumeric"


(* 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
      | Attr ("pconst", []) -> 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 _ ->
        ctx = CTPtr || ctx = CTDecl || ctx = CTSizeof
    | TInt _ -> true
    | TFloat _ -> true
    | _ -> ctx <> CTNumeric
  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;
      if hasAttribute "complex" a then
        E.s (E.bug "float type has attribute complex, this should never be the case as there are fkinds for this");
  | 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");
      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 ->
          let t = typeOf l in
          if not (isIntegralType t) then
            E.s (bug "Type of array length is not integer"))

  | 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 pointer type *)
and checkPointerType (t: typ) =
  checkType t CTExp;
  if not (isPointerType t) then
    ignore (warn "Non-pointer type")

(* Check that a type is a scalar type *)
and checkScalarType (t: typ) =
  checkType t CTExp;
  if not (isScalarType t) then
    ignore (warn "Non-scalar 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 (ik, _), TEnum (ei, _) when ik = ei.ekind -> ()
      | TEnum (ei, _), TInt (ik, _) when ik = ei.ekind -> ()

      (* Allow unspecified array lengths - this happens with
         flexible array members *)
      | TArray (t, None, _), TArray (t', _, _)
      | TArray (t, _, _), TArray (t', None, _) -> typeMatch t t'
      | _, _ -> 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" fullname);
    (match !olddef, isadef with
    | Defined, Defined ->
        ignore (warnContext "Multiple definition of %s" 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 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")
        | _ -> ());
        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" enum.ename);
    (match !olddef, isadef with
      Defined, Defined ->
        ignore (warnContext "Multiple definition of enum %s" 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" ti.tname);
    (match !olddef, isadef with
      Defined, Defined ->
        ignore (warnContext "Multiple definition of type %s" ti.tname)
    | Defined, Used -> ()
    | Used, Defined ->
        ignore (warnContext "Use of type %s before its definition" ti.tname)
    | _, _ ->
        ignore (warnContext "Bug in checkTypeInfo for %s" 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

      | Real e ->
          let te = checkExp isconst e in
          typeOfRealAndImagComponents te
      | Imag e ->
          let te = checkExp isconst e in
          typeOfRealAndImagComponents te
      | 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
          checkScalarType 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 ->
              checkScalarType t1; checkScalarType t2;
              typeMatch tres intType; 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 !ptrdiffType;
              tres
      end

      | Question (e1, e2, e3, tres) -> begin
          let t1 = checkExp isconst e1 in
          let t2 = checkExp isconst e2 in
          let t3 = checkExp isconst e3 in
          checkScalarType t1;
          typeMatch t2 t3;
          typeMatch t2 tres;
          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 (ei, _) -> TPtr(TInt(ei.ekind, []), [])
          | _ -> E.s (bug "AddrOf on unknown type")
      end

      | AddrOfLabel (gref) -> begin
          (* Find a label *)
          let lab =
            match List.filter (function Label _ -> true | _ -> false)
                  !gref.labels with
              Label (lab, _, _) :: _ -> lab
            | _ ->
                ignore (warn "Address of label to block without a label");
                "<missing label>"
          in
          (* Remember it as a target *)
          gotoTargets := (lab, !gref) :: !gotoTargets;
          voidPtrType
      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, elen, _) ->
              let len =
                match elen with
                | None -> 0L
                | Some e -> (ignore (checkExp true e);
                match getInteger (constFold true e) with
                  Some len -> Z.to_int64 len (* Z on purpose, we don't want to ignore overflows here *)
                | 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(CInt(i', _, _)), NoOffset), ei) :: rest ->
                    if Int64.compare (Z.to_int64 i') i <> 0 then
                      ignore (warn "Initializer for index %s when %s was expected"
                                (Printf.sprintf "%Ld" (Z.to_int64 i')) (Printf.sprintf "%Ld" i));
                    checkInitType ei bt;
                    loopIndex (Int64.succ i) rest
                | _ :: rest ->
                    ignore (warn "Malformed initializer for array element")
              in
              loopIndex Int64.zero initl
          | 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" 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");
                      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, _, _) ->
           let t = checkExp true e in
           if not (isIntegralType t) then
               E.s (bug "Type of case expression is not integer");
        | CaseRange (e1, e2, _, _) ->
           let t1 = checkExp true e1 in
           if not (isIntegralType t1) then
               E.s (bug "Type of case expression is not integer");
           let t2 = checkExp true e2 in
           if not (isIntegralType t2) then
               E.s (bug "Type of case expression is not integer");
        | _ -> () (* 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");
                "<missing label>"
          in
          (* Remember it as a target *)
          gotoTargets := (lab, !gref) :: !gotoTargets
      | ComputedGoto (e, l) ->
          currentLoc := l;
          let te = checkExp false e in
          typeMatch te voidPtrType
      | 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, el, _, _) -> checkBlock b
      | Block b -> checkBlock b
      | If (e, bt, bf, l, el) ->
          currentLoc := l;
          currentExpLoc := el;
          let te = checkExp false e in
          checkScalarType te;
          checkBlock bt;
          checkBlock bf
      | Switch (e, b, cases, l, el) ->
          currentLoc := l;
          currentExpLoc := el;
          let t = checkExp false e in
          if not (isIntegralType t) then
              E.s (bug "Type of switch expression is not integer");
          (* 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;

      | 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, el) ->
      currentLoc := l;
      currentExpLoc := el;
      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, el) ->
      currentLoc := l;
      currentExpLoc := el;
      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 _ -> ()
      (* Avoid spurious warnings for atomic builtins *)
      | Some _, TVoid [Attr ("overloaded", [])] -> ()
      | 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

  | VarDecl (v,_) ->
      if not v.vhasdeclinstruction then
        E.s (bug "Encountered a VarDecl, but vhasdeclinstruction for the varinfo is not set")

  | 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 *)
          if vi.vinit != init then
              E.s (bug "GVar initializer doesn't match vinit (%s)" vi.vname);
          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
      if H.mem fundecForVarIds vi.vid then
        ignore (warn "There already is a different fundec for vid %d (%s)" vi.vid vi.vname);

      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 && v.vstorage <> Static 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 fundecForVarIds;
  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


let checkStandaloneExp ~(vars: varinfo list) (exp: exp) =
  if !E.verboseFlag then ignore (E.log "Checking exp %a\n" d_exp exp);
  valid := true;
  List.iter defineVariable vars;

  (try ignore (checkExp false exp) with _ -> ());

  (* Clean the hashes to let the GC do its job *)
  H.clear typeDefs;
  H.clear varNamesEnv;
  H.clear varIdsEnv;
  H.clear allVarIds;
  H.clear fundecForVarIds;
  H.clear compNames;
  H.clear compUsed;
  H.clear enumUsed;
  H.clear typUsed;
  varNamesList := [];
  if !E.verboseFlag then
    ignore (E.log "Finished checking exp %a\n" d_exp exp);
  !valid