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_indeterminate ~alarm_mode state loc =
  let is_invalid = not Locations.(is_valid Read loc) in
  track_alarms is_invalid alarm_mode;
  Model.find_indeterminate ~conflate_bottom:true state loc

let find_or_alarm ~alarm_mode state loc =
  let v = find_indeterminate ~alarm_mode 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

let contains_invalid_loc access loc =
  let valid_loc = Locations.valid_part access loc in
  not (Locations.Location.equal loc valid_loc)

(* 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 = Some (Cvalue.Model.join s1 s2) in
  if m1 == m2 then m1
  else Logic_label.Map.union aux m1 m2

(* Environment for mathematical variables introduced by quantifiers:
   maps from their int identifiers to cvalues representing an over-approximation
   of their values (either mathematical integers or mathematical reals). *)
module LogicVarEnv = struct
  include Cil_datatype.Logic_var.Map

  let find logic_var map =
    try find logic_var map
    with Not_found -> unsupported_lvar logic_var

  let join m1 m2 =
    let aux _ v1 v2 = Some (Cvalue.V.join v1 v2) in
    if m1 == m2 then m1
    else union aux m1 m2
end

type logic_env = Cvalue.V.t LogicVarEnv.t

(* 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. [logic_vars] binds mathematical variables
   to their possible values. [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;
  logic_vars: logic_env;
  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;
  logic_vars = LogicVarEnv.join e1.logic_vars e2.logic_vars;
  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;
    logic_vars = LogicVarEnv.empty;
    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));
  logic_vars = LogicVarEnv.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))));
  logic_vars = LogicVarEnv.empty;
  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));
  logic_vars = LogicVarEnv.empty;
  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)));
  logic_vars = LogicVarEnv.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);
  logic_vars = LogicVarEnv.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 c_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 top_float =
  let neg_infinity = Fval.F.of_float neg_infinity
  and pos_infinity = Fval.F.of_float infinity in
  let fval = Fval.inject ~nan:false Fval.Real neg_infinity pos_infinity in
  Ival.inject_float fval

let bind_logic_vars env lvs =
  let bind_one (state, logic_vars) lv =
    let bind_logic_var ival =
      state, LogicVarEnv.add lv (Cvalue.V.inject_ival ival) logic_vars
    in
    match Logic_utils.unroll_type lv.lv_type with
    | Linteger -> bind_logic_var Ival.top
    | Lreal -> bind_logic_var top_float
    | _ ->
      try
        let b, cty = c_logic_var lv in
        let size = Int.of_int (Cil.bitsSizeOf cty) in
        let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
        let state = Model.add_base_value b ~size v ~size_v:Int.one state in
        state, logic_vars
      with Cil.SizeOfError _ -> unsupported_lvar lv
  in
  let state = env_current_state env in
  let state, logic_vars = List.fold_left bind_one (state, env.logic_vars) lvs in
  overwrite_current_state { env with logic_vars } state

let unbind_logic_vars env lvs =
  let unbind_one (state, logic_vars) lv =
    match Logic_utils.unroll_type lv.lv_type with
    | Linteger | Lreal -> state, LogicVarEnv.remove lv logic_vars
    | _ ->
      let b, _ = c_logic_var lv in
      Model.remove_base b state, logic_vars
  in
  let state = env_current_state env in
  let state, logic_vars = List.fold_left unbind_one (state, env.logic_vars) lvs in
  overwrite_current_state { env with logic_vars } 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 *)

(* Computes [*tsets], assuming that [tsets] has a pointer type. *)
let deref_tsets tsets = Cil.mkTermMem ~addr:tsets ~off:TNoOffset


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] is an over-approximation of the evaluation. [eunder] is 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.

   This type can be used for the evaluation of logical sets, in which case
   an eval_result [r] represents all *non-empty* sets [S] such that:
   [r.eunder ⊆ S ⊆ r.eover]. The value {V.bottom} does *not* represents empty
   sets, as for most predicates, P(∅) ≠ P(⊥) (if the latter has a meaning).
   The boolean [empty] indicates whether an eval_result also represents a
   possible empty set. *)
type 'a eval_result = {
  etype: Cil_types.typ;
  eunder: 'a;
  eover: 'a;
  empty: bool;
  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

(* Injects [cvalue] as an eval_result of type [typ] with no dependencies. *)
let inject_no_deps typ cvalue =
  { etype = typ;
    eunder = under_from_over cvalue;
    eover = cvalue;
    empty = false;
    ldeps = empty_logic_deps }

(* Integer result with no memory dependencies: constants, sizeof & alignof,
   and values of logic variables.*)
let einteger = inject_no_deps Cil.intType

(* Note: some reals cannot be exactly represented as floats; in which
   case we do not know their under-approximation. *)
let ereal fval = inject_no_deps Cil.doubleType (Cvalue.V.inject_float fval)
let efloat fval = inject_no_deps Cil.floatType (Cvalue.V.inject_float fval)

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; empty = false; 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; empty = false; 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

(* V.cast_int_to_int is unsound when the destination type is _Bool.
   Use this function instead. *)
let cast_to_bool r =
  let contains_zero = V.contains_zero r.eover
  and contains_non_zero = V.contains_non_zero r.eover in
  let eover = V.interp_boolean ~contains_zero ~contains_non_zero in
  { eover; eunder = under_from_over eover; empty = r.empty;
    ldeps = r.ldeps; etype = TInt (IBool, []) }

(* -------------------------------------------------------------------------- *)
(* --- 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_plus_infinity", ACSL;
  "\\is_minus_infinity", ACSL;
  "\\is_NaN", ACSL;
  "\\eq_float", ACSL;
  "\\ne_float", ACSL;
  "\\lt_float", ACSL;
  "\\le_float", ACSL;
  "\\gt_float", ACSL;
  "\\ge_float", ACSL;
  "\\eq_double", ACSL;
  "\\ne_double", ACSL;
  "\\lt_double", ACSL;
  "\\le_double", ACSL;
  "\\gt_double", ACSL;
  "\\ge_double", 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_nearest; r_lower ; r_upper }) -> begin
      if Fc_float.is_nan r_nearest
      then ereal Fval.nan
      else
        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 f
    end

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

  | TAddrOf tlval ->
    let r = eval_tlval ~alarm_mode env tlval 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;
      empty = r.empty; }

  | TStartOf tlval ->
    let r = eval_tlval ~alarm_mode env tlval 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;
      empty = r.empty; }

  (* Special case for the constants \pi, \e, \infinity and \NaN. *)
  | TLval (TVar {lv_name = "\\pi"}, _) -> ereal Fval.pi
  | TLval (TVar {lv_name = "\\e"}, _)  -> ereal Fval.e
  | TLval (TVar {lv_name = "\\plus_infinity"}, _) ->
    efloat Fval.(pos_infinity Single)
  | TLval (TVar {lv_name = "\\minus_infinity"}, _) ->
    efloat Fval.(neg_infinity Single)
  | TLval (TVar {lv_name = "\\NaN"}, _) -> efloat Fval.nan

  (* Mathematical logic variable: uses the [logic_vars] environment. *)
  | TLval (TVar ({ lv_type = Linteger | Lreal } as logic_var), TNoOffset) ->
    let cvalue = LogicVarEnv.find logic_var env.logic_vars in
    if logic_var.lv_type = Linteger
    then einteger cvalue
    else inject_no_deps Cil.doubleType cvalue

  | TLval tlval ->
    let lval = eval_tlval ~alarm_mode env tlval 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 Locations.Read 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; empty = lval.empty; }

  (* 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; empty = r.empty; }

  | Trange (opt_low, opt_high) ->
    (* 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
    (* Evaluates the minimum and maximum integer value of an optional term.
       According to the Ival convention, None stands for -∞ and ∞ for the
       minimum and maximum respectively. *)
    let min_max = function
      | None -> None, None
      | Some term ->
        try
          let result = eval_term ~alarm_mode env term in
          deps := join_logic_deps !deps result.ldeps;
          let ival = Cvalue.V.project_ival result.eover in
          Ival.min_int ival, Ival.max_int ival
        with
        | Cvalue.V.Not_based_on_null -> None, None
        | 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 term pretty_logic_evaluation_error e;
          None, None
    in
    let min_over, min_under = min_max opt_low
    and max_under, max_over = min_max opt_high in
    let eover = Cvalue.V.inject_ival (Ival.inject_range min_over max_over) in
    (* Beware: [None] stands for positive infinity for [min_under] and for
       negative infiny for [max_under] (in which case eunder must be bottom),
       except when the bound was itself [None]. *)
    let eunder =
      if (opt_low <> None && min_under = None)
      || (opt_high <> None && max_under = None)
      then Cvalue.V.bottom
      else Cvalue.V.inject_ival (Ival.inject_range min_under max_under)
    in
    let empty = Cvalue.V.is_bottom eunder in
    { ldeps = !deps;
      etype = Cil.intType;
      eunder; eover; empty; }

  | TCastE (typ, t) ->
    let r = eval_term ~alarm_mode env t in
    (* 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 with etype = typ }
    else if Cil.isBoolType typ
    then cast_to_bool r
    else
      let eover = cast ~src_typ:r.etype ~dst_typ:typ r.eover in
      { etype = typ; ldeps = r.ldeps; eunder = under_from_over eover; eover;
        empty = r.empty; }

  | 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, empty = List.fold_left
        (fun (accunder, accover, accdeps, accempty) 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,
            accempty || r.empty))
        (Cvalue.V.bottom, Cvalue.V.bottom, empty_logic_deps, false) l
    in
    { etype = infer_type t.term_type;
      ldeps = deps; eunder; eover; empty; }

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

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

  | 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 when Logic_typing.is_integral_type t.term_type
                  || Logic_const.is_boolean_type t.term_type -> r
     | Ctype typ when Cil.isIntegralOrPointerType typ -> r
     | Lreal ->
       let eover =
         if Logic_typing.is_integral_type t.term_type
         then V.cast_int_to_float Fval.Real r.eover
         else V.cast_float_to_float Fval.Real r.eover
       in
       { etype = Cil.longDoubleType; (** hack until logic type *)
         ldeps = r.ldeps;
         eover; eunder = under_from_over eover;
         empty = r.empty }
     | _ ->
       if Logic_const.is_boolean_type ltyp
       && Logic_typing.is_integral_type t.term_type
       then cast_to_bool r
       else
         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