cabs2cil.ml

(****************************************************************************)
(*                                                                          *)
(*  Copyright (C) 2001-2003                                                 *)
(*   George C. Necula    <necula@cs.berkeley.edu>                           *)
(*   Scott McPeak        <smcpeak@cs.berkeley.edu>                          *)
(*   Wes Weimer          <weimer@cs.berkeley.edu>                           *)
(*   Ben Liblit          <liblit@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.                                             *)
(*                                                                          *)
(*  File modified by CEA (Commissariat à l'énergie atomique et aux          *)
(*                        énergies alternatives)                            *)
(*               and INRIA (Institut National de Recherche en Informatique  *)
(*                          et Automatique).                                *)
(*                                                                          *)
(****************************************************************************)

(* Modified by TrustInSoft *)

(* Type check and elaborate ABS to CIL *)

(* The references to ISO means ANSI/ISO 9899-1999 *)
module H = Hashtbl
module IH = Datatype.Int.Hashtbl

open Pretty_utils
open Cabs
open Cabshelper
open Cil
let valid_sid = false
(* All statements generated here must have an invalid sid. Use this variable
   for the valid_sid label of Cil.mkStmt*. *)
open Cil_types
open Cil_datatype
open Cil_const

(* Maps the start and end positions of a function declaration or definition
   (including its possible contract) to its name. *)
module FuncLocs = struct
  include
    State_builder.List_ref
      (Datatype.Triple
         (Cil_datatype.Position)(Cil_datatype.Position)(Datatype.String)
      )
      (struct
        let name = "FuncLocs"
        let dependencies = [ Kernel.Files.self ]
      end)

  let add_loc ?spec loc1 loc2 funcname =
    let startpos =
      match spec with
      | None -> fst loc1
      | Some (_, spec_loc) -> fst spec_loc
    in
    let endpos = snd loc2 in
    add (startpos, endpos, funcname)
end

let func_locs () = FuncLocs.get ()

(* Attributes which are entirely unsupported by Frama-C and must cause a
   parsing error, since their behavior requires non-standard parsing *)
let unsupported_attributes = ["vector_size"]

(* Attributes which must be erased to avoid issues (e.g., GCC 'malloc'
   attributes can refer to erased functions and make the code un-reparsable *)
let erased_attributes = ["malloc"]
let () =
  List.iter
    (fun a -> Ast_attributes.register_attribute a AttrIgnored)
    erased_attributes

let stripUnderscore s =
  if String.length s = 1 then begin
    if s = "_" then
      Kernel.error ~once:true ~current:true "Invalid attribute name %s" s;
    s
  end else begin
    let res = Extlib.strip_underscore s in
    if res = "" then
      Kernel.error ~once:true ~current:true "Invalid attribute name %s" s;
    if List.mem res unsupported_attributes then
      Kernel.error ~current:true "unsupported attribute: %s" s
    else begin
      if not (Ast_attributes.is_known_attribute res) then
        Kernel.warning
          ~once:true ~current:true ~wkey:Kernel.wkey_unknown_attribute
          "Unknown attribute: %s" s
    end;
    res
  end

let frama_c_keep_block = "FRAMA_C_KEEP_BLOCK"
let () = Cil_printer.register_shallow_attribute frama_c_keep_block
let () = Ast_attributes.register_attribute frama_c_keep_block AttrStmt

let fc_stdlib = "fc_stdlib"
let fc_stdlib_generated = "fc_stdlib_generated"
let () = Cil_printer.register_shallow_attribute fc_stdlib
let () = Cil_printer.register_shallow_attribute fc_stdlib_generated
(* fc_stdlib attribute already registered in cil.ml *)
let () = Ast_attributes.register_attribute fc_stdlib_generated (AttrName false)

let fc_local_static = "fc_local_static"
let () = Cil_printer.register_shallow_attribute fc_local_static
let () = Ast_attributes.register_attribute fc_local_static (AttrName false)

let frama_c_destructor = "fc_destructor"
let () = Cil_printer.register_shallow_attribute frama_c_destructor
let () = Ast_attributes.register_attribute frama_c_destructor (AttrName false)

let () =
  (* packed and aligned are treated separately, we ignore them
     during standard processing.
  *)
  Ast_attributes.register_attribute "packed" AttrIgnored;
  Ast_attributes.register_attribute "aligned" AttrIgnored;
  Ast_attributes.register_attribute "warn_unused_result" (AttrFunType false);
  Ast_attributes.register_attribute "FC_OLDSTYLEPROTO" (AttrName false);
  Ast_attributes.register_attribute "static" (AttrName false);
  Ast_attributes.register_attribute "missingproto" (AttrName false);
  Ast_attributes.register_attribute "dummy" AttrIgnored;
  Ast_attributes.register_attribute "signal" AttrIgnored; (* AVR-specific attribute *)
  Ast_attributes.register_attribute "leaf" AttrIgnored;
  Ast_attributes.register_attribute "nonnull" AttrIgnored;
  Ast_attributes.register_attribute "deprecated" AttrIgnored;
  Ast_attributes.register_attribute "access" AttrIgnored;
  Ast_attributes.register_attribute "returns_twice" AttrIgnored;
  Ast_attributes.register_attribute "pure" AttrIgnored;
  Ast_attributes.register_attribute "cleanup" AttrIgnored;
  Ast_attributes.register_attribute "warning" AttrIgnored;
  ()

(** A hook into the code that creates temporary local vars.  By default this
    is the identity function, but you can overwrite it if you need to change the
    types of cabs2cil-introduced temp variables. *)
let typeForInsertedVar: (Cil_types.typ -> Cil_types.typ) ref = ref (fun t -> t)

let cabs_exp loc node = { expr_loc = loc; expr_node = node }

let abort_context ?loc msg =
  let loc = match loc with
    | None -> Current_loc.get()
    | Some loc -> loc
  in
  let append fmt =
    Format.pp_print_newline fmt ();
    Errorloc.pp_context_from_file fmt loc
  in
  Kernel.abort ~current:true ~append msg

module IgnorePureExpHook =
  Hook.Build (struct type t = string * Cil_types.exp end)

let register_ignore_pure_exp_hook f =
  IgnorePureExpHook.extend (fun (x,z) -> f x z)

module ImplicitPrototypeHook =
  Hook.Build (struct type t = varinfo end)

let register_implicit_prototype_hook f = ImplicitPrototypeHook.extend f

module DifferentDeclHook =
  Hook.Build(struct type t = varinfo * varinfo end)

let register_different_decl_hook f =
  DifferentDeclHook.extend (fun (x,y) -> f x y)

module NewGlobalHook = Hook.Build(struct type t = varinfo * bool end)
let register_new_global_hook f = NewGlobalHook.extend (fun (x, y) -> f x y)

module LocalFuncHook = Hook.Build(struct type t = varinfo end)

let register_local_func_hook = LocalFuncHook.extend

module IgnoreSideEffectHook =
  Hook.Build(struct type t = Cabs.expression * Cil_types.exp end)

let register_ignore_side_effect_hook f =
  IgnoreSideEffectHook.extend (fun (y,z) -> f y z)

module ConditionalSideEffectHook =
  Hook.Build(struct type t = Cabs.expression * Cabs.expression end)

module ForLoopHook =
  Hook.Build(struct
    type t =
      Cabs.for_clause * Cabs.expression * Cabs.expression * Cabs.statement
  end)

let register_for_loop_all_hook f =
  ForLoopHook.extend (fun (x,y,z,t) -> f x y z t)

let register_for_loop_init_hook f =
  ForLoopHook.extend (fun (x,_,_,_) -> f x)

let register_for_loop_test_hook f =
  ForLoopHook.extend (fun (_,x,_,_) -> f x)

let register_for_loop_incr_hook f =
  ForLoopHook.extend (fun (_,_,x,_) -> f x)

let register_for_loop_body_hook f =
  ForLoopHook.extend (fun (_,_,_,x) -> f x)

let register_conditional_side_effect_hook f =
  ConditionalSideEffectHook.extend (fun (y,z) -> f y z)

(* These symbols are supposed to be macros. It is not possible to
   take their address or to redeclare them outside of the proper header
   in stdlib. See CERT MSC38-C rule.
*)
let no_suppress_function_macro =
  [ "assert"; "setjmp"; "va_arg"; "va_copy"; "va_end"; "va_start" ]

let no_redefine_macro =
  "errno" :: "math_errhandling" :: no_suppress_function_macro

let is_stdlib_function_macro n = List.mem n no_suppress_function_macro

let is_stdlib_macro n = List.mem n no_redefine_macro

let is_bitwise_bop = function
  | Cabs.BAND | Cabs.BOR | Cabs.XOR -> true
  | _ -> false

let is_relational_bop = function
  | EQ | NE | LT | GT | LE | GE -> true
  | _ -> false

let rec stripParen e =
  match e with
  | { expr_node = Cabs.PAREN e } -> stripParen e
  | e -> e

let is_for_builtin builtin info =
  match info with
  | SINGLE_INIT { expr_node = VARIABLE name } ->
    String.equal ("__fc_" ^ builtin) name
  | _ -> false

let rec is_dangerous_offset = function
    NoOffset -> false
  | Field (fi, o) ->
    Cil.typeHasAttribute "volatile" (Cil.unrollType fi.ftype) ||
    is_dangerous_offset o
  | Index _ -> true

let rec is_dangerous e = match e.enode with
  | Lval lv | AddrOf lv | StartOf lv -> is_dangerous_lval lv
  | UnOp (_,e,_) | CastE(_,e) -> is_dangerous e
  | BinOp(_,e1,e2,_) -> is_dangerous e1 || is_dangerous e2
  | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
    false
and is_dangerous_lval = function
  | Var v,_ when
      (not v.vglob && not v.vformal && not v.vtemp)
      || Ast_attributes.has_attribute "volatile" v.vattr
      || Cil.typeHasAttribute "volatile" (Cil.unrollType v.vtype)
    -> true
  (* Local might be uninitialized, which will trigger UB,
     but we assume that the variables we generate are correctly initialized.
  *)
  | Var _, o -> is_dangerous_offset o
  | Mem _,_ -> true

class check_no_locals = object
  inherit nopCilVisitor
  method! vlval (h,_) =
    (match h with
     | Var v ->
       if not v.vglob then
         Kernel.error ~once:true ~current:true
           "Forbidden access to local variable %a in static initializer"
           Cil_printer.pp_varinfo v
     | _ -> ());
    DoChildren
end

let rec check_no_locals_in_initializer i =
  match i with
  | SingleInit e ->
    ignore (visitCilExpr (new check_no_locals) e)
  | CompoundInit (ct, initl) ->
    foldLeftCompound ~implicit:false
      ~doinit:(fun _off' i' _ () ->
          check_no_locals_in_initializer i')
      ~ct:ct
      ~initl:initl
      ~acc:()


(* ---------- source error message handling ------------- *)
let cabslu s =
  {Cil_datatype.Position.unknown with
   Filepath.pos_path = Datatype.Filepath.of_string ("Cabs2cil_start" ^ s)},
  {Cil_datatype.Position.unknown with
   Filepath.pos_path = Datatype.Filepath.of_string ("Cabs2cil_end" ^ s)}


(** Keep a list of the variable ID for the variables that were created to
 * hold the result of function calls *)
let callTempVars: unit IH.t = IH.create 13

(* Check that s starts with the prefix p *)
let prefix p s =
  let lp = String.length p in
  let ls = String.length s in
  lp <= ls && String.sub s 0 lp = p


(***** PROCESS PRAGMAS **********)

(* fc_stdlib pragma. Delimits blocks of globals that are declared in
   a given std lib header. By default, they will not be pretty-printed by
   frama-c -print, which will emit #include "header.h" instead
*)
let current_stdheader = ref []

let pop_stdheader () =
  match !current_stdheader with
  | s::l ->
    Kernel.debug ~dkey:Kernel.dkey_typing_pragma "Popping %s %s" fc_stdlib s;
    current_stdheader := l
  | [] ->
    Kernel.warning ~current:true
      "#pragma %s pop does not match a push" fc_stdlib

let push_stdheader s =
  Kernel.debug ~dkey:Kernel.dkey_typing_pragma "Pushing %s %s@." fc_stdlib s;
  current_stdheader := s::!current_stdheader

(* Returns the topmost (latest) header that is not internal to Frama-C,
   unless it is the only one.
   This prevents the pretty-printing function from including Frama-C
   internal files, unless they were directly specified by the user. *)
let get_current_stdheader () =
  let rec aux = function
    | [] -> ""
    | [ s ] -> s
    | s :: l when String.starts_with ~prefix:"__fc_" s -> aux l
    | s :: _ -> s
  in
  aux !current_stdheader

(* there are several pragmas that we process directly here and remove
   from the globals list, by returning None. We bind their respective
   processing functions with the operator below.
*)
let (>>?) opt f =
  match opt with
  | Some (name, args) -> f name args
  | _ -> opt

let process_stdlib_pragma name args =
  if name = fc_stdlib then begin
    match args with
    | [ ACons ("pop",_) ] -> pop_stdheader (); None
    | [ ACons ("push",_); AStr s ] ->
      let base_name = (System_config.Share.libc:>string) in
      let relative_name = Filepath.relativize ~base_name s in
      push_stdheader relative_name;
      None
    | _ -> Some (name, args)
  end else Some (name, args)

let fc_stdlib_attribute attrs =
  let open Ast_attributes in
  let s = get_current_stdheader () in
  if s = "" then attrs
  else begin
    let payload, attrs =
      if has_attribute fc_stdlib attrs then begin
        AStr s :: find_attribute fc_stdlib attrs,
        drop_attribute fc_stdlib attrs
      end else [AStr s], attrs
    in
    add_attribute (fc_stdlib, payload) attrs
  end
(* ICC align/noalign pragmas (not supported by GCC/MSVC with this syntax).
   Implemented by translating them to 'aligned' attributes. Currently,
   only default and noalign are supported, not explicit alignment values.
   Cf. www.slac.stanford.edu/grp/cd/soft/rmx/manuals/IC_386.PDF *)
let current_pragma_align = ref (None : bool option)
let pragma_align_by_struct = H.create 17

let process_align_pragma name args =
  let aux pname v =
    (if Machine.(msvcMode () || gccMode ())
     then Kernel.warning ?wkey:None else Kernel.debug ~level:1 ?dkey:None)
      ~current:true "Parsing ICC '%s' pragma." pname;
    match args with
    | [] -> current_pragma_align := Some v
    | l ->
      List.iter
        (function
          | AStr s | ACons (s, _) -> H.replace pragma_align_by_struct s v
          | _ -> Kernel.warning ~current:true
                   "Unsupported '%s' pragma not honored by Frama-C." pname
        ) l
  in
  match name with
  | "align" -> aux "align" true
  | "noalign" -> aux "noalign" false
  | _ -> ()

let align_pragma_for_struct sname =
  try Some (H.find pragma_align_by_struct sname)
  with Not_found -> !current_pragma_align

(* The syntax and semantics for the pack pragmas are GCC's, which emulates most
   of MSVC's behaviors. Some of it has been tested using MSVC 2010.
   Note that #pragma pack directives are emulated by translating them into
   GCC-style attributes, which in turn are not supported by MSVC.
   Therefore some combinations of attributes may be impossible to produce in
   MSVC, which means that Frama-C on an MSVC machdep may accept more programs
   that MSVC would. *)

(* The pack pragma stack *)
let packing_pragma_stack = Stack.create ()

(* The current pack pragma *)
let current_packing_pragma = ref None
let pretty_current_packing_pragma fmt =
  let align =
    Option.value ~default:(Integer.of_int (Machine.alignof_aligned ()))
      !current_packing_pragma
  in
  Integer.pretty fmt align

(* Checks if [n] is a valid alignment for #pragma pack, and emits a warning
   if it is not the case. Returns the value to be set as current packing pragma.
   From the MSDN reference
   (msdn.microsoft.com/en-us/library/2e70t5y1(v=vs.100).aspx):
   Valid values are 1, 2, 4, 8, and 16.

   NOTE: GCC seems to consider '#pragma pack(0)' as equivalent to '#pragma pack()',
   but this is not specified in their documentation. To avoid rejecting programs
   with such pragmas, we emulate GCC's current behavior but emit a warning.
   This is the only case when this function returns [None]. *)
let get_valid_pragma_pack_alignment n =
  if Integer.is_zero n && Machine.gccMode () then begin
    Kernel.warning ~current:true "GCC accepts pack(0) but does not specify its \
                                  behavior; considering it equivalent to pack()";
    true, None
  end
  else begin
    let valid = Integer.(equal n one || equal n two || equal n four ||
                         equal n eight || equal n sixteen)
    in
    if not valid then
      Kernel.warning ~current:true "ignoring invalid packing alignment (%a)"
        Integer.pretty n;
    valid, Some n
  end

let process_pack_pragma name args =
  begin match name with
    | "pack" -> begin
        match args with
        | [ACons ("",[])] (*  #pragma pack() *) ->
          Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
            "packing pragma: restoring alignment to default (%d)"
            (Machine.alignof_aligned ());
          current_packing_pragma := None; None
        | [AInt n] (* #pragma pack(n) *) ->
          let is_valid, new_pragma = get_valid_pragma_pack_alignment n in
          if is_valid then begin
            Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
              "packing pragma: setting alignment to %a" Integer.pretty n;
            current_packing_pragma := new_pragma; None
          end else
            Some (name, args)
        | [ACons ("push",[])] (* #pragma pack(push) *) ->
          Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
            "packing pragma: pushing alignment %t" pretty_current_packing_pragma;
          Stack.push !current_packing_pragma packing_pragma_stack; None
        | [ACons ("push",[]); AInt n] (* #pragma pack(push,n) *) ->
          let is_valid, new_pragma = get_valid_pragma_pack_alignment n in
          if is_valid then begin
            Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
              "packing pragma: pushing alignment %t, setting alignment to %a"
              pretty_current_packing_pragma Integer.pretty n;
            Stack.push !current_packing_pragma packing_pragma_stack;
            current_packing_pragma:= new_pragma; None
          end else
            Some (name, args)
        | ACons ("push",[]) :: args (* unknown push directive *) ->
          Kernel.warning ~current:true
            "Unsupported argument for pragma pack push directive: `%a'."
            Format.(
              pp_print_list
                ~pp_sep:(fun fmt ()->pp_print_string fmt ", ")
                Cil_printer.pp_attrparam)
            args;
          (* We don't change the current packing directive, but
             nevertheless push it on the stack, to avoid a mismatched
             pop somewhere later. *)
          Stack.push !current_packing_pragma packing_pragma_stack;
          None
        | [ACons ("pop",[])] (* #pragma pack(pop) *) ->
          begin try
              current_packing_pragma := Stack.pop packing_pragma_stack;
              Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
                "packing pragma: popped alignment %t" pretty_current_packing_pragma;
              None
            with Stack.Empty ->
              (* GCC/Clang/MSVC seem to ignore the directive when a pop() is
                 called with an empty stack, so we emulate their behavior. *)
              Kernel.warning ~current:true
                "ignoring #pragma pack(pop) with empty stack";
              None
          end
        | [ACons ("show",[])] (* #pragma pack(show) *) ->
          Some (name, args)
        | _ ->
          Kernel.warning ~current:true
            "Unsupported packing pragma not honored by Frama-C: #pragma pack(%a)"
            (Pretty_utils.pp_list ~sep:", " ~empty:"<empty>"
               Cil_printer.pp_attrparam) args;
          Some (name, args)
      end
    | _ -> Some (name, args)
  end

let force_packed_attribute a =
  if Ast_attributes.has_attribute "packed" a then a
  else Ast_attributes.add_attribute ("packed",[]) a

let is_power_of_two i = i > 0 && i land (i-1) = 0

(* Computes the numeric value corresponding to an 'aligned' attribute:
   – if 'aligned' (without integer), then use the maximum machine alignment;
   – else, try to const-fold the expression to an integer value.
   Returns [Some n] in case of success, [None] otherwise.
   Note that numeric values that are not powers of two are invalid and
   also return [None]. *)
let eval_aligned_attrparams aps =
  match aps with
  | [] -> Some (Integer.of_int (Machine.alignof_aligned ()))
  | [ap] ->
    begin
      match Cil.intOfAttrparam ap with
      | None -> None
      | Some n -> if is_power_of_two n then Some (Integer.of_int n) else None
    end
  | _ -> (* 'aligned(m,n,...)' is not a valid syntax *) None

let warn_invalid_align_attribute aps =
  Kernel.warning ~current:true ~once:true
    "ignoring invalid aligned attribute: %a"
    Cil_printer.pp_attribute ("aligned", aps)

(* If there is more than one 'aligned' attribute, GCC's behavior is to
   consider the maximum among them. This function computes this value
   and also emits warnings for invalid attributes. *)
let combine_aligned_attributes attrs =
  match Ast_attributes.filter_attributes "aligned" attrs with
  | [] -> None
  | aligned_attrs ->
    List.fold_left (fun acc attr ->
        match attr with
        | ("aligned", aps) ->
          begin
            let align = eval_aligned_attrparams aps in
            if align = None then begin
              warn_invalid_align_attribute aps;
              acc
            end else
              match acc, align with
              | None, a | a, None -> a
              | Some old_n, Some new_n -> Some (Integer.max old_n new_n)
          end
        | _ -> assert false (* attributes were previously filtered by name *)

      ) None aligned_attrs

let warn_incompatible_pragmas_attributes apragma has_attrs =
  if apragma <> None then
    Kernel.warning ~current:true ~once:true
      "ignoring 'align' pragma due to presence of 'pack' pragma.@ \
       No compiler was supposed to accept both syntaxes.";
  if Machine.msvcMode () && has_attrs then
    (* MSVC does not allow attributes *)
    Kernel.warning ~current:true ~once:true
      "field attributes should not be present in MSVC-compatible sources"

(* checks [attrs] for invalid aligned() attributes *)
let check_aligned attrs =
  List.fold_right (fun attr acc ->
      match attr with
      | ("aligned", aps) ->
        if eval_aligned_attrparams aps = None then
          (warn_invalid_align_attribute aps; acc)
        else attr :: acc
      | _ -> attr :: acc
    ) attrs []

(* Takes into account the possible effect of '#pragma pack' directives on
   component [ci], and checks the alignment of aligned() attributes.
   This function is complemented by
   [process_pragmas_pack_align_field_attributes]. *)
let process_pragmas_pack_align_comp_attributes loc ci cattrs =
  let open Ast_attributes in
  let source = snd loc in
  match !current_packing_pragma, align_pragma_for_struct ci.corig_name with
  | None, None -> check_aligned cattrs
  | Some n, apragma ->
    warn_incompatible_pragmas_attributes apragma (cattrs <> []);
    let with_aligned_attributes =
      match combine_aligned_attributes cattrs with
      | None ->
        (* No valid aligned attributes in this field.
           – if the composite type has a packed attribute, then add the
             alignment given by the pack pragma;
           – otherwise, no alignment attribute is necessary.
           Drop existing "aligned" attributes, if there are invalid ones. *)
        if has_attribute "packed" cattrs then (drop_attribute "aligned" cattrs)
        else begin
          Kernel.feedback ~source ~dkey:Kernel.dkey_typing_pragma
            "adding aligned(%a) attribute to comp '%s' due to packing pragma"
            Integer.pretty n ci.cname;
          add_attribute ("aligned",[AInt n]) (drop_attribute "aligned" cattrs)
        end
      | Some local ->
        (* The largest aligned wins with GCC. Don't know
           with other compilers. *)
        let align = Integer.max n local in
        Kernel.feedback ~source ~dkey:Kernel.dkey_typing_pragma
          "setting aligned(%a) attribute to comp '%s' due to packing pragma"
          Integer.pretty align ci.cname;
        add_attribute ("aligned",[AInt align])
          (drop_attribute "aligned" cattrs)
    in
    force_packed_attribute with_aligned_attributes
  | None, Some true ->
    drop_attribute "aligned" cattrs
  | None, Some false ->
    force_packed_attribute
      (add_attribute
         (("aligned",[AInt Integer.one]))
         (drop_attribute "aligned" cattrs))

(* Takes into account the possible effect of '#pragma pack' directives on
   field [fi], and checks the alignment of aligned() attributes.
   Because we emulate them using GCC attributes, this transformation
   is complex and depends on several factors:
   - if the struct inside the pragma is packed, then ignore alignment constraints
     given by the pragma;
   - otherwise, each struct field should have the alignment given by the pack
     directive, unless that field already has an align attribute, in which case
     the minimum of both is taken into account (note that, in GCC, if a field
     has 2 alignment directives, it is the maximum of those that is taken). *)
let process_pragmas_pack_align_field_attributes fi fattrs cattr =
  let open Current_loc.Operators in
  let open Ast_attributes in
  let<> UpdatedCurrentLoc = fi.floc in
  match !current_packing_pragma, align_pragma_for_struct fi.forig_name with
  | None, None -> check_aligned fattrs
  | Some n, apragma ->
    warn_incompatible_pragmas_attributes apragma (fattrs <> []);
    let field_align = combine_aligned_attributes fattrs in
    (* If this field has no valid aligned attributes and the composite type
        has a packed attribute, nothing needs to be done: the composite will
        have the "packed" attribute anyway. *)
    if field_align = None && has_attribute "packed" cattr then
      drop_attribute "aligned" fattrs
    else
      (* Otherwise, align on min(n, max(field alignment, type alignment)):
         the field alignment attribute (if there is one) may be smaller than
         its type alignment, so we get the maximum of both. Then, we apply
         the pragma pack: the final alignment will be the minimum between what
         we had and [n]. *)
      let type_align = Integer.of_int (Cil.bytesAlignOf fi.ftype) in
      let existing_align =
        Option.fold field_align ~none:type_align ~some:(Integer.max type_align)
      in
      let new_align = Integer.min n existing_align in
      Kernel.feedback ~dkey:Kernel.dkey_typing_pragma ~current:true
        "%s aligned(%a) attribute to field '%s.%s' due to packing pragma"
        (if Option.is_none field_align then "adding" else "setting")
        Integer.pretty new_align fi.fcomp.cname fi.fname;
      let new_attr = ("aligned", [AInt new_align]) in
      add_attribute new_attr (drop_attribute "aligned" fattrs)
  | None, Some true ->
    drop_attribute "aligned" fattrs
  | None, Some false ->
    (add_attribute
       ("aligned",[AInt Integer.one])
       (drop_attribute "aligned" fattrs))


(***** COMPUTED GOTO ************)

(* The address of labels are small integers (starting from 0). A computed
 * goto is replaced with a switch on the address of the label. We generate
 * only one such switch and we'll jump to it from all computed gotos. To
 * accomplish this we'll add a local variable to store the target of the
 * goto. *)

(* The local variable in which to put the detonation of the goto and the
 * statement where to jump *)
let gotoTargetData: (varinfo * stmt) option ref = ref None

(* The "addresses" of labels *)
let gotoTargetHash: (string, int) H.t = H.create 13
let gotoTargetNextAddr: int ref = ref 0


(* When we process an argument list, remember the argument index which has a
 * transparent union type, along with the original type. We need this to
 * process function definitions *)
let transparentUnionArgs : (int * typ) list ref = ref []

let debugLoc = false
let convLoc (l : cabsloc) =
  if debugLoc then
    Kernel.debug "convLoc at %a: line %d, btye %d\n"
      Datatype.Filepath.pretty (fst l).Filepath.pos_path
      (fst l).Filepath.pos_lnum (fst l).Filepath.pos_bol;
  l

let isOldStyleVarArgName n =
  if Machine.msvcMode () then n = "va_alist"
  else n = "__builtin_va_alist"

let isOldStyleVarArgTypeName n =
  if Machine.msvcMode () then n = "va_list"  || n = "__ccured_va_list"
  else n = "__builtin_va_alist_t"

(* CERT EXP 46 rule: operands of bitwise operators should not be of type _Bool
   or the result of a comparison.
*)
let check_logical_operand e t =
  let (source,_) = e.expr_loc in
  match Cil.unrollTypeNode t with
  | TInt IBool ->
    Kernel.warning ~wkey:Kernel.wkey_cert_exp_46 ~source
      "operand of bitwise operator has boolean type"
  | _ ->
    let rec aux = function
      | { expr_node = Cabs.PAREN e} -> aux e
      | { expr_node = Cabs.BINARY (bop,_,_); expr_loc = (source, _) }
        when is_relational_bop bop ->
        Kernel.warning ~wkey:Kernel.wkey_cert_exp_46 ~source
          "operand of bitwise operator is a logical relation"
      | _ -> (* EXP 46 does not forbid something like
                (x && y) & z, even though the logical and returns 0 or 1 as
                a relational operator. Maybe this should be clarified. *)
        ()
    in
    aux e

(*** EXPRESSIONS *************)

(* We collect here the program *)
let theFile : global list ref = ref []
let theFileTypes : global list ref = ref []
(* This hashtbl contains the varinfo-indexed globals of theFile.
   They are duplicated here for faster lookup *)
let theFileVars : global Cil_datatype.Varinfo.Hashtbl.t =
  Cil_datatype.Varinfo.Hashtbl.create 13

let findVarInTheFile vi =
  try  List.rev (Cil_datatype.Varinfo.Hashtbl.find_all theFileVars vi)
  with Not_found -> []

let update_fundec_in_theFile vi (f:global -> unit) =
  let rec aux = function
    | [] -> assert false
    | (GFunDecl _ as g) :: _ -> f g
    | _ :: tl -> aux tl
  in
  aux (findVarInTheFile vi)

let update_funspec_in_theFile vi spec =
  let rec aux = function
    | [] -> assert false
    | GFun (f,oldloc) :: _ ->
      Logic_utils.merge_funspec ~oldloc f.sspec spec
    | _ :: tl -> aux tl
  in
  aux (findVarInTheFile vi)

let find_existing_behaviors vi =
  let behaviors spec = List.map (fun x -> x.b_name) spec.spec_behavior in
  let aux acc = function
    | GFun(f,_) -> (behaviors f.sspec) @ acc
    | GFunDecl (spec,_,_)  -> behaviors spec @ acc
    | _ -> acc
  in List.fold_left aux [] (findVarInTheFile vi)

let get_formals vi =
  let rec aux = function
    | [] -> assert false
    | GFun(f,_)::_ -> f.sformals
    | _ :: tl -> aux tl
  in aux (findVarInTheFile vi)

let initGlobals () =
  theFile := [];
  theFileTypes := [];
  Cil_datatype.Varinfo.Hashtbl.clear theFileVars


(* Keep track of some variable ids that must be turned into definitions. We
 * do this when we encounter what appears a definition of a global but
 * without initializer. We leave it a declaration because maybe down the road
 * we see another definition with an initializer. But if we don't see any
 * then we turn the last such declaration into a definition without
 * initializer *)
let mustTurnIntoDef: bool IH.t = IH.create 117

(* Globals that have already been defined. Indexed by the variable name. *)
let alreadyDefined: (string, location) H.t = H.create 117

let isDefined vi = H.mem alreadyDefined vi.vorig_name

(* Globals that were created due to static local variables. We chose their
 * names to be distinct from any global encountered at the time. But we might
 * see a global with conflicting name later in the file. *)
let staticLocals: (string, varinfo) H.t = H.create 13


(* Typedefs. We chose their names to be distinct from any global encountered
 * at the time. But we might see a global with conflicting name later in the
 * file *)
let typedefs: (string, typeinfo) H.t = H.create 13

let fileGlobals () =
  let rec revonto (tail: global list) = function
      [] -> tail

    | GVarDecl (vi, _) :: rest when IH.mem mustTurnIntoDef vi.vid ->
      IH.remove mustTurnIntoDef vi.vid;
      (* Use the location of vi instead of the one carried by GVarDecl.
         Maybe we found in the same file a declaration and then a tentative
         definition. In this case, both are GVarDecl, but the location carried
         by [vi] is the location of the tentative definition, which is more
         useful. *)
      if vi.vstorage = Extern then vi.vstorage <- NoStorage;
      vi.vdefined <- true;
      revonto (GVar (vi, {init = None}, vi.vdecl) :: tail) rest

    | x :: rest -> revonto (x :: tail) rest
  in
  revonto (revonto [] !theFile) !theFileTypes


class checkGlobal = object
  inherit nopCilVisitor


  method! vglob = function
    | GVar _ -> DoChildren
    | _ -> SkipChildren

  method! vexpr exp =
    begin
      match exp.enode with
      | SizeOfE _ ->
        (* sizeOf doesn't depend on the definitions *)
        ()
      | _ ->
        let problematic_var : string option ref = ref None in
        let is_varinfo_cst vi =
          let res = Cil.isConstType vi.vtype && isDefined vi in
          if not res then problematic_var := Some vi.vorig_name;
          res
        in
        if not(isConstant ~is_varinfo_cst exp)
        then
          match !problematic_var with
          | Some name ->
            Kernel.error ~once:true ~current:true
              ("%s is not a compile-time constant") name
          | None ->
            Kernel.error ~once:true ~current:true
              "Initializer element is not a compile-time constant";
    end;
    SkipChildren

end

let cabsPushGlobal (g: global) =
  ignore (visitCilGlobal (new checkGlobal) g);
  pushGlobal g ~types:theFileTypes ~variables:theFile;
  (match g with
   | GVar (vi, _, _) | GVarDecl (vi, _)
   | GFun ({svar = vi}, _) | GFunDecl (_, vi, _) ->
     (* Do 'add' and not 'replace' here, as we may store both
        declarations and definitions for the same varinfo *)
     Cil_datatype.Varinfo.Hashtbl.add theFileVars vi g
   | _ -> ()
  )


(********* ENVIRONMENTS ***************)

(* The environment is kept in two distinct data structures. A hash table maps
 * each original variable name into a varinfo (for variables, or an
 * enumeration tag, or a type). (Note that the varinfo might contain an
 * alpha-converted name different from that of the lookup name.) The Ocaml
 * hash tables can keep multiple mappings for a single key. Each time the
 * last mapping is returned and upon deletion the old mapping is restored. To
 * keep track of local scopes we also maintain a list of scopes (represented
 * as lists).  *)
type envdata =
    EnvVar of varinfo                   (* The name refers to a variable
                                         * (which could also be a function) *)
  | EnvEnum of enumitem                 (* the name refers to an enum item *)
  | EnvTyp of typ                       (* The name is of the form  "struct
                                         * foo", or "union foo" or "enum foo"
                                         * and refers to a type. Note that
                                         * the name of the actual type might
                                         * be different from foo due to alpha
                                         * conversion *)
  | EnvLabel of string                  (* The name refers to a label. This
                                         * is useful for GCC's locally
                                         * declared labels. The lookup name
                                         * for this category is "label foo" *)

let env  = Datatype.String.Hashtbl.create 307
(* ghost environment: keep track of all symbols, in the order
   in which they have been introduced. Superset of env *)
let ghost_env = Datatype.String.Hashtbl.create 307
(* We also keep a global environment. This is always a subset of the env *)
let global_env = Datatype.String.Hashtbl.create 307
(* ghost global environment: superset of global and subset of ghost *)
let ghost_global_env = Datatype.String.Hashtbl.create 307

(* maps a C label to the ghost environment of variables in scope
   at this program point. Used for typing \at() terms and predicates. *)
let label_env = Datatype.String.Hashtbl.create 307

let add_label_env lab =
  let add_if_absent v (d,_) map =
    match d with
    | EnvVar vi when not (Datatype.String.Map.mem v map) ->
      Datatype.String.Map.add v vi map
    | _ -> map
  in
  let open Datatype.String.Hashtbl in
  let lab_env = fold add_if_absent ghost_env Datatype.String.Map.empty in
  add label_env lab lab_env

let remove_label_env lab =
  Datatype.String.Hashtbl.remove label_env lab

(* In the scope we keep the original name, so we can remove them from the
 * hash table easily *)
type undoScope =
    UndoRemoveFromEnv of bool * string (* boolean indicates whether we should
                                          remove from ghost env only, or both.*)
  | UndoAlphaEnv of location Alpha.undoAlphaElement list

let scopes :  undoScope list ref list ref = ref []

(* tries to estimate if the name 's' was declared in the current scope;
   note that this may not work in all cases *)
let declared_in_current_scope ~ghost s =
  match !scopes with
  | [] -> (* global scope *)
    let env = if ghost then ghost_global_env else global_env in
    Datatype.String.Hashtbl.mem env s
  | cur_scope :: _ ->
    let names_declared_in_current_scope =
      List.filter_map
        (function
          | UndoRemoveFromEnv (ghost',s) when ghost || not ghost' -> Some s
          | _ -> None)
        !cur_scope