eval_terms.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    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 Locations
open Cvalue

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

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

let join_predicate_status x y = match x, y with
  | True, True -> True
  | False, False -> False
  | True, False | False, True
  | Unknown, _ | _, Unknown -> 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 ->
    Self.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 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

(* Returns true if [loc] contains a memory location definitely invalid
   for a memory access of kind [access]. *)
let contains_invalid_loc access loc =
  let valid_loc = Locations.valid_part access loc in
  not (Locations.Location.equal loc valid_loc)

(* -------------------------------------------------------------------------- *)
(* --- Evaluation environments.                                           --- *)
(* -------------------------------------------------------------------------- *)

(* Evaluation environments are used to evaluate predicate on \at nodes,
   the varinfo \result and logic variables introduced by quantifiers. *)

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

module Logic_label = Cil_datatype.Logic_label
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 states =
  match Cvalue_results.get_global_state () with
  | `Bottom -> states
  | `Value state -> add_logic Logic_const.init_label state states

let add_logic_var env lv cvalue =
  { env with logic_vars = LogicVarEnv.add lv cvalue env.logic_vars }

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 *);
}

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
    | Ctype ctyp when Cil.isIntegralType ctyp ->
      let base = Base.of_c_logic_var lv in
      let size = Integer.of_int (Cil.bitsSizeOf ctyp) in
      let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
      let state = Model.add_base_value base ~size v ~size_v:Integer.one state in
      state, logic_vars
    | _ -> 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 copy_logic_vars ~src ~dst lvars =
  let copy_one env lvar =
    match Logic_utils.unroll_type lvar.lv_type with
    | Linteger | Lreal ->
      let value = LogicVarEnv.find lvar src.logic_vars in
      let logic_vars = LogicVarEnv.add lvar value env.logic_vars in
      { env with logic_vars }
    | Ctype _ ->
      begin
        let base = Base.of_c_logic_var lvar in
        match Model.find_base base (env_current_state src) with
        | `Bottom | `Top -> env
        | `Value offsm ->
          let state = Model.add_base base offsm (env_current_state env) in
          overwrite_current_state env state
      end
    | _ -> unsupported_lvar lvar
  in
  List.fold_left copy_one dst lvars

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
    | Ctype _ ->
      let base = Base.of_c_logic_var lv in
      Model.remove_base base state, logic_vars
    | _ -> unsupported_lvar lv
  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

(* -------------------------------------------------------------------------- *)
(* --- Evaluation results.                                                --- *)
(* -------------------------------------------------------------------------- *)

(* Result of the evaluation of a term as an exact location (to reduce its value
   in the current state). *)
type exact_location =
  | Location of typ * Locations.location
  (* A location represented in the cvalue state. *)
  | Logic_var of logic_var
  (* A logic variable, introduced by a quantifier, and stored in an environment
     besides the states. *)

(* Raised when a term cannot be evaluated as an exact location.*)
exception Not_an_exact_loc

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;
}

let join_eval_result r1 r2 =
  let eover = Cvalue.V.join r2.eover r1.eover in
  let eunder = Cvalue.V.meet r1.eunder r2.eunder in
  let ldeps = join_logic_deps r1.ldeps r2.ldeps in
  { eover; eunder; ldeps; etype = r1.etype; empty = r1.empty || r2.empty; }

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

(* 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_const.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_const.doubleType (Cvalue.V.inject_float fval)
let efloat fval = inject_no_deps Cil_const.floatType (Cvalue.V.inject_float fval)

(* -------------------------------------------------------------------------- *)
(* --- Utilitary functions on the Cil AST                                 --- *)
(* -------------------------------------------------------------------------- *)

let is_rel_binop = function
  | Lt
  | Gt
  | Le
  | Ge
  | Eq
  | Ne -> true
  | _ -> false

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

let rel_of_binop = function
  | Lt -> Rlt
  | Gt -> Rgt
  | Le -> Rle
  | Ge -> Rge
  | Eq -> Req
  | Ne -> Rneq
  | _ -> assert false

(* 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, _) ->
    info.lt_name = "sign" ||
    (try isLogicNonCompositeType (Logic_const.type_of_element t)
     with Failure _ -> false)
  | Lboolean | Linteger | Lreal -> true
  | Ctype t -> Cil.isScalarType t

let rec infer_type = function
  | Ctype t ->
    (match t.tnode with
     | TInt _ -> Cil_const.intType
     | TFloat _ -> Cil_const.doubleType
     | _ -> t)
  | Lvar _ -> Cil_const.voidPtrType (* For polymorphic empty sets *)
  | Lboolean -> Cil_const.boolType
  | Linteger -> Cil_const.intType
  | Lreal -> Cil_const.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.unrollTypeNode t1, Cil.unrollTypeNode 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

(* Returns the kind of floating-point represented by a logic type, or None. *)
let logic_type_fkind = function
  | Ctype typ -> begin
      match Cil.unrollTypeNode typ with
      | TFloat fkind -> Some fkind
      | _ -> None
    end
  | _ -> None

let infer_binop_res_type op targ =
  match op with
  | PlusA | MinusA | Mult | Div -> targ
  | PlusPI | MinusPI ->
    assert (Cil.isPointerType targ); targ
  | MinusPP -> Cil_const.intType
  | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr ->
    (* can only be applied on integral arguments *)
    assert (Cil.isIntegralType targ); Cil_const.intType
  | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr ->
    Cil_const.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

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

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

(* If casting [trm] to [typ] has no effect in terms of the values contained
   in [trm], do nothing. Otherwise, raise [exn]. Adapted from [pass_cast] *)
let pass_logic_cast exn typ trm =
  match Logic_utils.unroll_type typ, Logic_utils.unroll_type trm.term_type with
  | Linteger, Ctype { tnode = (TInt _ | TEnum _) } -> () (* Always inclusion *)
  | Ctype ({ tnode = (TInt _ | TEnum _) } as typ),
    Ctype ({ tnode = (TInt _ | TEnum _) } as typeoftrm) ->
    let sztyp = Bit_utils.sizeof typ in
    let szexpr = Bit_utils.sizeof typeoftrm in
    let styp, sexpr =
      match sztyp, szexpr with
      | Int_Base.Value styp, Int_Base.Value sexpr -> styp, sexpr
      | _ -> raise exn
    in
    let sityp = Bit_utils.is_signed_int_enum_pointer typ in
    let sisexpr = Bit_utils.is_signed_int_enum_pointer typeoftrm in
    if (Integer.ge styp sexpr && sityp = sisexpr) (* larger, same signedness *)
    || (Integer.gt styp sexpr && sityp) (* strictly larger and signed *)
    then ()
    else raise exn

  | Lreal,  Ctype { tnode = (TFloat _) } -> () (* Always inclusion *)
  | Ctype { tnode = (TFloat f1) }, Ctype { tnode = (TFloat f2) } ->
    if Cil.frank f1 < Cil.frank f2
    then raise exn

  | _ -> raise exn (* Not a scalar type *)

let is_same_term_coerce t1 t2 =
  match t1.term_node, t2.term_node with
  | TCast (true,_,_), TCast (true,_,_) -> Logic_utils.is_same_term t1 t2
  | TCast (true, _,t1), _ -> Logic_utils.is_same_term t1 t2
  | _, TCast (true, _,t2) -> Logic_utils.is_same_term t1 t2
  | _ -> Logic_utils.is_same_term t1 t2

(* 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 Option.bind size_arr Cil.constFoldToInt 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 (Integer.pred size))
          in
          Logic_const.trange ~loc (low, up)
      end
    | _ -> idx
  else idx

(* -------------------------------------------------------------------------- *)
(* --- 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;
  "memchr_off", Libc;
  "wmemchr_off", Libc;
  "atan2", ACSL;
  "atan2f", ACSL;
  "pow", ACSL;
  "powf", ACSL;
  "fmod", ACSL;
  "fmodf", ACSL;
  "sqrt", ACSL;
  "sqrtf", ACSL;
  "\\sign", ACSL;
  "\\min", ACSL;
  "\\max", ACSL;
  "\\abs", ACSL;
  "\\neg_float",ACSL;
  "\\add_float",ACSL;
  "\\sub_float",ACSL;
  "\\mul_float",ACSL;
  "\\div_float",ACSL;
  "\\neg_double",ACSL;
  "\\add_double",ACSL;
  "\\sub_double",ACSL;
  "\\mul_double",ACSL;
  "\\div_double",ACSL;
]
let known_predicates = [
  "\\warning", ACSL;
  "\\is_finite", ACSL;
  "\\is_infinite", 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;
  "\\tainted", 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)

(* -------------------------------------------------------------------------- *)
(* --- Auxiliary evaluation functions                                     --- *)
(* -------------------------------------------------------------------------- *)

(* 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 Integer.one
let negative_cvalue = Cvalue.V.inject_int Integer.minus_one

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
  | _ -> ()

(* 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 = Cil_const.boolType }

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

(* Applies a cvalue [builtin] to the list of arguments [args_list] in the
   current state of [env]. Returns [v, alarms], where [v] is the resulting
   cvalue, which can be bottom. *)
let apply_logic_builtin builtin env args_list =
  (* the call below could in theory return Builtins.Invalid_nb_of_args,
     but logic typing constraints prevent that. *)
  builtin (env_current_state env) args_list

(* 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 =
    let v, alarms = apply_logic_builtin wrapper env [v] in
    if alarms && not (Cvalue.V.is_bottom v)
    then Cvalue.V.inject_ival (Ival.inject_range (Some Integer.minus_one) None)
    else 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_const.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 =
    let v, alarms = apply_logic_builtin builtin env [s; c] in
    if Cvalue.V.is_bottom v then v else
    if alarms then Cvalue.V.zero_or_one else
      let ctrue = Cvalue.V.contains_non_zero v
      and cfalse = Cvalue.V.contains_zero v 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 = Cil_const.boolType in
  let ldeps = join_logic_deps ldeps_s ldeps_c in
  { etype; ldeps; eover; empty = false; eunder }

(* Evaluates the logical functions memchr_off/wmemchr_off. *)
let eval_logic_memchr_off builtin env s c n =
  let minus_one = Cvalue.V.inject_int Integer.minus_one in
  let positive = Cvalue.V.inject_ival Ival.positive_integers in
  let pred_n = Cvalue.V.add_untyped ~factor:Int_Base.one n.eover minus_one in
  let n_pos = Cvalue.V.narrow positive pred_n in
  let eover =
    if Cvalue.V.is_bottom n_pos then minus_one else
      let args = [s.eover; c.eover; n_pos] in
      let v, alarms = apply_logic_builtin builtin env args in
      if Cvalue.V.is_bottom v then pred_n else
      if alarms then Cvalue.V.join pred_n v else
      if Cvalue.V.equal n_pos pred_n then v else
        Cvalue.V.join minus_one v
  in
  let ldeps = join_logic_deps s.ldeps (join_logic_deps c.ldeps n.ldeps) in
  { (einteger eover) with ldeps }

(* 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, Parameters.AllocReturnsNull.get () with
  | Alarmset.False, _ -> False
  | Alarmset.Unknown, _ | _, true -> Unknown
  | Alarmset.True, false -> True

(* Evaluates a [valid_read_string] or [valid_read_wstring] predicate
   using str* builtins.
   - if [bottom] is obtained, return False;
   - otherwise, if no alarms are emitted, return True;
   - otherwise, return [Unknown]. *)
let eval_valid_read_str ~wide env v =
  let wrapper =
    if wide then Builtins_string.frama_c_wcslen_wrapper
    else Builtins_string.frama_c_strlen_wrapper
  in
  let v, alarms = apply_logic_builtin wrapper env [v] in
  if Cvalue.V.is_bottom v
  then False (* bottom state => string always invalid *)
  else if alarms
  then Unknown (* alarm => string possibly invalid *)
  else True (* no alarm => string always valid for reading *)

(* Evaluates a [valid_string] or [valid_wstring] predicate.
   First, we check the constness of the arguments.
   Then, we evaluate [valid_read_string/valid_read_wstring] on non-const ones. *)
let eval_valid_str ~wide env v =
  assert (not (Cvalue.V.is_bottom v));
  (* filter const bases *)
  let v' = Cvalue.V.filter_base (fun b -> not (Base.is_read_only b)) v in
  if Cvalue.V.is_bottom v' then False (* all bases were const *)
  else
  if Cvalue.V.equal v v' then
    eval_valid_read_str ~wide env v (* all bases non-const *)
  else (* at least one base was const *)
    match eval_valid_read_str ~wide env v with
    | True -> Unknown (* weaken result *)
    | False | Unknown as r -> r

(* Do all the possible values of a location in [state] satisfy [test]?  [loc] is
   an over-approximation of the location, so the answer cannot be [False] even
   if some parts of [loc] do not satisfy [test]. Thus, this function does not
   fold the location, but instead applies [test] to the join of all values
   stored in [loc] in [state].  *)
let forall_in_over_location state loc test =
  let v = Model.find_indeterminate state loc in
  test v

(* Do all the possible values of a location in [state] satisfy [test]?  [loc] is
   an under-approximation of the location, so the answer cannot be [True], as
   the values of some other parts of the location may not satisfy [test].
   However, it is [False] as soon as some part of [loc] contradicts [test]. *)
let forall_in_under_location state loc test =
  let exception EFalse in
  let inspect_value (_, _) (value, _, _) acc =
    match test value with
    | True | Unknown -> acc
    | False -> raise EFalse
  in
  let inspect_itv base itv acc =
    match Cvalue.Model.find_base_or_default base state with
    | `Top | `Bottom -> Unknown
    | `Value offsm ->
      Cvalue.V_Offsetmap.fold_between ~entire:true itv inspect_value offsm acc
  in
  let inspect_base base intervals acc =
    Int_Intervals.fold (inspect_itv base) intervals acc
  in
  let zone = Locations.enumerate_bits loc in
  try Zone.fold_i inspect_base zone Unknown
  with EFalse -> False
     | Abstract_interp.Error_Top -> Unknown

(* Evaluates an universal predicate about the values of a location evaluated to
   [r] in [state]. The predicates holds whenever all the possible values at the
   location satisfy [test]. *)
let eval_forall_predicate state r test =
  let size_bits = Eval_typ.sizeof_lval_typ r.etype in
  let make_loc loc = make_loc loc size_bits in
  let over_loc = make_loc r.eover in
  if not Locations.(is_valid Read over_loc) then c_alarm ();
  match forall_in_over_location state over_loc test with
  | Unknown ->
    let under_loc = make_loc r.eunder in
    forall_in_under_location state under_loc test
  | True -> True
  | False -> if r.empty then Unknown else False

(* Evaluation of an \initialized predicate on a location evaluated to [r]
   in the state [state]. *)
let eval_initialized state r =
  let test = function
    | V_Or_Uninitialized.C_init_esc _
    | V_Or_Uninitialized.C_init_noesc _ -> True
    | V_Or_Uninitialized.C_uninit_esc _ -> Unknown
    | V_Or_Uninitialized.C_uninit_noesc v ->
      if Location_Bytes.is_bottom v then False else Unknown
  in
  eval_forall_predicate state r test

(* Evaluation of a \dangling predicate on a location evaluated to [r]
   in the state [state]. *)
let eval_dangling state r =
  let test = function
    | V_Or_Uninitialized.C_init_esc v ->
      if Location_Bytes.is_bottom v then True else Unknown
    | V_Or_Uninitialized.C_uninit_esc _ -> Unknown
    | V_Or_Uninitialized.C_init_noesc _
    | V_Or_Uninitialized.C_uninit_noesc _ -> False
  in
  eval_forall_predicate state r test

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

exception Reduce_to_bottom

let int_or_float_op typ int_op float_op =
  match typ.tnode with
  | TInt _ | TPtr _ | TEnum _ -> int_op
  | TFloat _fk -> 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
  | Eva_ast.Eq | Ne | Le | Lt | Ge | Gt ->
    let comp = Eva_ast.conv_relation 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 (Boolean true) -> einteger Cvalue.V.singleton_one
  | TConst (Boolean false) -> einteger Cvalue.V.singleton_zero
  | 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