(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2022                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- ACSL Translation                                                   --- *)
(* --- LogicSemantics and LogicCompiler are mutually recursive (cycle     --- *)
(* --- closed by "boostrap*" function                                     --- *)
(* -------------------------------------------------------------------------- *)

open Cil_types
open Cil_datatype
open LogicBuiltins
open Clabels
open Ctypes
open Lang
open Lang.F
open Definitions
open Sigs

module Make(M : Sigs.Model) =
struct

  module M = M
  open M

  type loc = M.loc
  type value = loc Sigs.value
  type logic = loc Sigs.logic
  type result = loc Sigs.result
  type region = loc Sigs.region
  type sigma = Sigma.t

  module L = Cvalues.Logic(M)
  module C = LogicCompiler.Make(M)

  (* -------------------------------------------------------------------------- *)
  (* --- Frames                                                             --- *)
  (* -------------------------------------------------------------------------- *)

  type call = C.call
  type frame = C.frame
  let pp_frame = C.pp_frame
  let get_frame = C.get_frame
  let mk_frame = C.mk_frame
  let in_frame = C.in_frame
  let mem_frame = C.mem_frame
  let has_at_frame = C.has_at_frame
  let mem_at_frame = C.mem_at_frame
  let set_at_frame = C.set_at_frame
  let mem_at = C.mem_at
  let env_at = C.env_at
  let local = C.local
  let frame = C.frame
  let call = C.call
  let call_pre = C.call_pre
  let call_post = C.call_post
  let return = C.return
  let result = C.result
  let status = C.status
  let guards = C.guards

  (* -------------------------------------------------------------------------- *)
  (* --- Translation Environment & Recursion                                --- *)
  (* -------------------------------------------------------------------------- *)

  type env = C.env
  let mk_env = C.mk_env
  let move_at = C.move_at
  let current = C.current

  let logic_of_value = function
    | Val e -> Vexp e
    | Loc l -> Vloc l

  let loc_of_term env t =
    match C.logic env t with
    | Vexp e -> M.pointer_loc e
    | Vloc l -> l
    | _ ->
      Warning.error "Non-expected set of locations (%a)" Printer.pp_term t

  let val_of_term env t =
    match C.logic env t with
    | Vexp e -> e
    | Vloc l -> M.pointer_val l
    | Vset s -> Vset.concretize s
    | Lset _ ->
      Warning.error "Non-expected set of values (%a)" Printer.pp_term t

  let set_of_term env t = L.vset (C.logic env t)

  let collection_of_term env t =
    let v = C.logic env t in
    match v with
    | Vexp s when Logic_typing.is_set_type t.term_type ->
      let te = Logic_typing.type_of_set_elem t.term_type in
      Vset [Vset.Set(tau_of_ltype te,s)]
    | w -> w

  let term env t =
    match C.logic env t with
    | Vexp e -> e
    | Vloc l -> M.pointer_val l
    | s -> Vset.concretize (L.vset s)

  (* -------------------------------------------------------------------------- *)
  (* --- Accessing an Offset (sub field-index in a compound)                --- *)
  (* -------------------------------------------------------------------------- *)

  let rec access_offset env (v:logic) = function
    | TNoOffset -> v
    | TModel _ -> Wp_parameters.not_yet_implemented "Model field"
    | TField(f,offset) ->
      let v_f = L.map (fun r -> e_getfield r (Cfield (f, KValue))) v in
      access_offset env v_f offset
    | TIndex(k,offset) ->
      let rk = C.logic env k in
      let v_k = L.apply e_get v rk in
      access_offset env v_k offset

  (* -------------------------------------------------------------------------- *)
  (* --- Updating an Offset (sub field-index in a compound)                 --- *)
  (* -------------------------------------------------------------------------- *)

  let rec update_offset env (r:term) offset (v:term) = match offset with
    | TNoOffset -> v
    | TModel _ -> Wp_parameters.not_yet_implemented "Model field"
    | TField(f,offset) ->
      let r_f = e_getfield r (Cfield (f, KValue)) in
      let r_fv = update_offset env r_f offset v in
      e_setfield r (Cfield (f, KValue)) r_fv
    | TIndex(k,offset) ->
      let k = val_of_term env k in
      let r_kv = update_offset env (e_get r k) offset v in
      e_set r k r_kv

  (* -------------------------------------------------------------------------- *)
  (* --- Shifting Location of an Offset (pointer shift)                     --- *)
  (* -------------------------------------------------------------------------- *)

  (* typ is logic-type of (load v) *)
  let rec logic_offset env typ (v:logic) = function
    | TNoOffset -> typ , v
    | TModel _ -> Wp_parameters.not_yet_implemented "Model field"
    | TField(f,offset) ->
      logic_offset env f.ftype (L.field v f) offset
    | TIndex(k,offset) ->
      let te = Cil.typeOf_array_elem typ in
      let size = Ctypes.get_array_size (Ctypes.object_of typ) in
      let obj = Ctypes.object_of te in
      let vloc = L.shift v obj ?size (C.logic env k) in
      logic_offset env te vloc offset

  (* -------------------------------------------------------------------------- *)
  (* --- Logic Variable                                                     --- *)
  (* -------------------------------------------------------------------------- *)

  type lv_value =
    | VAL of logic
    | VAR of varinfo

  let logic_var env lv =
    match lv.lv_origin with
    | None -> VAL (C.logic_var env lv)
    | Some x ->
      if x.vformal then match C.formal x with
        | Some v -> VAL (logic_of_value v)
        | None -> VAR x
      else VAR x

  (* -------------------------------------------------------------------------- *)
  (* --- Term L-Values (this means 'loading' the l-value)                   --- *)
  (* -------------------------------------------------------------------------- *)

  let load_loc env typ loc loffset =
    let te,lp = logic_offset env typ (Vloc loc) loffset in
    L.load (C.current env) (Ctypes.object_of te) lp

  let term_lval env (lhost,loffset) =
    match lhost with
    | TResult ty ->
      begin match C.result () with
        | Sigs.R_var x ->
          access_offset env (Vexp (e_var x)) loffset
        | Sigs.R_loc l ->
          load_loc env ty l loffset
      end
    | TMem e ->
      let te = Logic_typing.ctype_of_pointed e.term_type in
      let te , lp = logic_offset env te (C.logic env e) loffset in
      L.load (C.current env) (Ctypes.object_of te) lp
    | TVar{lv_name="\\exit_status"} ->
      assert (loffset = TNoOffset) ; (* int ! *)
      Vexp (e_var (C.status ()))
    | TVar lv ->
      begin
        match logic_var env lv with
        | VAL v -> access_offset env v loffset
        | VAR x -> load_loc env x.vtype (M.cvar x) loffset
      end

  (* -------------------------------------------------------------------------- *)
  (* --- Address of L-Values                                                --- *)
  (* -------------------------------------------------------------------------- *)

  let logic_lval env (lhost,loffset) =
    match lhost with
    | TResult ty ->
      begin match C.result () with
        | R_loc l ->
          logic_offset env ty (Vloc l) loffset
        | R_var _ ->
          Wp_parameters.abort ~current:true "Address of \\result"
      end
    | TMem e ->
      let te = Logic_typing.ctype_of_pointed e.term_type in
      logic_offset env te (C.logic env e) loffset
    | TVar lv ->
      begin
        match logic_var env lv with
        | VAL v ->
          Wp_parameters.abort ~current:true
            "Address of logic value (%a)@." (Cvalues.pp_logic M.pretty) v
        | VAR x ->
          logic_offset env x.vtype (Vloc (M.cvar x)) loffset
      end

  let addr_lval env lv = snd (logic_lval env lv)

  let lval env lv =
    let te,ve = logic_lval env lv in
    match ve with
    | Vexp e -> te , M.pointer_loc e
    | Vloc l -> te , l
    | _ ->
      Wp_parameters.abort ~current:true "Unexpected set (%a)"
        Printer.pp_term_lval lv

  (* -------------------------------------------------------------------------- *)
  (* --- Unary Operators                                                    --- *)
  (* -------------------------------------------------------------------------- *)

  (* Only integral *)
  let term_unop = function
    | Neg -> L.map_opp
    | BNot -> L.map Cint.l_not
    | LNot -> L.map e_not

  (* -------------------------------------------------------------------------- *)
  (* --- Equality                                                           --- *)
  (* -------------------------------------------------------------------------- *)

  type eqsort =
    | EQ_set
    | EQ_loc
    | EQ_plain
    | EQ_float of c_float
    | EQ_array of matrixinfo
    | EQ_comp of compinfo
    | EQ_incomparable

  and matrixinfo = c_object * int option list

  let eqsort_of_type t =
    match Logic_utils.unroll_type ~unroll_typedef:false t with
    | Ltype({lt_name="set"},[_]) -> EQ_set
    | Linteger | Lreal | Lvar _ | Larrow _ | Ltype _ -> EQ_plain
    | Ctype t ->
      match Ctypes.object_of t with
      | C_pointer _ -> EQ_loc
      | C_int _ -> EQ_plain
      | C_float f -> EQ_float f
      | C_comp c -> EQ_comp c
      | C_array a -> EQ_array (Ctypes.array_dimensions a)

  let eqsort_of_comparison a b =
    match eqsort_of_type a.term_type , eqsort_of_type b.term_type with
    | EQ_set , _ | _ , EQ_set -> EQ_set
    | EQ_loc , EQ_loc -> EQ_loc
    | EQ_comp c1 , EQ_comp c2 ->
      if Compinfo.equal c1 c2 then EQ_comp c1 else EQ_incomparable
    | EQ_array(t1,d1) , EQ_array(t2,d2) ->
      if Ctypes.equal t1 t2 then
        match Matrix.merge d1 d2 with
        | Some d -> EQ_array(t1,d)
        | None -> EQ_incomparable
      else EQ_incomparable
    | EQ_plain , EQ_plain -> EQ_plain
    | EQ_float f1 , EQ_float f2 when f1 = f2 -> EQ_float f1
    | _ -> EQ_incomparable

  let use_equal = function
    | `Negative -> Wp_parameters.ExtEqual.get ()
    | `Positive | `NoPolarity -> false

  let term_equal polarity env a b =
    match eqsort_of_comparison a b with

    | EQ_set ->
      let sa = set_of_term env a in
      let sb = set_of_term env b in
      (* TODO: should be parametric in the equality of elements *)
      Vset.equal sa sb

    | EQ_loc ->
      let la = loc_of_term env a in
      let lb = loc_of_term env b in
      M.loc_eq la lb

    | EQ_comp c ->
      let va = val_of_term env a in
      let vb = val_of_term env b in
      if use_equal polarity
      then p_equal va vb
      else Cvalues.equal_comp c va vb

    | EQ_array m ->
      let va = val_of_term env a in
      let vb = val_of_term env b in
      if use_equal polarity
      then p_equal va vb
      else Cvalues.equal_array m va vb

    | EQ_float f ->
      Cfloat.feq f (val_of_term env a) (val_of_term env b)

    | EQ_plain ->
      p_equal (val_of_term env a) (val_of_term env b)

    | EQ_incomparable ->
      (* incomparable terms *)
      Warning.error
        "@[Incomparable terms:@ type %a with@ type %a@]"
        Printer.pp_logic_type a.term_type
        Printer.pp_logic_type b.term_type

  let term_diff polarity env a b =
    p_not (term_equal (Cvalues.negate polarity) env a b)


  let float_of_logic_type lt =
    match Logic_utils.unroll_type lt with
    | Ctype ty ->
      (match Cil.unrollType ty with
       | TFloat(f,_) -> Some (Ctypes.c_float f)
       | _ -> None)
    | _ -> None

  let compare_term env vrel lrel frel a b =
    if Logic_typing.is_pointer_type a.term_type then
      lrel (loc_of_term env a) (loc_of_term env b)
    else match float_of_logic_type a.term_type with
      | Some f -> frel f (val_of_term env a) (val_of_term env b)
      | None -> vrel (val_of_term env a) (val_of_term env b)

  (* -------------------------------------------------------------------------- *)
  (* --- Term Comparison                                                    --- *)
  (* -------------------------------------------------------------------------- *)

  let exp_equal env a b =
    Vexp(e_prop (term_equal `NoPolarity env a b))

  let exp_diff env a b =
    Vexp(e_prop (term_diff `NoPolarity env a b))

  let exp_compare env vrel lrel frel a b =
    Vexp(e_prop (compare_term env vrel lrel frel a b))

  (* -------------------------------------------------------------------------- *)
  (* --- Binary Operators                                                   --- *)
  (* -------------------------------------------------------------------------- *)

  let toreal t v =
    if t then L.map Cmath.real_of_int v else v

  let arith env fint freal a b =
    let va = C.logic env a in
    let vb = C.logic env b in
    let ta = Logic_typing.is_integral_type a.term_type in
    let tb = Logic_typing.is_integral_type b.term_type in
    if ta && tb
    then fint va vb
    else freal (toreal ta va) (toreal tb vb)

  let rec fold_assoc bop acc ts =
    match ts with
    | [] -> acc
    | t::others ->
      match t.term_node with
      | TBinOp(binop,a,b) when bop == binop ->
        fold_assoc bop acc (a::b::others)
      | _  -> fold_assoc bop (t::acc) others

  let term_binop env binop a b =
    match binop with
    | PlusA -> arith env L.apply_add (L.apply F.e_add) a b
    | MinusA -> arith env L.apply_sub (L.apply F.e_sub) a b
    | Mult -> arith env (L.apply e_mul) (L.apply F.e_mul) a b
    | Div -> arith env (L.apply e_div) (L.apply F.e_div) a b
    | Mod -> L.apply e_mod (C.logic env a) (C.logic env b)
    | PlusPI ->
      let va = C.logic env a in
      let vb = C.logic env b in
      let te = Logic_typing.ctype_of_pointed a.term_type in
      L.shift va (Ctypes.object_of te) vb
    | MinusPI ->
      let va = C.logic env a in
      let vb = C.logic env b in
      let te = Logic_typing.ctype_of_pointed a.term_type in
      L.shift va (Ctypes.object_of te) (L.map_opp vb)
    | MinusPP ->
      let te = Logic_typing.ctype_of_pointed a.term_type in
      let la = loc_of_term env a in
      let lb = loc_of_term env b in
      Vexp(M.loc_diff (Ctypes.object_of te) la lb)
    | Shiftlt -> L.apply Cint.l_lsl (C.logic env a) (C.logic env b)
    | Shiftrt -> L.apply Cint.l_lsr (C.logic env a) (C.logic env b)
    | BAnd -> L.apply Cint.l_and (C.logic env a) (C.logic env b)
    | BXor -> L.apply Cint.l_xor (C.logic env a) (C.logic env b)
    | BOr -> L.apply Cint.l_or (C.logic env a) (C.logic env b)
    | LAnd -> Vexp(e_and (List.map (val_of_term env) (fold_assoc LAnd [] [a;b])))
    | LOr  -> Vexp(e_or  (List.map (val_of_term env) (fold_assoc LOr  [] [a;b])))
    | Lt -> exp_compare env p_lt M.loc_lt Cfloat.flt a b
    | Gt -> exp_compare env p_lt M.loc_lt Cfloat.flt b a
    | Le -> exp_compare env p_leq M.loc_leq Cfloat.fle a b
    | Ge -> exp_compare env p_leq M.loc_leq Cfloat.fle b a
    | Eq -> exp_equal env a b
    | Ne -> exp_diff env a b

  (* -------------------------------------------------------------------------- *)
  (* --- Term Cast                                                          --- *)
  (* -------------------------------------------------------------------------- *)

  type cvsort =
    | L_bool
    | L_real
    | L_integer
    | L_cint of c_int
    | L_cfloat of c_float
    | L_pointer of typ
    | L_array of arrayinfo

  let rec cvsort_of_ltype src_ltype =
    match Logic_utils.unroll_type ~unroll_typedef:false src_ltype with
    | Linteger -> L_integer
    | Lreal -> L_real
    | Ctype src_ctype ->
      begin
        match Ctypes.object_of src_ctype with
        | C_int i -> L_cint i
        | C_float f -> L_cfloat f
        | C_pointer te -> L_pointer te
        | C_array a -> L_array a (* into the logic, C array = logic array *)
        | C_comp c when c.cstruct ->
          Warning.error "@[Logic cast from struct (%a) not implemented yet@]"
            Printer.pp_typ src_ctype
        | C_comp _ ->
          Warning.error "@[Logic cast from union (%a) not implemented yet@]"
            Printer.pp_typ src_ctype
      end
    | Ltype _ as b when Logic_const.is_boolean_type b -> L_bool
    | Ltype({lt_name="set"},[elt_ltype]) -> (* lifting or set of elements ? *)
      cvsort_of_ltype elt_ltype
    | (Ltype _ | Lvar _ | Larrow _) as typ ->
      Warning.error "@[Logic cast from (%a) not implemented yet@]"
        Printer.pp_logic_type typ

  (** cast to a C type *)
  let term_cast_to_ctype env dst_ctype t =
    let cast_ptr ty t0 =
      let value = C.logic env t in
      let o_src = Ctypes.object_of t0 in
      let o_dst = Ctypes.object_of ty in
      if Ctypes.compare o_src o_dst = 0
      then value
      else L.map_loc (M.cast { pre=o_src ; post=o_dst }) value
    in
    match Ctypes.object_of dst_ctype , cvsort_of_ltype t.term_type with
    (* Cast to C integers from ...*)
    | C_int _ , L_bool ->
      L.map Cvalues.bool_val (C.logic env t)
    | C_int i , L_cint i0 ->
      let v = C.logic env t in
      if (Ctypes.sub_c_int i0 i) then v
      else L.map (Cint.convert i) v
    | C_int i , L_integer ->
      L.map (Cint.convert i) (C.logic env t)
    | C_int i , L_pointer _ ->
      L.map_l2t (M.int_of_loc i) (C.logic env t)
    | C_int i , L_real ->
      L.map (Cint.of_real i) (C.logic env t)
    | C_int i , L_cfloat f ->
      L.map (fun v -> Cint.of_real i (Cfloat.real_of_float f v)) (C.logic env t)
    | C_int _, L_array _ ->
      Warning.error "@[Logic cast to sized integer (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
    (* Cast to C float from ... *)
    | C_float f , L_real ->
      L.map (Cfloat.float_of_real f) (C.logic env t)
    | C_float ft,  L_cfloat ff ->
      let map v = if Ctypes.equal_float ff ft then v else Cfloat.float_of_real ft (Cfloat.real_of_float ff v) in
      L.map map (C.logic env t)
    | C_float f , (L_cint _ | L_integer) ->
      L.map (Cfloat.float_of_int f) (C.logic env t)
    | C_float _, (L_bool|L_pointer _|L_array _) ->
      Warning.error "@[Logic cast to float (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
    (* Cast to C pointer from ...  *)
    | C_pointer ty , (L_integer | L_cint _) ->
      let obj = Ctypes.object_of ty in
      L.map_t2l (M.loc_of_int obj) (C.logic env t)
    | C_pointer ty , L_pointer t0 ->
      cast_ptr ty t0
    | C_pointer _, (L_bool|L_real|L_cfloat _|L_array _) ->
      Warning.error "@[Logic cast to pointer (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
    (* Cast to C array from ... *)
    | C_array _, L_pointer t0 ->
      (* cast to an array `(T[])(p)` is equivalent
         to a deref of a cast to a pointer `*(T( * )[])(p)` *)
      let cast = cast_ptr dst_ctype t0 in
      L.load (C.current env) (Ctypes.object_of dst_ctype) cast
    | C_array dst_arr_info, L_array src_arr_info
      when Ctypes.AinfoComparable.equal dst_arr_info src_arr_info ->
      (* cast from/to the same type *)
      C.logic env t
    | C_array {arr_flat=Some _}, (L_integer|L_cint _|L_bool|L_real|L_cfloat _|L_array _) ->
      Warning.error "@[Logic cast to sized array (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
    | C_array {arr_flat=None}, (L_integer|L_cint _|L_bool|L_real|L_cfloat _|L_array _) ->
      Warning.error "@[Logic cast to unsized array (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
    (* Cast to C compound from ... *)
    | C_comp c, (L_integer|L_cint _|L_bool|L_real|L_cfloat _|L_array _|L_pointer _) when c.cstruct ->
      Warning.error "@[Logic cast to struct (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type
    | C_comp _, (L_integer|L_cint _|L_bool|L_real|L_cfloat _|L_array _|L_pointer _) ->
      Warning.error "@[Logic cast to union (%a) from (%a) not implemented yet@]"
        Printer.pp_typ dst_ctype Printer.pp_logic_type t.term_type

  let term_cast_to_real env t =
    let src_ltype = Logic_utils.unroll_type ~unroll_typedef:false t.term_type in
    match cvsort_of_ltype src_ltype with
    | L_cint _ ->
      L.map (fun x -> Cmath.real_of_int (Cint.to_integer x)) (C.logic env t)
    | L_integer ->
      L.map Cmath.real_of_int (C.logic env t)
    | L_cfloat f ->
      L.map (Cfloat.real_of_float f) (C.logic env t)
    | L_real -> C.logic env t
    | L_bool|L_pointer _|L_array _ ->
      Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
        Printer.pp_logic_type src_ltype Printer.pp_logic_type Lreal

  let term_cast_to_integer env t =
    let src_ltype = Logic_utils.unroll_type ~unroll_typedef:false t.term_type in
    match cvsort_of_ltype src_ltype with
    | L_real ->
      L.map Cmath.int_of_real (C.logic env t)
    | L_cint _ ->
      L.map Cint.to_integer (C.logic env t)
    | L_integer -> C.logic env t
    | L_cfloat f ->
      L.map
        (fun x -> Cmath.int_of_real (Cfloat.real_of_float f x))
        (C.logic env t)
    | L_bool ->
      L.map Cmath.bool_of_int (C.logic env t)
    | L_pointer _|L_array _ ->
      Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
        Printer.pp_logic_type src_ltype Printer.pp_logic_type Linteger

  let term_cast_to_boolean env t =
    let src_ltype = Logic_utils.unroll_type ~unroll_typedef:false t.term_type in
    match cvsort_of_ltype src_ltype with
    | L_bool -> C.logic env t
    | L_integer | L_cint _ ->
      L.map Cmath.int_of_bool (C.logic env t)
    | L_real | L_cfloat _ | L_pointer _ | L_array _ ->
      Warning.error "@[Logic cast from (%a) to (%a) not implemented yet@]"
        Printer.pp_logic_type src_ltype Printer.pp_logic_type Logic_const.boolean_type

  let rec term_cast_to_ltype env dst_ltype t =
    match Logic_utils.unroll_type ~unroll_typedef:false dst_ltype with
    | Ctype typ-> term_cast_to_ctype env typ t
    | Linteger -> term_cast_to_integer env t
    | Lreal -> term_cast_to_real env t
    | Ltype _ as b when Logic_const.is_boolean_type b -> term_cast_to_boolean env t
    | Ltype({lt_name="set"},[elt_ltype]) -> (* lifting, set of elements ? *)
      term_cast_to_ltype env elt_ltype t
    | (Ltype _ | Lvar _ | Larrow _) as dst_ltype ->
      let src_ltype = Logic_utils.unroll_type ~unroll_typedef:false t.term_type in
      Warning.error "@[Logic cast to (%a) from (%a) not implemented yet@]"
        Printer.pp_logic_type dst_ltype Printer.pp_logic_type src_ltype


  (* -------------------------------------------------------------------------- *)
  (* --- Environment Binding                                                --- *)
  (* -------------------------------------------------------------------------- *)

  let bind_quantifiers (env:env) qs =
    let rec acc xs env hs = function
      | [] -> List.rev xs , env , hs
      | v::vs ->
        let t = Lang.tau_of_ltype v.lv_type in
        let x = Lang.freshvar ~basename:v.lv_name t in
        let h =
          if Wp_parameters.SimplifyForall.get ()
          then F.p_true
          else C.has_ltype v.lv_type (e_var x)
        in
        let e = C.env_let env v (Vexp (e_var x)) in
        acc (x::xs) e (h::hs) vs in
    acc [] env [] qs

  (* -------------------------------------------------------------------------- *)
  (* --- Undefined Term                                                     --- *)
  (* -------------------------------------------------------------------------- *)

  let term_undefined t =
    let x = Lang.freshvar ~basename:"w" (Lang.tau_of_ltype t.term_type) in
    Cvalues.plain t.term_type (e_var x)

  (* -------------------------------------------------------------------------- *)
  (* --- Term Nodes                                                         --- *)
  (* -------------------------------------------------------------------------- *)

  let term_node (env:env) t =
    match t.term_node with
    | TConst c -> Vexp (Cvalues.logic_constant c)
    | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
      Vexp (Cvalues.constant_term t)

    | TLval lval ->
      if Cil.isVolatileTermLval lval &&
         Cvalues.volatile ~warn:"unsafe volatile access to (term) l-value" ()
      then term_undefined t
      else term_lval env lval
    | TAddrOf lval -> addr_lval env lval
    | TStartOf lval ->
      begin
        let lt = Cil.typeOfTermLval lval in
        let base = addr_lval env lval in
        match Logic_utils.unroll_type lt with
        | Ctype ct ->
          L.map_loc (fun l -> Cvalues.startof ~shift:M.shift l ct) base
        | _ -> base
      end

    | TUnOp(Neg,t) when not (Logic_typing.is_integral_type t.term_type) ->
      L.map F.e_opp (C.logic env t)
    | TUnOp(unop,t) -> term_unop unop (C.logic env t)
    | TBinOp(binop,a,b) -> term_binop env binop a b

    | TCastE(ty,t) -> term_cast_to_ctype env ty t
    | TLogic_coerce(typ,t) -> term_cast_to_ltype env typ t

    | Tapp(f,ls,ts) ->
      let vs = List.map (val_of_term env) ts in
      let result = Lang.tau_of_ltype t.term_type in
      let r = match LogicBuiltins.logic f with
        | ACSLDEF -> C.call_fun env result f ls vs
        | HACK phi -> phi vs
        | LFUN f -> e_fun ~result f vs
      in Vexp r

    | Tlambda _ ->
      Warning.error "Lambda-functions not yet implemented"

    | TDataCons({ctor_name="\\true"},_) -> Vexp(e_true)
    | TDataCons({ctor_name="\\false"},_) -> Vexp(e_false)

    | TDataCons(c,ts) ->
      let es = List.map (val_of_term env) ts in
      let r = match LogicBuiltins.ctor c with
        | ACSLDEF -> e_fun (CTOR c) es
        | HACK phi -> phi es
        | LFUN f -> e_fun f es ~result:(Lang.tau_of_ltype t.term_type)
      in Vexp r

    | Tif( cond , a , b ) ->
      let c = val_of_term env cond in
      let a = val_of_term env a in
      let b = val_of_term env b in
      Vexp (e_if c a b)

    | Tat( t , label ) ->
      let clabel = Clabels.of_logic label in
      C.logic (C.env_at env clabel) t

    | Tbase_addr (label,t) ->
      ignore label ;
      L.map_loc M.base_addr (C.logic env t)

    | Toffset (label,t) ->
      ignore label ;
      L.map_l2t M.base_offset (C.logic env t)

    | Tblock_length (label,t) ->
      let obj = object_of (Logic_typing.ctype_of_pointed t.term_type) in
      let sigma = C.mem_at env (of_logic label) in
      L.map_l2t (M.block_length sigma obj) (C.logic env t)

    | Tnull ->
      Vloc M.null

    | TUpdate(a,offset,b) ->
      Vexp (update_offset env (val_of_term env a) offset (val_of_term env b))

    | Tempty_set -> Vset []
    | Tunion ts ->
      L.union t.term_type (List.map (collection_of_term env) ts)
    | Tinter ts ->
      L.inter t.term_type (List.map (collection_of_term env) ts)
    | Tcomprehension(t,qs,cond) ->
      begin
        let xs,env,domain = bind_quantifiers env qs in
        let condition = match cond with
          | None -> p_conj domain
          | Some p ->
            let cc = C.pred `NoPolarity env in
            let p = Lang.without_assume cc p in
            p_conj (p :: domain)
        in match C.logic env t with
        | Vexp e -> Vset[Vset.Descr(xs,e,condition)]
        | Vloc l -> Lset[Sdescr(xs,l,condition)]
        | _ -> Wp_parameters.fatal "comprehension set of sets"
      end

    | Tlet( { l_var_info=v ; l_body=LBterm a } , b ) ->
      let va = C.logic env a in
      C.logic (C.env_let env v va) b

    | Tlet _ ->
      Warning.error "Complex let-binding not implemented yet (%a)"
        Printer.pp_term t

    | Trange(a,b) ->
      let bound env = function
        | None -> None
        | Some x -> Some (val_of_term env x)
      in Vset(Vset.range (bound env a) (bound env b))

    | Ttypeof _ | Ttype _ ->
      Warning.error "Type tag not implemented yet"

  (* -------------------------------------------------------------------------- *)
  (* --- Separated                                                          --- *)
  (* -------------------------------------------------------------------------- *)

  let separated_terms env ts =
    L.separated
      begin
        List.map
          (fun t ->
             let te = Logic_typing.ctype_of_pointed t.term_type in
             let obj = Ctypes.object_of te in
             L.region obj (C.logic env t)
          ) ts
      end

  (* -------------------------------------------------------------------------- *)
  (* --- Relations                                                          --- *)
  (* -------------------------------------------------------------------------- *)

  let relation polarity env rel a b =
    match rel with
    | Rlt -> compare_term env p_lt M.loc_lt Cfloat.flt a b
    | Rgt -> compare_term env p_lt M.loc_lt Cfloat.flt b a
    | Rle -> compare_term env p_leq M.loc_leq Cfloat.fle a b
    | Rge -> compare_term env p_leq M.loc_leq Cfloat.fle b a
    | Req -> term_equal polarity env a b
    | Rneq -> term_diff polarity env a b

  (* -------------------------------------------------------------------------- *)
  (* --- Predicates                                                         --- *)
  (* -------------------------------------------------------------------------- *)

  let valid env acs label t =
    let te = Logic_typing.ctype_of_pointed t.term_type in
    let sigma = C.mem_at env (Clabels.of_logic label) in
    let addrs = C.logic env t in
    p_all (L.valid sigma acs) (L.region (Ctypes.object_of te) addrs)

  let initialized env label t =
    let te = Logic_typing.ctype_of_pointed t.term_type in
    let sigma = C.mem_at env (Clabels.of_logic label) in
    let addrs = C.logic env t in
    p_all (L.initialized sigma) (L.region (Ctypes.object_of te) addrs)

  let call_pred env f ls es =
    match C.logic_info env f with
    | Some p ->
      if ls <> [] || es <> [] then
        Warning.error "Unexpected parameters for named predicate '%a'"
          Logic_info.pretty f ; p
    | None ->
      let empty ls =
        if ls <> [] then
          Warning.error "Unexpected labels for purely logic '%a'"
            Logic_info.pretty f ;
      in
      match LogicBuiltins.logic f with
      | ACSLDEF -> C.call_pred env f ls es
      | HACK phi -> empty ls ; F.p_bool (phi es)
      | LFUN p -> empty ls ; p_call p es

  let predicate polarity env p =
    match p.pred_content with
    | Pfalse -> p_false
    | Ptrue -> p_true
    | Pseparated ts -> separated_terms env ts
    | Prel(rel,a,b) -> relation polarity env rel a b
    | Pand(a,b) -> p_and (C.pred polarity env a) (C.pred polarity env b)
    | Por(a,b)  -> p_or (C.pred polarity env a) (C.pred polarity env b)
    | Pxor(a,b) -> p_not (p_equiv (C.pred `NoPolarity env a) (C.pred `NoPolarity env b))
    | Pimplies(a,b) ->
      let negated = Cvalues.negate polarity in
      p_imply (C.pred negated env a) (C.pred polarity env b)
    | Piff(a,b) -> p_equiv (C.pred `NoPolarity  env a) (C.pred `NoPolarity  env b)
    | Pnot a -> p_not (C.pred (Cvalues.negate polarity) env a)
    | Pif(t,a,b) ->
      p_if (p_bool (val_of_term env t))
        (C.pred polarity env a)
        (C.pred polarity env b)
    | Papp({l_var_info = {lv_name = "\\subset"}},_,ts) ->
      begin match ts with
        | [a;b] -> L.subset
                     a.term_type (C.logic env a)
                     b.term_type (C.logic env b)
        | _ -> Warning.error "\\subset requires 2 arguments"
      end
    | Papp(f,ls,ts) ->
      call_pred env f ls @@ List.map (val_of_term env) ts

    | Plet( { l_var_info=v ; l_body=LBterm a } , p ) ->
      let va = C.logic env a in
      C.pred polarity (C.env_let env v va) p

    | Plet( { l_var_info=v ; l_body=LBpred q } , p ) ->
      let vq = C.pred `NoPolarity env q in
      C.pred polarity (C.env_letp env v vq) p

    | Plet _ ->
      Warning.error "Complex let-inding not implemented yet (%a)"
        Printer.pp_predicate p

    | Pforall(qs,p) ->
      let xs,env,hs = bind_quantifiers env qs in
      let p = Lang.without_assume (C.pred polarity env) p in
      p_forall xs (p_hyps hs p)

    | Pexists(qs,p) ->
      let xs,env,hs = bind_quantifiers env qs in
      let p = Lang.without_assume (C.pred polarity env) p in
      p_exists xs (p_conj (p :: hs))

    | Pat(p,label) ->
      let clabel = Clabels.of_logic label in
      C.pred polarity (C.env_at env clabel) p

    | Pvalid(label,t) -> valid env RW label t
    | Pvalid_read(label,t) -> valid env RD label t
    | Pobject_pointer(label,t) -> valid env OBJ label t

    | Pinitialized(label, t) -> initialized env label t

    | Pvalid_function _t ->
      Warning.error
        "\\valid_function not yet implemented@\n\
         @[<hov 0>(%a)@]" Printer.pp_predicate p

    | Pallocable _ | Pfreeable _ | Pfresh _ | Pdangling _ ->
      Warning.error
        "Allocation, initialization and danglingness not yet implemented@\n\
         @[<hov 0>(%a)@]" Printer.pp_predicate p


  (* -------------------------------------------------------------------------- *)
  (* --- Set of locations for a term representing a set of l-values         --- *)
  (* -------------------------------------------------------------------------- *)

  let assignable_lval env lv =
    match fst lv with
    | TResult _  | TVar{lv_name="\\exit_status"} -> [] (* special case ! *)
    | _ ->
      let obj = Ctypes.object_of_logic_type (Cil.typeOfTermLval lv) in
      L.region obj (addr_lval env lv)

  let assignable env t =
    match t.term_node with
    | Tempty_set -> []
    | TLval lv -> assignable_lval env lv
    | Tunion ts -> List.concat (List.map (C.region env) ts)
    | Tinter _ -> Warning.error "Intersection in assigns not implemented yet"
    | Tcomprehension(t,qs,cond) ->
      begin
        let xs,env,domain = bind_quantifiers env qs in
        let conditions = match cond with
          | None -> domain
          | Some p -> C.pred `NoPolarity env p :: domain
        in
        List.map
          (function (obj,sloc) ->
             obj , match sloc with
             | Sloc l -> Sdescr(xs,l,p_conj conditions)
             | (Sarray _ | Srange _ | Sdescr _) as sloc ->
               let ys,l,extend = L.rdescr sloc in
               Sdescr(xs@ys,l,p_conj (extend :: conditions))
          ) (C.region env t)
      end

    | Tat(t,label) ->
      C.region (C.env_at env (Clabels.of_logic label)) t

    | Tlet( { l_var_info=v ; l_body=LBterm a } , b ) ->
      let va = C.logic env a in
      C.region (C.env_let env v va) b

    | Tlet _ ->
      Warning.error "Complex let-binding not implemented yet (%a)"
        Printer.pp_term t

    | TCastE (_,t)
    | TLogic_coerce(_,t) -> C.region env t

    | TBinOp _ | TUnOp _ | Trange _ | TUpdate _ | Tapp _ | Tif _
    | TConst _ | Tnull | TDataCons _ | Tlambda _
    | Ttype _ | Ttypeof _
    | TAlignOfE _ | TAlignOf _ | TSizeOfStr _ | TSizeOfE _ | TSizeOf _
    | Tblock_length _ | Tbase_addr _ | Toffset _ | TAddrOf _ | TStartOf _
      -> Wp_parameters.abort ~current:true
           "Non-assignable term (%a)" Printer.pp_term t

  (* -------------------------------------------------------------------------- *)
  (* --- Protection                                                         --- *)
  (* -------------------------------------------------------------------------- *)

  let term_protected env t =
    Warning.handle
      ~handler:term_undefined
      ~severe:false
      ~effect:"Hide sub-term definition"
      (term_node env) t

  let pred_protected polarity env p =
    match polarity with
    | `Positive ->
      Warning.handle
        ~effect:"Target turned to False"
        ~severe:true ~handler:(fun _ -> p_false)
        (predicate `Positive env) p
    | `Negative ->
      Warning.handle
        ~effect:"Ignored Hypothesis"
        ~severe:false ~handler:(fun _ -> p_true)
        (predicate `Negative env) p
    | `NoPolarity ->
      predicate `NoPolarity env p

  (* -------------------------------------------------------------------------- *)
  (* --- Boot Strapping                                                     --- *)
  (* -------------------------------------------------------------------------- *)

  let term_trigger env t =
    let v = term_protected env t in
    if List.mem "TRIGGER" t.term_name then
      begin
        match v with
        | Vexp e -> C.trigger (Trigger.of_term e)
        | Vloc l -> C.trigger (Trigger.of_term (M.pointer_val l))
        | _ -> Wp_parameters.warning ~current:true
                 "Can not trigger on tset"
      end ; v

  let pred_trigger positive env np =
    let p = pred_protected positive env np in
    if List.mem "TRIGGER" np.Cil_types.pred_name then
      C.trigger (Trigger.of_pred p);
    p

  let pred polarity env p =
    Context.with_current_loc p.pred_loc (pred_trigger polarity env) p

  let logic env t =
    Context.with_current_loc t.term_loc (term_trigger env) t

  let region env t =
    Context.with_current_loc t.term_loc (assignable env) t

  let () = C.bootstrap_pred pred
  let () = C.bootstrap_term term
  let () = C.bootstrap_logic logic
  let () = C.bootstrap_region region

  let lemma = C.lemma

  (* -------------------------------------------------------------------------- *)
  (* --- Regions                                                            --- *)
  (* -------------------------------------------------------------------------- *)

  let assigned_of_lval env (lv : Cil_types.lval) =
    assignable_lval env (Logic_utils.lval_to_term_lval lv)

  let assigned_of_froms env froms =
    List.concat
      (List.map
         (fun ({it_content=wr},_deps) -> region env wr) froms)

  let assigned_of_assigns env = function
    | WritesAny -> None
    | Writes froms -> Some (assigned_of_froms env froms)

  let occurs_opt x = function None -> false | Some t -> F.occurs x t

  let occurs_sloc x = function
    | Sloc l -> M.occurs x l
    | Sarray(l,_,_) -> M.occurs x l
    | Srange(l,_,a,b) -> M.occurs x l || occurs_opt x a || occurs_opt x b
    | Sdescr(xs,l,p) ->
      if List.exists (Var.equal x) xs then false
      else (M.occurs x l || F.occursp x p)

  let occurs x region = List.exists (fun (_,s) -> occurs_sloc x s) region

  let vars_opt = function None -> Vars.empty | Some t -> F.vars t

  let vars_sloc = function
    | Sloc l
    | Sarray(l,_,_) ->
      M.vars l
    | Srange(l,_,a,b) ->
      Vars.union (M.vars l) (Vars.union (vars_opt a) (vars_opt b))
    | Sdescr(xs,l,p) ->
      List.fold_left
        (fun xs x -> Vars.remove x xs)
        (Vars.union (M.vars l) (F.varsp p)) xs

  let vars region =
    List.fold_left
      (fun xs (_,s) -> Vars.union xs (vars_sloc s)) Vars.empty region

  (* -------------------------------------------------------------------------- *)
  (* --- CheckAssigns                                                       --- *)
  (* -------------------------------------------------------------------------- *)

  let rec assignable_region unfold reg assignable =
    let inclusion = p_any (L.included reg) assignable in
    if unfold = 0 then inclusion
    else p_or inclusion (assignable_unfolded_region unfold reg assignable)

  (* Note that when a region cannot be unfolded anymore (that is, when it is a
     [Sloc] with atomic type, including unknown size arrays and opaque structs),
     the function return [p_false]. *)
  and assignable_unfolded_region unfold (obj, sloc) assignable =
    let range size = Some e_zero, Some (e_sub (e_int size) e_one) in
    match sloc with
    | Sloc loc ->
      begin match obj with
        | C_pointer _ | C_int _ | C_float _
        | C_comp { cfields = None } | C_array { arr_flat = None } ->
          (* Nothing to unfold *)
          p_false

        | C_comp { cfields = Some fields } ->
          let assignable_field f =
            let reg = Ctypes.object_of f.ftype, Sloc (M.field loc f) in
            assignable_region (unfold-1) reg assignable
          in
          p_conj (List.map assignable_field fields)

        | C_array { arr_flat = Some { arr_size=len ; arr_cell=typ } } ->
          let obj = Ctypes.object_of typ in
          assignable_unfolded_range unfold loc obj (range len) assignable
      end

    | Sarray (loc, obj, len) ->
      assignable_unfolded_range unfold loc obj (range len) assignable

    | Srange (loc, obj, b, e) ->
      assignable_unfolded_range unfold loc obj (b, e) assignable

    | Sdescr (xs, loc, guard) ->
      assignable_unfolded_descr unfold obj xs loc guard assignable

  and assignable_unfolded_range unfold loc obj (low, up) =
    let x = Lang.freshvar ~basename:"k" Lang.t_int in
    let k = e_var x in
    let guard = Vset.in_range k low up in
    let loc = M.shift loc obj k in
    assignable_unfolded_descr unfold obj [x] loc guard

  and assignable_unfolded_descr unfold obj xs loc guard assignable =
    p_forall xs
      (p_imply guard
         (assignable_region (unfold-1) (obj, Sloc loc) assignable))

  let check_assigns ~unfold sigma ~written ~assignable =
    p_all
      (fun reg ->
         p_imply
           (p_not (L.invalid sigma reg))
           (assignable_region unfold reg assignable)
      ) (written : region)

end