eval_terms.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2019                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         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).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype
open Locations
open Abstract_interp
open Cvalue
open Bit_utils


(* Truth values for a predicate analyzed by the value analysis *)

type predicate_status = Comp.result = True | False | Unknown

let string_of_predicate_status = function
  | Unknown -> "unknown"
  | True -> "valid"
  | False -> "invalid"

let pretty_predicate_status fmt v =
  Format.fprintf fmt "%s" (string_of_predicate_status v)

let join_predicate_status x y = match x, y with
  | True, True -> True
  | False, False -> False
  | True, False | False, True
  | Unknown, _ | _, Unknown -> Unknown

exception Stop

let _join_list_predicate_status l =
  try
    let r =
      List.fold_left
        (fun acc e ->
           match e, acc with
           | Unknown, _ -> raise Stop
           | e, None -> Some e
           | e, Some eacc -> Some (join_predicate_status eacc e)
        ) None l
    in
    match r with
    | None -> True
    | Some r -> r
  with Stop -> Unknown

(* Type of possible errors during evaluation. See pretty-printer for details *)
type logic_evaluation_error =
  | Unsupported of string
  | UnsupportedLogicVar of logic_var
  | AstError of string
  | NoEnv of logic_label
  | NoResult
  | CAlarm

let pretty_logic_evaluation_error fmt = function
  | Unsupported s -> Format.fprintf fmt "unsupported ACSL construct: %s" s
  | UnsupportedLogicVar tv ->
    Format.fprintf fmt "unsupported logic var %s" tv.lv_name
  | AstError s -> Format.fprintf fmt "error in AST: %s; please report" s
  | NoEnv (FormalLabel s) ->
    Format.fprintf fmt "no environment to evaluate \\at(_,%s)" s
  | NoEnv (BuiltinLabel l) ->
    Format.fprintf fmt "no environment to evaluate \\at(_,%a)"
      Printer.pp_logic_builtin_label l
  | NoEnv (StmtLabel _) ->
    Format.fprintf fmt "\\at() on a C label is unsupported"
  | NoResult -> Format.fprintf fmt "meaning of \\result not specified"
  | CAlarm -> Format.fprintf fmt "alarm during evaluation"

exception LogicEvalError of logic_evaluation_error

let unsupported s = raise (LogicEvalError (Unsupported s))
let unsupported_lvar v = raise (LogicEvalError (UnsupportedLogicVar v))
let ast_error s = raise (LogicEvalError (AstError s))
let no_env lbl = raise (LogicEvalError (NoEnv lbl))
let no_result () = raise (LogicEvalError NoResult)
let c_alarm () = raise (LogicEvalError CAlarm)

(** Three modes to handle the alarms when evaluating a logical term. *)
type alarm_mode =
  | Ignore            (* Ignores all alarms. *)
  | Fail              (* Raises a LogicEvalError when an alarm is encountered. *)
  | Track of bool ref (* Tracks the possibility of an alarm in the boolean. *)

(* Process the possibility of an alarm according to the alarm_mode.
   The boolean [b] is true when an alarm is possible. *)
let track_alarms b = function
  | Ignore -> ()
  | Fail -> if b then c_alarm ()
  | Track bref -> if b then bref := true

let display_evaluation_error ~loc = function
  | CAlarm -> ()
  | pa ->
    Value_parameters.result ~source:(fst loc) ~once:true
      "cannot evaluate ACSL term, %a" pretty_logic_evaluation_error pa

(* Warning mode use when performing _reductions_ in the logic ( ** not **
   evaluation). "Logic alarms" are ignored, and the reduction proceeds as if
   they had not occurred. *)
let alarm_reduce_mode () =
  if Value_parameters.ReduceOnLogicAlarms.get () then Ignore else Fail

let find_or_alarm ~alarm_mode state loc =
  let is_invalid = not (Locations.is_valid ~for_writing:false loc) in
  track_alarms is_invalid alarm_mode;
  let v = Model.find_indeterminate ~conflate_bottom:true state loc in
  let is_indeterminate = Cvalue.V_Or_Uninitialized.is_indeterminate v in
  track_alarms is_indeterminate alarm_mode;
  V_Or_Uninitialized.get_v v

(* Evaluation environments. Used to evaluate predicate on \at nodes *)

(* Labels:
   pre: pre-state of the function. Equivalent to \old in the postcondition
     (and displayed as such)
   here: current location, always the intuitive meaning. Assertions are
     evaluated before the statement.
   post: forbidden in preconditions;
     In postconditions:
      in function contracts, state of in the post-state
      in statement contracts, state after the evaluation of the statement
   old: forbidden in assertions.
        In statement contracts post, means the state before the statement
        In functions contracts post, means the pre-state
*)

(* TODO: evaluating correctly Pat with the current Value domain is tricky,
   and only works reliably for the four labels below, that are either
   invariant during the course of the program, or fully local. The
   program below shows the problem:
   if (c) x = 1; else x = 3;
   L:
   x = 1;
   \assert \at(x == 1, L);
   A naive implementation of assertions involving C labels is likely to miss
   the fact that the assertion is false after the else branch. A good
   solution is to use a dummy edge that flows from L to the assertion,
   to force its re-evaluation.
*)


type labels_states = Cvalue.Model.t Logic_label.Map.t

let join_label_states m1 m2 =
  let aux _ s1 s2 = match s1, s2 with
    | None, None -> None
    | Some s, None | None, Some s -> Some s
    | Some s1, Some s2 -> Some (Cvalue.Model.join s1 s2)
  in
  if m1 == m2 then m1
  else Logic_label.Map.merge aux m1 m2

(* The logic can refer to the state at other points of the program
   using labels. [e_cur] indicates the current label (in changes when
   evaluating the term in a \at(label,term). [e_states] associates a
   memory state to each label. [result] contains the variable
   corresponding to \result; this works even with leaf functions
   without a body. [result] is None when \result is meaningless
   (e.g. the function returns void, logic outside of a function
   contract, etc.) *)
type eval_env = {
  e_cur: logic_label;
  e_states: labels_states;
  result: varinfo option;
}

let join_env e1 e2 = {
  e_cur = (assert (Logic_label.equal e1.e_cur e2.e_cur); e1.e_cur);
  e_states = join_label_states e1.e_states e2.e_states;
  result = (assert (e1.result == e2.result); e1.result);
}

let env_state env lbl =
  try Logic_label.Map.find lbl env.e_states
  with Not_found -> no_env lbl

let env_current_state e = env_state e e.e_cur

let overwrite_state env state lbl =
  { env with e_states = Logic_label.Map.add lbl state env.e_states }

let overwrite_current_state env state = overwrite_state env state env.e_cur

let lbl_here = Logic_const.here_label

let add_logic ll state (states: labels_states): labels_states =
  Logic_label.Map.add ll state states
let add_here = add_logic Logic_const.here_label
let add_pre = add_logic Logic_const.pre_label
let add_post = add_logic Logic_const.post_label
let add_old = add_logic Logic_const.old_label
(* Init is a bit special, it is constant and always added to the initial state*)
let add_init state =
  add_logic Logic_const.init_label (Db.Value.globals_state ()) state

let make_env logic_env state =
  let transfer label map =
    Logic_label.Map.add label (logic_env.Abstract_domain.states label) map
  in
  let map =
    Logic_label.Map.add lbl_here state
      (transfer Logic_const.pre_label
         (transfer Logic_const.old_label
            (transfer Logic_const.post_label
               (add_init Logic_label.Map.empty))))
  in
  { e_cur = lbl_here;
    e_states = map;
    result = logic_env.Abstract_domain.result }

let env_pre_f ~pre () = {
  e_cur = lbl_here;
  e_states = add_here pre (add_pre pre (add_init Logic_label.Map.empty));
  result = None (* Never useful in a pre *);
}

let env_post_f ?(c_labels=Logic_label.Map.empty) ~pre ~post ~result () = {
  e_cur = lbl_here;
  e_states = add_post post
      (add_here post (add_pre pre (add_old pre (add_init c_labels))));
  result = result;
}

let env_annot ?(c_labels=Logic_label.Map.empty) ~pre ~here () = {
  e_cur = lbl_here;
  e_states = add_here here (add_pre pre (add_init c_labels));
  result = None (* Never useful in a 'assert'. TODO: will be needed for stmt
                   contracts *);
}

let env_assigns ~pre = {
  e_cur = lbl_here;
  (* YYY: Post label is missing, but is too difficult in the current evaluation
          scheme, since we build it by evaluating the assigns... *)
  e_states = add_old pre
      (add_here pre (add_pre pre (add_init Logic_label.Map.empty)));
  result = None (* Treated in a special way in callers *)
}

let env_only_here state = {
  e_cur = lbl_here;
  e_states = add_here state (add_init Logic_label.Map.empty);
  result = None (* Never useful in a 'assert'. TODO: will be needed for stmt
                   contracts *);
}

(* Return the base and the type corresponding to the logic var if it is within
   the scope of the supported ones. Fail otherwise. *)
let supported_logic_var lvi =
  match Logic_utils.unroll_type lvi.lv_type with
  | Ctype ty when Cil.isIntegralType ty ->
    (Base.of_c_logic_var lvi), ty
  | _ -> unsupported_lvar lvi

let bind_logic_vars env lvs =
  let bind_one state lv =
    try
      let b, cty = supported_logic_var lv in
      let size = Int.of_int (Cil.bitsSizeOf cty) in
      let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
      Model.add_base_value b ~size v ~size_v:Int.one state
    with Cil.SizeOfError _ -> unsupported_lvar lv
  in
  let state = env_current_state env in
  let state = List.fold_left bind_one state lvs in
  overwrite_current_state env state

let unbind_logic_vars env lvs =
  let unbind_one state lv =
    let b, _ = supported_logic_var lv in
    Model.remove_base b state
  in
  let state = env_current_state env in
  let state = List.fold_left unbind_one state lvs in
  overwrite_current_state env state

let lop_to_cop op =
  match op with
  | Req -> Eq
  | Rneq -> Ne
  | Rle -> Le
  | Rge -> Ge
  | Rlt -> Lt
  | Rgt -> Gt

(* Types currently understood in the evaluation of the logic: no arrays,
   structs, logic arrays or subtle ACSL types. Sets of sets seem to
   be flattened, so the current treatment of them is correct. *)
let rec isLogicNonCompositeType t =
  match t with
  | Lvar _ | Larrow _ -> false
  | Ltype (info, _) ->
    Logic_const.is_boolean_type t ||
    info.lt_name = "sign" ||
    (try isLogicNonCompositeType (Logic_const.type_of_element t)
     with Failure _ -> false)
  | Linteger | Lreal -> true
  | Ctype t -> Cil.isArithmeticOrPointerType t

let rec infer_type = function
  | Ctype t ->
    (match t with
     | TInt _ -> Cil.intType
     | TFloat _ -> Cil.doubleType
     | _ -> t)
  | Lvar _ -> Cil.voidPtrType (* For polymorphic empty sets *)
  | Linteger -> Cil.intType
  | Lreal -> Cil.doubleType
  | Ltype _ | Larrow _ as t ->
    if Logic_const.is_plain_type t then
      unsupported (Pretty_utils.to_string Cil_datatype.Logic_type.pretty t)
    else Logic_const.plain_or_set infer_type t

(* Best effort for comparing the types currently understood by Value: ignore
   differences in integer and floating-point sizes, that are meaningless
   in the logic *)
let same_etype t1 t2 =
  match Cil.unrollType t1, Cil.unrollType t2 with
  | (TInt _ | TEnum _), (TInt _ | TEnum _) -> true
  | TFloat _, TFloat _ -> true
  | TPtr (p1, _), TPtr (p2, _) -> Cil_datatype.Typ.equal p1 p2
  | _, _ -> Cil_datatype.Typ.equal t1 t2

let infer_binop_res_type op targ =
  match op with
  | PlusA | MinusA | Mult | Div -> targ
  | PlusPI | MinusPI | IndexPI ->
    assert (Cil.isPointerType targ); targ
  | MinusPP -> Cil.intType
  | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr ->
    (* can only be applied on integral arguments *)
    assert (Cil.isIntegralType targ); Cil.intType
  | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
    Cil.intType (* those operators always return a boolean *)

(* This function could probably be in Logic_utils. It computes [*tsets],
   assuming that [tsets] has a pointer type. *)
let deref_tsets tsets =
  let star_tsets = Cil.mkTermMem ~addr:tsets ~off:TNoOffset in
  let typ = Logic_typing.type_of_pointed tsets.term_type in
  Logic_const.term (TLval star_tsets) typ


type logic_deps = Zone.t Logic_label.Map.t

let deps_at lbl (ld:logic_deps) =
  try Logic_label.Map.find lbl ld
  with Not_found -> Zone.bottom

let add_deps lbl ldeps deps =
  let prev_deps = deps_at lbl ldeps in
  let deps = Zone.join prev_deps deps in
  let ldeps : logic_deps = Logic_label.Map.add lbl deps ldeps in
  ldeps

let join_logic_deps (ld1:logic_deps) (ld2: logic_deps) : logic_deps =
  let aux _ d1 d2 = match d1, d2 with
    | None as d, None | (Some _ as d), None | None, (Some _ as d) -> d
    | Some d1, Some d2 -> Some (Zone.join d1 d2)
  in
  Logic_label.Map.merge aux ld1 ld2

let empty_logic_deps =
  Logic_label.Map.add lbl_here Zone.bottom Logic_label.Map.empty


(* Type holding the result of an evaluation. Currently, 'a is either
   [Cvalue.V.t] for [eval_term], and [Location_Bits.t] for
   [eval_tlval_as_loc], and [Ival.t] for [eval_toffset].  [eover]
   contains an over-approximation of the evaluation. [eunder] contains an
   under-approximation, under the hypothesis that the state in which we
   evaluate is not Bottom. (Otherwise, all under-approximations would be
   Bottom themselves). The following two invariants should hold:
   (1) eunder \subset eover.
   (2) when evaluating something that is not a Tset, either eunder = Bottom,
      or eunder = eover, and cardinal(eover) <= 1. This is due to the fact
      that under-approximations are not propagated as an abstract domain, but
      only created from Trange or inferred from exact over-approximations. *)
type 'a eval_result = {
  etype: Cil_types.typ;
  eunder: 'a;
  eover: 'a;
  ldeps: logic_deps;
}

(* When computing an under-approximation, we make the hypothesis that the state
   is not Bottom. Hence, over-approximations of cardinal <= 1 are actually of
   cardinal 1, and are thus exact. *)
let under_from_over eover =
  if Cvalue.V.cardinal_zero_or_one eover
  then eover
  else Cvalue.V.bottom
;;

let under_loc_from_over eover =
  if Locations.Location_Bits.cardinal_zero_or_one eover
  then eover
  else Locations.Location_Bits.bottom
;;

let is_noop_cast ~src_typ ~dst_typ =
  let src_typ = Logic_const.plain_or_set
      (fun lt ->
         match Logic_utils.unroll_type lt with
         | Ctype typ -> Eval_typ.classify_as_scalar typ
         | _ -> None
      ) (Logic_utils.unroll_type src_typ)
  in
  let open Eval_typ in
  match src_typ, Eval_typ.classify_as_scalar dst_typ with
  | Some (TSInt rsrc), Some (TSInt rdst) ->
    Eval_typ.range_inclusion rsrc rdst
  | Some (TSFloat srckind), Some (TSFloat destkind) ->
    Cil.frank srckind <= Cil.frank destkind
  | Some (TSPtr _), Some (TSPtr _) -> true
  | _ -> false

(* Note: non-constant integers can happen e.g. for sizeof of structures of an unknown size. *)
let einteger v =
  { etype = Cil.intType;
    eunder = under_from_over v;
    eover = v;
    ldeps = empty_logic_deps }

(* Note: some reals cannot be exactly represented as floats; in which
   case we do not know their under-approximation. *)
let ereal v =
  let eunder = under_from_over v in
  { etype = Cil.doubleType; eunder; eover = v; ldeps = empty_logic_deps }

let is_true = function
  | `True | `TrueReduced _ -> true
  | `Unknown _ | `False | `Unreachable -> false

(* Check "logic alarms" when evaluating [v1 op v2]. All operators shifts are
   defined unambiguously in ACSL. *)
let check_logic_alarms ~alarm_mode typ (_v1: V.t eval_result) op v2 =
  match op with
  | Div | Mod when Cil.isIntegralOrPointerType typ ->
    let truth = Cvalue_forward.assume_non_zero v2.eover in
    let division_by_zero = not (is_true truth) in
    track_alarms division_by_zero alarm_mode
  | Shiftlt | Shiftrt -> begin
      (* Check that [e2] is positive. [e1] can be arbitrary, we use
         the arithmetic vision of shifts *)
      try
        let i2 = Cvalue.V.project_ival_bottom v2.eover in
        let valid = Ival.is_included i2 Ival.positive_integers in
        track_alarms (not valid) alarm_mode
      with Cvalue.V.Not_based_on_null -> track_alarms true alarm_mode
    end
  | _ -> ()

(* Constrain the ACSL range [idx] when it is used to access an array of
   [size_arr] cells, and it is a Trange in which one size is not
   specified. (E.g. t[1..] is transformed into t[1..9] when t has size 10). *)
let constraint_trange idx size_arr =
  if Kernel.SafeArrays.get () then
    match idx.term_node with
    | Trange ((None as low), up) | Trange (low, (None as up)) -> begin
        let loc = idx.term_loc in
        match Extlib.opt_bind Cil.constFoldToInt size_arr with
        | None -> idx
        | Some size ->
          let low = match low with (* constrained l.h.s *)
            | Some _ -> low
            | None -> Some (Logic_const.tint ~loc Integer.zero)
          in
          let up = match up with (* constrained r.h.s *)
            | Some _ -> up
            | None -> Some (Logic_const.tint ~loc (Int.pred size))
          in
          Logic_const.trange ~loc (low, up)
      end
    | _ -> idx
  else idx

(* Note: "charlen" stands for either strlen or wcslen *)

(* Evaluates the logical predicates [strlen/wcslen] using str* builtins.
   Returns [res, alarms], where [res] is the return value of [strlen]
   ([None] the evaluation results in [bottom]). *)
let logic_charlen_builtin wrapper state v =
  (* the call below could in theory return Builtins.Invalid_nb_of_args,
     but logic typing constraints prevent that. *)
  let res, alarms = wrapper state [v] in
  match res with
  | None -> None
  | Some offsm -> Some (offsm, alarms)

(* Never raises exceptions; instead, returns [-1,+oo] in case of alarms
   (most imprecise result possible for the logic strlen/wcslen predicates). *)
let eval_logic_charlen wrapper env v ldeps =
  let eover =
    match logic_charlen_builtin wrapper (env_current_state env) v with
    | None -> Cvalue.V.bottom
    | Some (offsm, alarms) ->
      if alarms
      then Cvalue.V.inject_ival (Ival.inject_range (Some Int.minus_one) None)
      else
        let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
        Cvalue.V_Or_Uninitialized.get_v v
  in
  let eunder = under_from_over eover in
  (* the C strlen function has type size_t, but the logic strlen function has
     type ℤ (signed) *)
  let etype = Cil.intType in
  { etype; ldeps; eover; eunder }

(* Evaluates the logical predicates strchr/wcschr. *)
let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
  let eover =
    match builtin (env_current_state env) [s; c] with
    | None, _ -> Cvalue.V.bottom
    | Some offsm, alarms ->
      if alarms
      then Cvalue.V.zero_or_one
      else
        let v = Extlib.the (Cvalue.V_Offsetmap.single_interval_value offsm) in
        let r = Cvalue.V_Or_Uninitialized.get_v v in
        let ctrue = Cvalue.V.contains_non_zero r
        and cfalse = Cvalue.V.contains_zero r in
        match ctrue, cfalse with
        | true, true -> Cvalue.V.zero_or_one
        | true, false -> Cvalue.V.singleton_one
        | false, true -> Cvalue.V.singleton_zero
        | false, false -> assert false (* a logic alarm would have been raised*)
  in
  let eunder = under_from_over eover in
  (* the C strchr function has type char*, but the logic strchr predicate has
     type 𝔹 *)
  let etype = TInt (IBool, []) in
  let ldeps = join_logic_deps ldeps_s ldeps_c in
  { etype; ldeps; eover; eunder }

(* Evaluates the logical predicate is_allocable, according to the following
   logic:
   - if the size to allocate is always too large (> SIZE_MAX), allocation fails;
   - otherwise, if AllocReturnsNull is true or if the size may exceed SIZE_MAX,
     returns Unknown (to simulate non-determinism);
   - otherwise, allocation always succeeds. *)
let eval_is_allocable size =
  let size_ok = Builtins_malloc.alloc_size_ok size in
  match size_ok, Value_parameters.AllocReturnsNull.get () with
  | Alarmset.False, _ -> False
  | Alarmset.Unknown, _ | _, true -> Unknown
  | Alarmset.True, false -> True

(* returns true iff the logic variable is defined by the
   Frama-C standard library *)
let comes_from_fc_stdlib lvar =
  Cil.hasAttribute "fc_stdlib" lvar.lv_attr ||
  match lvar.lv_origin with
  | None -> false
  | Some vi ->
    Cil.hasAttribute "fc_stdlib" vi.vattr

(* As usual in this file, [dst_typ] may be misleading: the 'size' is
   meaningless, because [src_typ] may actually be a logic type. Thus,
   this size must not be used below. *)
let cast ~src_typ ~dst_typ v =
  let open Eval_typ in
  match classify_as_scalar dst_typ, classify_as_scalar src_typ with
  | None, _ | _, None  -> v (* unclear whether this happens. *)
  | Some dst, Some src ->
    match dst, src with
    | TSFloat fkind, (TSInt _ | TSPtr _) ->
      Cvalue.V.cast_int_to_float (Fval.kind fkind) v

    | (TSInt dst | TSPtr dst), TSFloat fkind ->
      (* This operation is not fully defined in ACSL. We raise an alarm
         in case of overflow. *)
      if is_true (Cvalue_forward.assume_not_nan ~assume_finite:true fkind v)
      then Cvalue_forward.cast_float_to_int dst v
      else c_alarm ()

    | (TSInt dst | TSPtr dst), (TSInt _ | TSPtr _) ->
      let size = Integer.of_int dst.i_bits in
      let signed = dst.i_signed in
      V.cast_int_to_int ~signed ~size v

    | TSFloat fkind, TSFloat _ ->
      Cvalue.V.cast_float_to_float (Fval.kind fkind) v

(* -------------------------------------------------------------------------- *)
(* --- Inlining of defined logic functions and predicates                 --- *)
(* -------------------------------------------------------------------------- *)

type pred_fun_origin = ACSL | Libc

let known_logic_funs = [
  "strlen", Libc;
  "wcslen", Libc;
  "strchr", Libc;
  "wcschr", Libc;
  "atan2", ACSL;
  "atan2f", ACSL;
  "pow", ACSL;
  "powf", ACSL;
  "fmod", ACSL;
  "fmodf", ACSL;
  "\\sign", ACSL;
  "\\min", ACSL;
  "\\max", ACSL;
]
let known_predicates = [
  "\\warning", ACSL;
  "\\is_finite", ACSL;
  "\\is_NaN", ACSL;
  "\\subset", ACSL;
  "valid_read_string", Libc;
  "valid_string", Libc;
  "valid_read_wstring", Libc;
  "valid_wstring", Libc;
  "is_allocable", Libc;
]

let is_known_logic_fun_pred known lvi =
  try
    let origin = List.assoc lvi.lv_name known in
    match origin with
    | ACSL -> true
    | Libc -> comes_from_fc_stdlib lvi
  with Not_found -> false

let is_known_logic_fun = is_known_logic_fun_pred known_logic_funs
let is_known_predicate = is_known_logic_fun_pred known_predicates

let inline logic_info =
  let logic_var = logic_info.l_var_info in
  not (is_known_logic_fun logic_var || is_known_predicate logic_var)

(* We evaluate the ACSL sign type as integers 1 or -1. Sign values can only be
   constructed through the \sign function (handled in eval_known_logic_function)
   and the \Positive and \Negative constructors (handled in eval_term). They can
   only be compared through equality and disequality; no other operation exists
   on this type, so our interpretation remains correct. *)
let positive_cvalue = Cvalue.V.inject_int Int.one
let negative_cvalue = Cvalue.V.inject_int Int.minus_one

(* -------------------------------------------------------------------------- *)
(* --- Evaluation of terms                                                --- *)
(* -------------------------------------------------------------------------- *)

let int_or_float_op typ int_op float_op =
  match typ with
  | TInt _ | TPtr _ | TEnum _ -> int_op
  | TFloat (_fkind, _) -> float_op
  | _ -> ast_error (Format.asprintf
                      "binop on incorrect type %a" Printer.pp_typ typ)

let forward_binop_by_type typ =
  let forward_int = Cvalue_forward.forward_binop_int ~typ
  and forward_float = Cvalue_forward.forward_binop_float Fval.Real in
  int_or_float_op typ forward_int forward_float

let forward_binop typ v1 op v2 =
  match op with
  | Eq | Ne | Le | Lt | Ge | Gt ->
    let comp = Value_util.conv_comp op in
    if Cil.isPointerType typ || Cvalue_forward.are_comparable comp v1 v2
    then forward_binop_by_type typ v1 op v2
    else Cvalue.V.zero_or_one
  | _ -> forward_binop_by_type typ v1 op v2

let rec eval_term ~alarm_mode env t =
  match t.term_node with
  | Tat (t, lab) ->
    ignore (env_state env lab);
    eval_term ~alarm_mode { env with e_cur = lab } t

  | TConst (Integer (v, _)) -> einteger (Cvalue.V.inject_int v)
  | TConst (LEnum e) ->
    (match Cil.constFoldToInt e.eival with
     | Some v -> einteger (Cvalue.V.inject_int v)
     | _ -> ast_error "non-evaluable constant")
  | TConst (LChr c) ->
    einteger (Cvalue.V.inject_int (Cil.charConstToInt c))
  | TConst (LReal { r_lower ; r_upper }) -> begin
      let r_lower = Fval.F.of_float r_lower in
      let r_upper = Fval.F.of_float r_upper in
      let f = Fval.inject Fval.Real r_lower r_upper in
      ereal (V.inject_ival (Ival.inject_float f))
    end

  (*  | TConst ((CStr | CWstr) Missing cases *)

  | TAddrOf (thost, toffs) ->
    let r = eval_thost_toffset ~alarm_mode env thost toffs in
    { etype = TPtr (r.etype, []);
      ldeps = r.ldeps;
      eunder = loc_bits_to_loc_bytes_under r.eunder;
      eover = loc_bits_to_loc_bytes r.eover }

  | TStartOf (thost, toffs) ->
    let r = eval_thost_toffset ~alarm_mode env thost toffs in
    { etype = TPtr (Cil.typeOf_array_elem r.etype, []);
      ldeps = r.ldeps;
      eunder = loc_bits_to_loc_bytes_under r.eunder;
      eover = loc_bits_to_loc_bytes r.eover }

  (* Special case for the constants \pi and \e. *)
  | TLval (TVar {lv_name = "\\pi"}, _) -> ereal (V.inject_float Fval.pi)
  | TLval (TVar {lv_name = "\\e"}, _)  -> ereal (V.inject_float Fval.e)
  | TLval _ ->
    let lval = eval_tlval ~alarm_mode env t in
    let typ = lval.etype in
    let size = Eval_typ.sizeof_lval_typ typ in
    let state = env_current_state env in
    let eover_loc = make_loc (lval.eover) size in
    let eover = find_or_alarm ~alarm_mode state eover_loc in
    let eover = Cvalue_forward.make_volatile ~typ eover in
    let eover = Cvalue_forward.reinterpret typ eover in
    (* Skip dependencies if state is dead *)
    let deps =
      if Cvalue.Model.is_reachable state then
        add_deps env.e_cur empty_logic_deps
          (enumerate_valid_bits ~for_writing:false eover_loc)
      else empty_logic_deps
    in
    let eunder_loc = make_loc (lval.eunder) size in
    let eunder =
      match Eval_op.find_under_approximation state eunder_loc with
      | Some eunder -> V_Or_Uninitialized.get_v eunder
      | None -> under_from_over eover
    in
    { etype = typ;
      ldeps = join_logic_deps deps (lval.ldeps);
      eunder; eover }

  (* TBinOp ((LOr | LAnd), _t1, _t2) -> TODO: a special case would be useful.
     But this requires reducing the state after having evaluated t1 by
     a term that is in fact a predicate *)
  | TBinOp (op,t1,t2) -> eval_binop ~alarm_mode env op t1 t2

  | TUnOp (op, t) ->
    let r = eval_term ~alarm_mode env t in
    let typ' = match op with
      | Neg -> r.etype
      | BNot -> r.etype (* can only be used on an integer type *)
      | LNot -> Cil.intType
    in
    let v = Cvalue_forward.forward_unop r.etype op r.eover in
    let eover = v in
    { etype = typ';
      ldeps = r.ldeps;
      eover; eunder = under_from_over eover }

  | Trange(otlow, othigh) ->
    (* The overapproximation is the range [min(low.eover)..max(high.eover)].
       The underapproximation is the range [max(low.eover)..min(high.eover)].
       Perhaps surprisingly, we do not use the under-approximations of
       otlow and othigh to compute the underapproximation. We could
       potentially compute [min(max(low.over),  min(low.under) ..
                            max(min(high.over), max(high.under)]
       However, tsets cannot be used as bounds of ranges. By invariant (2),
       eunder is either Bottom, or equal to eover, both being of cardinal
       one. In both cases, using eover is more precise. *)
    let deps = ref empty_logic_deps in
    let min v =
      try (match Ival.min_int (Cvalue.V.project_ival v) with
          | None -> `Approx
          | Some(x) -> `Finite(x))
      with Cvalue.V.Not_based_on_null -> `Approx
    in
    let max v =
      try (match Ival.max_int (Cvalue.V.project_ival v) with
          | None -> `Approx
          | Some(x) -> `Finite(x))
      with Cvalue.V.Not_based_on_null -> `Approx
    in
    (* Evaluate a bound:
       - [sure_bound_under] is returned for the under-approximation when the
         bound is explicitly omitted in the ACSL term
       - [min_max_*] is the function to retrieve the bound from the
         over_approximation, for both the underapproximation and the
         overapproximation. *)
    let eval_bound sure_bound_under min_max_under min_max_over = function
      | None -> sure_bound_under, `Approx
      | Some(result) ->
        try
          let result = eval_term ~alarm_mode env result in
          deps := join_logic_deps !deps result.ldeps;
          let under = min_max_under result.eover in
          let over = min_max_over result.eover in
          under, over
        with LogicEvalError e ->
          if e <> CAlarm then
            Value_parameters.result ~source:(fst t.term_loc) ~once:true
              "@[<hov 0>Cannot evaluate@ range bound %a@ (%a). Approximating@]"
              Printer.pp_term result pretty_logic_evaluation_error e;
          `Approx, `Approx
    in
    let min_under, min_over = eval_bound `MinusInf max min otlow in
    let max_under, max_over = eval_bound `PlusInf min max othigh in
    let to_bound = function
      | `Finite x -> Some x
      | `PlusInf | `MinusInf | `Approx -> None
    in
    let eunder = match (min_under, max_under) with
      | `Approx, _ | _, `Approx -> Cvalue.V.bottom
      | (`MinusInf | `Finite _), (`PlusInf | `Finite _) ->
        Cvalue.V.inject_ival
          (Ival.inject_range (to_bound min_under) (to_bound max_under))
    in
    let eover =
      Cvalue.V.inject_ival
        (Ival.inject_range (to_bound min_over) (to_bound max_over))
    in
    { ldeps = !deps;
      etype = Cil.intType;
      eunder; eover }

  | TCastE (typ, t) ->
    let r = eval_term ~alarm_mode env t in
    let eover, eunder =
      (* See if the cast does something. If not, we can keep eunder as is.*)
      if is_noop_cast ~src_typ:t.term_type ~dst_typ:typ
      then r.eover, r.eunder
      else
        let eover = cast ~src_typ:r.etype ~dst_typ:typ r.eover in
        eover, under_from_over eover
    in
    { etype = typ; ldeps = r.ldeps; eunder; eover }

  | Tif (tcond, ttrue, tfalse) ->
    eval_tif eval_term Cvalue.V.join Cvalue.V.meet ~alarm_mode env
      tcond ttrue tfalse

  | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _ | TAlignOfE _ ->
    let e = Cil.constFoldTerm true t in
    let v = match e.term_node with
      | TConst (Integer (v, _)) -> Cvalue.V.inject_int v
      | _ -> V.top_int
    in
    einteger v

  | Tunion l ->
    let eunder, eover, deps = List.fold_left
        (fun (accunder, accover, accdeps) t ->
           let r = eval_term ~alarm_mode env t in
           (Cvalue.V.link accunder r.eunder,
            Cvalue.V.join accover r.eover,
            join_logic_deps accdeps r.ldeps))
        (Cvalue.V.bottom, Cvalue.V.bottom, empty_logic_deps) l
    in
    { etype = infer_type t.term_type;
      ldeps = deps; eunder; eover }

  | Tempty_set ->
    { etype = infer_type t.term_type;
      ldeps = empty_logic_deps;
      eunder = Cvalue.V.bottom;
      eover = Cvalue.V.bottom }

  | Tnull ->
    { etype = Cil.voidPtrType;
      ldeps = empty_logic_deps;
      eunder = Cvalue.V.singleton_zero;
      eover = Cvalue.V.singleton_zero }

  | TLogic_coerce(ltyp, t) ->
    let r = eval_term ~alarm_mode env t in
    (* we must handle coercion from singleton to set, for which there is
       nothing to do, AND coercion from an integer type to a floating-point
       type, that require a conversion. *)
    (match Logic_const.plain_or_set Extlib.id ltyp with
     | Linteger ->
       assert (Logic_typing.is_integral_type t.term_type);
       r
     | Ctype typ when Cil.isIntegralOrPointerType typ -> r
     | Lreal ->
       if Logic_typing.is_integral_type t.term_type
       then (* Needs to be converted to reals *)
         let eover = V.cast_int_to_float Fval.Real r.eover in
         { etype = Cil.longDoubleType; (** hack until logic type *)
           ldeps = r.ldeps;
           eunder = under_from_over eover;
           eover;  }
       else
         let eover = V.cast_float_to_float Fval.Real r.eover in
         { etype = Cil.longDoubleType; (** hack until logic type *)
           ldeps = r.ldeps;
           eunder = under_from_over eover;
           eover;  }
     | _ -> unsupported
              (Format.asprintf "logic coercion %a -> %a@."
                 Printer.pp_logic_type t.term_type Printer.pp_logic_type ltyp)
    )

  (* TODO: the meaning of the label in \offset and \base_addr is not obvious
     at all *)
  | Toffset (_lbl, t) ->
    let r = eval_term ~alarm_mode env t in
    let add_offset _ offs acc = Ival.join offs acc in
    let offs = Location_Bytes.fold_topset_ok add_offset r.eover Ival.bottom in
    let eover = Cvalue.V.inject_ival offs in
    { etype = Cil.intType;
      ldeps = r.ldeps;
      eover;
      eunder = under_from_over eover }

  | Tbase_addr (_lbl, t) ->
    let r = eval_term ~alarm_mode env t in
    let add_base b acc = V.join acc (V.inject b Ival.zero) in
    let eover = Location_Bytes.fold_bases add_base r.eover V.bottom in
    { etype = Cil.charPtrType;
      ldeps = r.ldeps;
      eover;
      eunder = under_from_over eover }

  | Tblock_length (_lbl, t) -> (* TODO: take label into account for locals *)
    let r = eval_term ~alarm_mode env t in
    let add_block_length b acc =
      let bl =
        (* Convert the validity frontiers into a range of bytes. The
           frontiers are always 0 or 8*k-1 (because validity is in bits and
           starts on zero), so we add 1 everywhere, then divide by eight. *)
        let convert start_bits end_bits =
          let congr_succ i = Int.(equal zero (e_rem (succ i) eight)) in
          let congr_or_zero i = Int.(equal zero i || congr_succ i) in
          assert (congr_or_zero start_bits || congr_or_zero end_bits);
          let start_bytes = Int.(e_div (Int.succ start_bits) eight) in
          let end_bytes =   Int.(e_div (Int.succ end_bits)   eight) in
          Ival.inject_range (Some start_bytes) (Some end_bytes)
        in
        match Base.validity b with
        | Base.Empty -> Ival.zero
        | Base.Invalid -> Ival.top (* we may also emit an alarm *)
        | Base.Known (_, ma) -> convert ma ma
        | Base.Unknown (mi, None, ma) -> convert mi ma
        | Base.Unknown (_, Some mi, ma) -> convert mi ma
        | Base.Variable weak_v ->
          convert weak_v.Base.min_alloc weak_v.Base.max_alloc
      in
      Ival.join acc bl
    in
    let bl = Location_Bytes.fold_bases add_block_length r.eover Ival.bottom in
    let eover = V.inject_ival bl in
    { etype = Cil.charPtrType;
      ldeps = r.ldeps;
      eover;
      eunder = under_from_over eover }

  | Tapp (li, labels, args) -> begin
      if is_known_logic_fun li.l_var_info then
        eval_known_logic_function ~alarm_mode env li labels args
      else
        match Inline.inline_term ~inline ~current:env.e_cur t with
        | Some t' -> eval_term ~alarm_mode env t'
        | None ->
          let s =
            Format.asprintf "logic function %a"
              Printer.pp_logic_var li.l_var_info
          in
          unsupported s
    end

  | TDataCons (ctor_info, _) ->
    begin
      match ctor_info.ctor_name with
      | "\\Positive" -> einteger positive_cvalue
      | "\\Negative" -> einteger negative_cvalue
      | "\\true" -> einteger Cvalue.V.singleton_one
      | "\\false" -> einteger Cvalue.V.singleton_zero
      | _ -> unsupported "logic inductive types"
    end

  | Tlambda _ -> unsupported "logic functions or predicates"
  | TUpdate _ -> unsupported "functional updates"
  | TCoerce _ | TCoerceE _ -> unsupported "logic coercions" (* jessie *)
  | Ttype _ -> unsupported "\\type operator"
  | Ttypeof _ -> unsupported "\\typeof operator"
  | Tcomprehension _ -> unsupported "sets defined by comprehension"
  | Tinter _ -> unsupported "set intersection"
  | Tlet _ -> unsupported "\\let bindings"
  | TConst (LStr _) -> unsupported "constant strings"
  | TConst (LWStr _) -> unsupported "wide constant strings"