Cint.ml

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

(* -------------------------------------------------------------------------- *)
(* --- Integer Arithmetics Model                                          --- *)
(* -------------------------------------------------------------------------- *)

open Qed
open Qed.Logic
open Lang
open Lang.F
module FunMap = Map.Make(Lang.Fun)

(* -------------------------------------------------------------------------- *)
(* --- Kernel Interface                                                   --- *)
(* -------------------------------------------------------------------------- *)

let is_overflow_an_error iota =
  if Ctypes.signed iota
  then Kernel.SignedOverflow.get ()
  else Kernel.UnsignedOverflow.get ()

let is_downcast_an_error iota =
  if Ctypes.signed iota
  then Kernel.SignedDowncast.get ()
  else Kernel.UnsignedDowncast.get ()

(* -------------------------------------------------------------------------- *)
(* --- Library Cint                                                       --- *)
(* -------------------------------------------------------------------------- *)

let is_cint_map = ref FunMap.empty
let to_cint_map = ref FunMap.empty

let is_cint f = FunMap.find f !is_cint_map
let to_cint f = FunMap.find f !to_cint_map

let library = "cint"

let make_fun_int op i =
  Lang.extern_f ~library ~result:Logic.Int "%s_%a" op Ctypes.pp_int i
let make_pred_int op i =
  Lang.extern_f
    ~library ~result:Logic.Prop ~coloring:true "%s_%a" op Ctypes.pp_int i

(* let fun_int op = Ctypes.imemo (make_fun_int op) *) (* unused for now *)
(* let pred_int op = Ctypes.imemo (make_pred_int op) *) (* unused for now *)

(* Signature int,int -> int over Z *)
let ac = {
  associative = true ;
  commutative = true ;
  idempotent = false ;
  invertible = false ;
  neutral = E_none ;
  absorbant = E_none ;
}

(* Functions -> Z *)
let result = Logic.Int

(* -------------------------------------------------------------------------- *)
(* --- Library Cbits                                                      --- *)
(* -------------------------------------------------------------------------- *)

let library = "cbits"
let balance = Lang.Left

let op_lxor = { ac with neutral = E_int 0 ; invertible = true }
let op_lor  = { ac with neutral = E_int 0 ; absorbant = E_int (-1); idempotent = true }
let op_land = { ac with neutral = E_int (-1); absorbant = E_int 0 ; idempotent = true }

let f_lnot = Lang.extern_f ~library ~result "lnot"
let f_lor  = Lang.extern_f ~library ~result ~category:(Operator op_lor) ~balance "lor"
let f_land = Lang.extern_f ~library ~result ~category:(Operator op_land) ~balance "land"
let f_lxor = Lang.extern_f ~library ~result ~category:(Operator op_lxor) ~balance "lxor"
let f_lsl = Lang.extern_f ~library ~result "lsl"
let f_lsr = Lang.extern_f ~library ~result "lsr"

let f_bitwised = [ f_lnot ; f_lor ; f_land ; f_lxor ; f_lsl ; f_lsr ]

(* [f_bit_stdlib] is related to the function [bit_test] of Frama-C StdLib *)
let f_bit_stdlib   = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
(* [f_bit_positive] is actually exported in forgoting the fact the position is positive *)
let f_bit_positive = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
(* At export, some constructs such as [e & (1 << k)] are written into [f_bit_export] construct *)
let f_bit_export   = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()

let () = let open LogicBuiltins in add_builtin "\\bit_test_stdlib" [Z;Z] f_bit_stdlib
let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit_positive

let f_bits = [ f_bit_stdlib ; f_bit_positive ; f_bit_export ]

let bit_test e k =
  let r = F.e_fun ~result:Logic.Bool
      (if k <= 0 then f_bit_positive else f_bit_stdlib) [e ; e_int k]
  in assert (is_prop r) ; r

(* -------------------------------------------------------------------------- *)
(* --- Matching utilities for simplifications                             --- *)
(* -------------------------------------------------------------------------- *)

let is_leq a b = F.is_true (F.e_leq a b)

let match_integer t =
  match F.repr t with
  | Logic.Kint c -> c
  | _ -> raise Not_found

let match_to_cint t =
  match F.repr t with
  | Logic.Fun( conv , [a] ) -> (to_cint conv), a
  | _ -> raise Not_found

let match_mod t =
  match F.repr t with
  | Logic.Mod (e1, e2) -> e1, e2
  | _ -> raise Not_found

(* integration with qed should be improved! *)
let is_positive t =
  match F.repr t with
  | Logic.Kint c -> Integer.le Integer.one c
  | _ -> false

(* integration with qed should be improved! *)
let rec is_positive_or_null e = match F.repr e with
  | Logic.Fun( f , [e] ) when Fun.equal f f_lnot -> is_negative e
  | Logic.Fun( f , es ) when Fun.equal f f_land  -> List.exists is_positive_or_null es
  | Logic.Fun( f , es ) when Fun.equal f f_lor   -> List.for_all is_positive_or_null es
  | Logic.Fun( f , es ) when Fun.equal f f_lxor  -> (match mul_xor_sign es with | Some b -> b | _ -> false)
  | Logic.Fun( f , es ) when Fun.equal f f_lsr || Fun.equal f f_lsl
    -> List.for_all is_positive_or_null es
  | _ -> (* try some improvement first then ask to qed *)
      let improved_is_positive_or_null e = match F.repr e with
        | Logic.Add es -> List.for_all is_positive_or_null es
        | Logic.Mul es -> (match mul_xor_sign es with | Some b -> b | _ -> false)
        | Logic.Mod(e1,e2) when is_positive e2 || is_negative e2 ->
            (* e2<>0 ==> ( 0<=(e1 % e2) <=> 0<=e1 ) *)
            is_positive_or_null e1
        | _ -> false
      in if improved_is_positive_or_null e then true
      else match F.is_true (F.e_leq e_zero e) with
        | Logic.Yes -> true
        | Logic.No | Logic.Maybe -> false
and is_negative e = match F.repr e with
  | Logic.Fun( f , [e] ) when Fun.equal f f_lnot -> is_positive_or_null e
  | Logic.Fun( f , es ) when Fun.equal f f_lor   -> List.exists is_negative es
  | Logic.Fun( f , es ) when Fun.equal f f_land  -> List.for_all is_negative es
  | Logic.Fun( f , es ) when Fun.equal f f_lxor  -> (match mul_xor_sign es with | Some b -> (not b) | _ -> false)
  | Logic.Fun( f , [k;n] ) when Fun.equal f f_lsr || Fun.equal f f_lsl
    -> is_positive_or_null n && is_negative k
  | _ -> (* try some improvement first then ask to qed *)
      let improved_is_negative e = match F.repr e with
        | Logic.Add es -> List.for_all is_negative es
        | Logic.Mul es -> (match mul_xor_sign es with | Some b -> (not b) | _ -> false)
        | _ -> false
      in if improved_is_negative e then true
      else match F.is_true (F.e_lt e e_zero) with
        | Logic.Yes -> true
        | Logic.No | Logic.Maybe -> false
and mul_xor_sign es = try
    Some (List.fold_left (fun acc e ->
        if is_positive_or_null e then acc (* as previous *)
        else if is_negative e then (not acc) (* opposite sign *)
        else raise Not_found) true es)
  with Not_found -> None

let match_positive_or_null e =
  if not (is_positive_or_null e) then raise Not_found;
  e

let match_power2, match_power2_minus1 =
  let highest_bit_number =
    let hsb p = if p land 2 = 0 then 0 else 1
    in let hsb p = let n = p lsr 2 in if n = 0 then hsb p else 2 + hsb n
    in let hsb p = let n = p lsr 4 in if n = 0 then hsb p else 4 + hsb n
    in let hsb = Array.init 256 hsb
    in let hsb p = let n = p lsr 8 in if n = 0 then hsb.(p) else 8 + hsb.(n)
    in let hsb p =
         let n = Integer.shift_right p Integer.sixteen in
         Integer.of_int (if Integer.is_zero n
                         then hsb (Integer.to_int_exn p)
                         else 16 + hsb (Integer.to_int_exn n))
    in let rec hsb_aux p =
         let n = Integer.shift_right p Integer.thirtytwo in
         if Integer.is_zero n then hsb p
         else Integer.add Integer.thirtytwo (hsb_aux n)
    in hsb_aux
  in let is_power2 k = (* exists n such that k == 2**n? *)
       (Integer.gt k Integer.zero) &&
       (Integer.equal k (Integer.logand k (Integer.neg k)))
  in let rec match_power2 e = match F.repr e with
      | Logic.Kint z
        when is_power2 z -> e_zint (highest_bit_number z)
      | Logic.Fun( f , [n;k] )
        when Fun.equal f f_lsl && is_positive_or_null k ->
          e_add k (match_power2 n)
      | _ -> raise Not_found
  in let match_power2_minus1 e = match F.repr e with
      | Logic.Kint z when is_power2 (Integer.succ z) ->
          e_zint (highest_bit_number (Integer.succ z))
      | _ -> match_power2 (e_add e_one e)
  in match_power2, match_power2_minus1

let match_fun op t =
  match F.repr t with
  | Logic.Fun( f , es ) when Fun.equal f op -> es
  | _ -> raise Not_found

let match_ufun uop t =
  match F.repr t with
  | Logic.Fun( f , e::[] ) when Fun.equal f uop -> e
  | _ -> raise Not_found

let match_positive_or_null_integer t =
  match F.repr t with
  | Logic.Kint c when Integer.le Integer.zero c -> c
  | _ -> raise Not_found

let match_binop_arg1 match_f = function (* for binop *)
  | [e1;e2] -> (match_f e1),e2
  | _ -> raise Not_found

let match_binop_arg2 match_f = function (* for binop *)
  | [e1;e2] -> e1,(match_f  e2)
  | _ -> raise Not_found

let match_list_head match_f = function
  | [] -> raise Not_found
  | e::es -> (match_f e), es

let match_binop_one_arg1 binop e = match F.repr e with
  | Logic.Fun( f , [one; e2] ) when Fun.equal f binop && one == e_one -> e2
  | _ -> raise Not_found

let match_list_extraction match_f =
  let match_f_opt n = try Some (match_f n) with Not_found -> None in
  let rec aux rs = function
    | [] -> raise Not_found
    | e::es ->
        match match_f_opt e with
        | Some k -> k, e, List.rev_append rs es
        | None -> aux (e::rs) es
  in aux []

let match_integer_arg1 = match_binop_arg1 match_integer

let match_positive_or_null_arg2 = match_binop_arg2 match_positive_or_null
let match_positive_or_null_integer_arg2 =
  match_binop_arg2 match_positive_or_null_integer

let match_integer_extraction = match_list_head match_integer

let match_power2_extraction = match_list_extraction match_power2
let match_power2_minus1_extraction = match_list_extraction match_power2_minus1
let match_binop_one_extraction binop = match_list_extraction (match_binop_one_arg1 binop)


(* -------------------------------------------------------------------------- *)
(* --- Conversion Symbols                                                 --- *)
(* -------------------------------------------------------------------------- *)

(* rule A: to_a(to_b x) = to_b x when domain(b) is all included in domain(a) *)
(* rule B: to_a(to_b x) = to_a x when range(b) is a multiple of range(a)
                          AND a is not bool *)

(* to_iota(e) where e = to_iota'(e'), only ranges for iota *)
let simplify_range_comp f iota e conv e' =
  let iota' = to_cint conv in
  let size' = Ctypes.i_bits iota' in
  let size = Ctypes.i_bits iota in
  if size <= size'
  then e_fun f [e']
  (* rule B:
     iota' is multiple of iota -> keep iota(e') *)
  else
  if ((Ctypes.signed iota) || not (Ctypes.signed iota'))
  then e
  (* rule A:
     have iota > iota' check sign to apply rule.
     unsigned iota -> iota' must be unsigned
     signed iota -> iota' can have any sign *)
  else raise Not_found

let simplify_f_to_bounds iota e =
  (* min(ctypes)<=y<=max(ctypes) ==> to_ctypes(y)=y *)
  let lower,upper = Ctypes.bounds iota in
  if (F.decide (F.e_leq e (e_zint upper))) &&
     (F.decide (F.e_leq (e_zint lower) e))
  then e
  else raise Not_found

let f_to_int = Ctypes.i_memo (fun iota -> make_fun_int "to" iota)

let configure_to_int iota =

  let simplify_range f iota e =
    begin
      try match F.repr e with
        | Logic.Kint value ->
            let size = Integer.of_int (Ctypes.i_bits iota) in
            let signed = Ctypes.signed iota in
            F.e_zint (Integer.cast ~size ~signed ~value)
        | Logic.Fun( fland , es )
          when Fun.equal fland f_land &&
               not (Ctypes.signed iota) &&
               List.exists is_positive_or_null es ->
            (* to_uintN(a) == a & (2^N-1) when a >= 0 *)
            let m = F.e_zint (snd (Ctypes.bounds iota)) in
            F.e_fun f_land (m :: es)
        | Logic.Fun( flor , es ) when (Fun.equal flor f_lor)
                                   && not (Ctypes.signed iota) ->
            (* to_uintN(a|b) == (to_uintN(a) | to_uintN(b)) *)
            F.e_fun f_lor (List.map (fun e' -> e_fun f [e']) es)
        | Logic.Fun( flnot , [ e ] ) when (Fun.equal flnot f_lnot)
                                       && not (Ctypes.signed iota) ->
            begin
              match F.repr e with
              | Logic.Fun( f' , w ) when f' == f ->
                  e_fun f [ e_fun f_lnot w ]
              | _ -> raise Not_found
            end
        | Logic.Fun( conv , [e'] ) -> (* unary op *)
            simplify_range_comp f iota e conv e'
        | _ -> raise Not_found
      with Not_found ->
        simplify_f_to_bounds iota e
    end
  in
  let simplify_conv f iota e =
    if iota = Ctypes.CBool then
      match F.is_equal e F.e_zero with
      | Yes -> F.e_zero
      | No -> F.e_one
      | Maybe -> raise Not_found
    else
      simplify_range f iota e
  in
  let simplify_leq f iota x y =
    let lower,upper = Ctypes.bounds iota in
    match F.repr y with
    | Logic.Fun( conv , [_] )
      when (Fun.equal conv f) &&
           (F.decide (F.e_leq x (e_zint lower))) ->
        (* x<=min(ctypes) ==> x<=to_ctypes(y) *)
        e_true
    | _ ->
        begin
          match F.repr x with
          | Logic.Fun( conv , [_] )
            when (Fun.equal conv f) &&
                 (F.decide (F.e_leq (e_zint upper) y)) ->
              (* max(ctypes)<=y ==> to_ctypes(y)<=y *)
              e_true
          | _ -> raise Not_found
        end
  in
  let f = f_to_int iota in
  F.set_builtin_1 f (simplify_conv f iota) ;
  F.set_builtin_leq f (simplify_leq f iota) ;
  to_cint_map := FunMap.add f iota !to_cint_map


let simplify_p_is_bounds iota e =
  let bounds = Ctypes.bounds iota in
  (* min(ctypes)<=y<=max(ctypes) <==> is_ctypes(y) *)
  match F.is_true (F.e_and
                     [F.e_leq (e_zint (fst bounds)) e;
                      F.e_leq e (e_zint (snd bounds))]) with
  | Logic.Yes -> e_true
  | Logic.No  -> e_false
  | _  -> raise Not_found

(* is_<cint> : int -> prop *)
let p_is_int = Ctypes.i_memo (fun iota -> make_pred_int "is" iota)

let configure_is_int iota =
  let f = p_is_int iota in
  let simplify = function
    | [e] ->
        begin
          match F.repr e with
          | Logic.Kint k ->
              let vmin,vmax = Ctypes.bounds iota in
              F.e_bool (Z.leq vmin k && Z.leq k vmax)
          | Logic.Fun( flor , es ) when (Fun.equal flor f_lor)
                                     && not (Ctypes.signed iota) ->
              (* is_uintN(a|b) == is_uintN(a) && is_uintN(b) *)
              F.e_and (List.map (fun e' -> e_fun f [e']) es)
          | _ -> simplify_p_is_bounds iota e
        end
    | _ -> raise Not_found
  in
  F.set_builtin f simplify;
  is_cint_map := FunMap.add f iota !is_cint_map

let convert i a = e_fun (f_to_int i) [a]

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

type model =
  | Natural (** Integer arithmetics with no upper-bound *)
  | Machine (** Integer/Module wrt Kernel options on RTE *)

let () =
  Context.register
    begin fun () ->
      Ctypes.i_iter configure_to_int;
      Ctypes.i_iter configure_is_int;
    end

let model = Context.create "Cint.model"
let current () = Context.get model
let configure m =
  let orig_model = Context.push model m in
  (fun () -> Context.pop model orig_model)

let to_integer a = a
let of_integer i a = convert i a
let of_real i a = convert i (Cmath.int_of_real a)

let range i a =
  match Context.get model with
  | Natural ->
      if Ctypes.signed i
      then F.p_true
      else F.p_leq F.e_zero a
  | Machine -> p_call (p_is_int i) [a]

let ensures warn i a =
  if warn i
  then a
  else e_fun (f_to_int i) [a]

let downcast = ensures is_downcast_an_error
let overflow = ensures is_overflow_an_error

(* -------------------------------------------------------------------------- *)
(* --- Arithmetics                                                        --- *)
(* -------------------------------------------------------------------------- *)

let binop f i x y  = overflow i (f x y)
let unop f i x = overflow i (f x)

(* C Code Semantics *)
let iopp = unop e_opp
let iadd = binop e_add
let isub = binop e_sub
let imul = binop e_mul
let idiv = binop e_div
let imod = binop e_mod

(* -------------------------------------------------------------------------- *)
(* --- Bits                                                               --- *)
(* -------------------------------------------------------------------------- *)

(* smp functions raise Not_found when simplification isn't possible *)

let smp1 zf =  (* f(c1) ~> zf(c1) *)
  function
  | [e] -> begin match F.repr e with
      | Logic.Kint c1 -> e_zint (zf c1)
      | _ -> raise Not_found
    end
  | _ -> raise Not_found

let smp2 f zf = (* f(c1,c2) ~> zf(c1,c2),  f(c1,c2,...) ~> f(zf(c1,c2),...) *)
  function
  | e1::e2::others -> begin match (F.repr e1), (F.repr e2) with
      (* integers should be at the beginning of the list *)
      | Logic.Kint c1, Logic.Kint c2 ->
          let z12 = ref (zf c1 c2) in
          let rec smp2 = function (* look at the other integers *)
            | [] -> []
            | (e::r) as l -> begin match F.repr e with
                | Logic.Kint c -> z12 := zf !z12 c; smp2 r
                | _ -> l
              end
          in let others = smp2 others
          in let c12 = e_zint !z12 in
          if others = [] || F.is_absorbant f c12
          then c12
          else if F.is_neutral f c12
          then e_fun f others
          else e_fun f (c12::others)
      | _ -> raise Not_found
    end
  | _ -> raise Not_found

let bitk_positive k e = F.e_fun ~result:Logic.Bool f_bit_positive [e;k]
let smp_mk_bit_stdlib = function
  | [ a ; k ] when is_positive_or_null k ->
      (* No need to expand the logic definition of the ACSL stdlib symbol when
         [k] is positive (the definition must comply with that simplification). *)
      bitk_positive k a
  | [ a ; k ] ->
      (* TODO: expand the current logic definition of the ACSL stdlib symbol *)
      F.e_neq F.e_zero (F.e_fun f_land [a; (F.e_fun f_lsl [F.e_one;k])])
  | _ -> raise Not_found

let smp_bitk_positive = function
  | [ a ; k ] -> (* requires k>=0 *)
      begin
        try e_eq (match_power2 a) k
        with Not_found ->
        match F.repr a with
        | Logic.Kint za ->
            let zk = match_integer k (* simplifies constants *)
            in if Integer.is_zero (Integer.logand za
                                     (Integer.shift_left Integer.one zk))
            then e_false else e_true
        | Logic.Fun( f , [e;n] ) when Fun.equal f f_lsr && is_positive_or_null n ->
            bitk_positive (e_add k n) e
        | Logic.Fun( f , [e;n] ) when Fun.equal f f_lsl && is_positive_or_null n ->
            begin match is_leq n k with
              | Logic.Yes -> bitk_positive (e_sub k n) e
              | Logic.No  -> e_false
              | Logic.Maybe -> raise Not_found
            end
        | Logic.Fun( f , es ) when Fun.equal f f_land ->
            F.e_and (List.map (bitk_positive k) es)
        | Logic.Fun( f , es ) when Fun.equal f f_lor ->
            F.e_or (List.map (bitk_positive k) es)
        | Logic.Fun( f , [a;b] ) when Fun.equal f f_lxor ->
            F.e_neq (bitk_positive k a) (bitk_positive k b)
        | Logic.Fun( f , [a] ) when Fun.equal f f_lnot ->
            F.e_not (bitk_positive k a)
        | Logic.Fun( conv , [a] ) (* when is_to_c_int conv *) ->
            let iota = to_cint conv in
            let range = Ctypes.i_bits iota in
            let signed = Ctypes.signed iota in
            if signed then (* beware of sign-bit *)
              begin match is_leq k (e_int (range-2)) with
                | Logic.Yes -> bitk_positive k a
                | Logic.No | Logic.Maybe -> raise Not_found
              end
            else begin match is_leq (e_int range) k with
              | Logic.Yes -> e_false
              | Logic.No -> bitk_positive k a
              | Logic.Maybe -> raise Not_found
            end
        | _ -> raise Not_found
      end
  | _ -> raise Not_found

let introduction_bit_test_positive es b =
  (* introduces bit_test(n,k) only when k>=0 *)
  let k,_,es = match_power2_extraction es in
  let es' = List.map (bitk_positive k) es in
  if b == e_zero then e_not (e_and es')
  else
    try let k' = match_power2 b in e_and ( e_eq k k' :: es' )
    with Not_found ->
      let bs = match_fun f_land b in
      let k',_,bs = match_power2_extraction bs in
      let bs' = List.map (bitk_positive k') bs in
      match F.is_true (F.e_eq k k') with
      | Logic.Yes -> e_eq (e_and es') (e_and bs')
      | Logic.No  -> e_and [e_not (e_and es'); e_not (e_and bs')]
      | Logic.Maybe -> raise Not_found

let smp_land es =
  let introduction_bit_test_positive_from_land es =
    if true then raise Not_found; (* [PB] true: until alt-ergo 0.95.2 trouble *)
    let k,e,es = match_power2_extraction es in
    let t = match es with
      | x::[] -> x
      | _ -> e_fun f_land es
    in e_if (bitk_positive k t) e e_zero
  in
  try let r = smp2 f_land Integer.logand es in
    try match F.repr r with
      | Logic.Fun( f , es ) when Fun.equal f f_land ->
          introduction_bit_test_positive_from_land es
      | _ -> r
    with Not_found -> r
  with Not_found -> introduction_bit_test_positive_from_land es

let smp_shift zf = (* f(e1,0)~>e1, c2>0==>f(c1,c2)~>zf(c1,c2), c2>0==>f(0,c2)~>0 *)
  function
  | [e1;e2] -> begin match (F.repr e1), (F.repr e2) with
      | _, Logic.Kint c2 when Z.equal c2 Z.zero -> e1
      | Logic.Kint c1, Logic.Kint c2 when Z.leq Z.zero c2 ->
          (* undefined when c2 is negative *)
          e_zint (zf c1 c2)
      | Logic.Kint c1, _ when Z.equal c1 Z.zero && is_positive_or_null e2 ->
          (* undefined when c2 is negative *)
          e1
      | _ -> raise Not_found
    end
  | _ -> raise Not_found

let smp_lnot = function
  | ([e] as args) -> begin match F.repr e with
      | Logic.Fun( f , [e] ) when Fun.equal f f_lnot ->
          (* ~~e ~> e *)
          e
      | _ -> smp1 Integer.lognot args
    end
  | _ -> raise Not_found

(* -------------------------------------------------------------------------- *)
(* --- Comparision with L-AND / L-OR / L-NOT                              --- *)
(* -------------------------------------------------------------------------- *)

let smp_leq_improved f a b =
  ignore (match_fun f b) ; (* It must be an improved of [is_positive_or_null f(args)] *)
  (* a <= 0 && 0 <= f(args) *)
  if F.decide (F.e_leq a F.e_zero) && is_positive_or_null b
  then e_true
  else raise Not_found

let smp_leq_with_land a b =
  try
    let es = match_fun f_land a in
    let a1,_ = match_list_head match_positive_or_null_integer es in
    if F.decide (F.e_leq (e_zint a1) b)
    then e_true
    else raise Not_found
  with Not_found ->
    (* a <= 0 && 0 <= (x&y) ==> a <= (x & y) *)
    smp_leq_improved f_land a b

let smp_eq_with_land a b =
  let es = match_fun f_land a in
  try
    try
      let b1 = match_integer b in
      try (* (b1&~a2)!=0 ==> (b1==(a2&e) <=> false) *)
        let a2,_ = match_integer_extraction es in
        if Integer.is_zero (Integer.logand b1 (Integer.lognot a2))
        then raise Not_found ;
        e_false
      with Not_found when b == e_minus_one ->
        (* -1==(a1&a2) <=> (-1==a1 && -1==a2) *)
        F.e_and (List.map (e_eq b) es)
    with Not_found -> introduction_bit_test_positive es b
  with Not_found ->
  try
    (* k>=0 & b1>=0 ==> (b1 & ((1 << k) -1) == b1 % (1 << k)  <==> true) *)
    let b1,b2 = match_mod b in
    let k = match_power2 b2 in
    (* note: a positive or null k is required by match_power2, match_power2_minus1 *)
    let k',_,es = match_power2_minus1_extraction es in
    if not ((is_positive_or_null b1) &&
            (F.decide (F.e_eq k k')) &&
            (F.decide (F.e_eq b1 (F.e_fun f_land es))))
    then raise Not_found ;
    F.e_true
  with Not_found ->
    (* k in {8,16,32,64} ==> (b1 & ((1 << k) -1) == to_cint_unsigned_bits(k, b1)  <==> true *)
    let iota,b1 = match_to_cint b in
    if Ctypes.signed iota then raise Not_found ;
    let n = Ctypes.i_bits iota in
    if n = 1 then
      (* rejects [to_bool()] that is not a modulo *)
      raise Not_found ;
    let k',_,es = match_power2_minus1_extraction es in
    let k' = match_integer k' in
    let k = Integer.of_int n in
    if not ((Integer.equal k k') &&
            (F.decide (F.e_eq b1 (F.e_fun f_land es))))
    then raise Not_found ;
    F.e_true

let smp_eq_with_lor a b =
  let b1 = match_integer b in
  let es = match_fun f_lor a in
  try (* b1==(a2|e) <==> (b1^a2)==(~a2&e) *)
    let a2,es = match_integer_extraction es in
    let k1 = Integer.logxor b1 a2 in
    let k2 = Integer.lognot a2 in
    e_eq (e_zint k1) (e_fun f_land [e_zint k2 ; e_fun f_lor es])
  with Not_found when b == e_zero ->
    (* 0==(a1|a2) <=> (0==a1 && 0==a2) *)
    F.e_and (List.map (e_eq b) es)

let smp_eq_with_lxor a b = (* b1==(a2^e) <==> (b1^a2)==e *)
  let b1 = match_integer b in
  let es = match_fun f_lxor a in
  try (* b1==(a2^e) <==> (b1^a2)==e *)
    let a2,es = match_integer_extraction es in
    let k1 = Integer.logxor b1 a2 in
    e_eq (e_zint k1) (e_fun f_lxor es)
  with Not_found when b == e_zero  ->
    (* 0==(a1^a2) <=> (a1==a2) *)
    (match es with
     | e1::e2::[] -> e_eq e1 e2
     | e1::((_::_) as e22) -> e_eq e1 (e_fun f_lxor e22)
     | _ -> raise Not_found)
     | Not_found when b == e_minus_one ->
         (* -1==(a1^a2) <=> (a1==~a2) *)
         (match es with
          | e1::e2::[] -> e_eq e1 (e_fun f_lnot [e2])
          | e1::((_::_) as e22) -> e_eq e1 (e_fun f_lnot [e_fun f_lxor e22])
          | _ -> raise Not_found)

let smp_eq_with_lnot a b =
  let e = match_ufun f_lnot a in
  try (* b1==~e <==> ~b1==e *)
    let b1 = match_integer b in
    let k1 = Integer.lognot b1 in
    e_eq (e_zint k1) e
  with Not_found ->(* ~b==~e <==> b==e *)
    let b = match_ufun f_lnot b in
    e_eq e b

(* -------------------------------------------------------------------------- *)
(* --- Comparision with LSL / LSR                                         --- *)
(* -------------------------------------------------------------------------- *)

let two_power_k k =
  try Integer.two_power k
  with Z.Overflow -> raise Not_found

let two_power_k_minus1 k =
  try Integer.pred (Integer.two_power k)
  with Z.Overflow -> raise Not_found

let smp_eq_with_lsl_cst a0 b0 =
  let b1 = match_integer b0 in
  let es = match_fun f_lsl a0 in
  try (* looks at the sd arg of a0 *)
    let e,a2= match_positive_or_null_integer_arg2 es in
    if not (Integer.is_zero (Integer.logand b1 (two_power_k_minus1 a2)))
    then
      (* a2>=0 && 0!=(b1 & ((2**a2)-1)) ==> ( (e<<a2)==b1 <==> false ) *)
      e_false
    else
      (* a2>=0 && 0==(b1 & ((2**a2)-1)) ==> ( (e<<a2)==b1 <==> e==(b1>>a2) ) *)
      e_eq e (e_zint (Integer.shift_right b1 a2))
  with Not_found -> (* looks at the fistt arg of a0 *)
    let a1,e= match_integer_arg1 es in
    if is_negative e then raise Not_found ;
    (* [PB] can be generalized to any term for a1 *)
    if Integer.le Integer.zero a1 && Integer.lt b1 a1 then
      (* e>=0 && 0<=a1 && b1<a1 ==> ( (a1<<e)==b1 <==> false ) *)
      e_false
    else if Integer.ge Integer.zero a1 && Integer.gt b1 a1 then
      (* e>=0 && 0>=a1 && b1>a1 ==> ( (a1<<e)==b1 <==> false ) *)
      e_false
    else raise Not_found

let smp_cmp_with_lsl cmp a0 b0 =
  if a0 == e_zero then
    let b,_ = match_fun f_lsl b0 |> match_positive_or_null_arg2 in
    cmp e_zero b (* q>=0 ==> ( (0 cmp(b<<q)) <==> (0 cmp b) ) *)
  else if b0 == e_zero then
    let a,_ = match_fun f_lsl a0 |> match_positive_or_null_arg2 in
    cmp a e_zero (* p>=0 ==> ( ((a<<p) cmp 0) <==> (a cmp 0) ) *)
  else
    let a,p = match_fun f_lsl a0 |> match_positive_or_null_arg2 in
    let b,q = match_fun f_lsl b0 |> match_positive_or_null_arg2 in
    if p == q then
      (* p>=0 && q>=0 && p==q ==> ( ((a<<p)cmp(b<<q)) <==> (a cmp b) ) *)
      cmp a b
    else if a == b && (cmp==e_eq || is_positive_or_null a) then
      (* p>=0 && q>=0 && a==b         ==> ( ((a<<p)== (b<<q)) <==> (p ==  q) ) *)
      (* p>=0 && q>=0 && a==b && a>=0 ==> ( ((a<<p)cmp(b<<q)) <==> (p cmp q) ) *)
      cmp p q
    else if a == b && is_negative a then
      (* p>=0 && q>=0 && a==b && a<0 ==> ( ((a<<p)cmp(b<<q)) <==> (q cmp p) ) *)
      cmp q p
    else
      let p = match_integer p in
      let q = match_integer q in
      if Z.lt p q then
        (* p>=0 && q>=0 && p>q ==> ( ((a<<p)cmp(b<<q)) <==> (a cmp(b<<(q-p))) ) *)
        cmp a (e_fun f_lsl [b;e_zint (Z.sub q p)])
      else if Z.lt q p then
        (* p>=0 && q>=0 && p<q ==> ( ((a<<p)cmp(b<<q)) <==> ((a<<(p-q)) cmp b) ) *)
        cmp (e_fun f_lsl [a;e_zint (Z.sub p q)]) b
      else
        (* p>=0 && q>=0 && p==q ==> ( ((a<<p)cmp(b<<q)) <==> (a cmp b) ) *)
        cmp a b

let smp_eq_with_lsl a b =
  try smp_eq_with_lsl_cst a b
  with Not_found -> smp_cmp_with_lsl e_eq a b

let smp_leq_with_lsl a b =
  try smp_cmp_with_lsl e_leq a b
  with Not_found ->
    (* a <= 0 && 0 <= (x << y) ==> a <= (x << y) *)
    smp_leq_improved f_lsl a b

let smp_eq_with_lsr a0 b0 =
  try
    let b1 = match_integer b0 in
    let e,a2 = match_fun f_lsr a0 |> match_positive_or_null_integer_arg2 in
    (* (e>>a2) == b1 <==> (e&~((2**a2)-1)) == (b1<<a2)
       That rule is similar to
       e/A2 == b2 <==> (e/A2)*A2 == b2*A2) with A2==2**a2
       So, A2>0 and (e/A2)*A2 == e&~((2**a2)-1)
    *)
    (* build (e&~((2**a2)-1)) == (b1<<a2) *)
    e_eq
      (e_zint (Integer.shift_left b1 a2))
      (e_fun f_land [e_zint (Integer.lognot (two_power_k_minus1 a2));e])
  with Not_found ->
    (* This rule takes into acount several cases.
       One of them is
       (a>>p) == (b>>(n+p)) <==> (a&~((2**p)-1)) == (b>>n)&~((2**p)-1)
       That rule is similar to
       (a/P) == (b/(N*P)) <==> (a/P)*P == ((b/N)/P)*P
       with P==2**p, N=2**n, q=p+n.
       So, (a/P)*P==a&~((2**p)-1), b/N==b>>n,  ((b/N)/P)*P==(b>>n)&~((2**p)-1)  *)
    let a,p = match_fun f_lsr a0 |> match_positive_or_null_integer_arg2 in
    let b,q = match_fun f_lsr b0 |> match_positive_or_null_integer_arg2 in
    let n = Integer.min p q in
    let a = if Integer.lt n p then e_fun f_lsr [a;e_zint (Z.sub p n)] else a in
    let b = if Integer.lt n q then e_fun f_lsr [b;e_zint (Z.sub q n)] else b in
    let m = F.e_zint (Integer.lognot (two_power_k_minus1 n)) in
    e_eq (e_fun f_land [a;m]) (e_fun f_land [b;m])

let smp_leq_with_lsr x y =
  try
    let a,p = match_fun f_lsr y |> match_positive_or_null_integer_arg2 in
    (* x <= (a >> p) with p >= 0 *)
    if x == e_zero then
      (* p >= 0 ==> ( 0 <= (a >> p) <==> 0 <= a )*)
      e_leq e_zero a
    else
      (* p >= 0 ==> ( x <= (a >> p) <==> x <= a/(2**p) ) *)
      let k = two_power_k p in
      e_leq x (e_div a (e_zint k))
  with Not_found ->
  try
    let a,p = match_fun f_lsr x |> match_positive_or_null_integer_arg2 in
    (* (a >> p) <= y with p >= 0 *)
    if y == e_zero then
      (* p >= 0 ==> ( (a >> p) <= 0 <==> a <= 0 ) *)
      e_leq a e_zero
    else
      (* p >= 0 ==> ( (a >> p) <= y <==> a/(2**p) <= y ) *)
      let k = two_power_k p in
      e_leq (e_div a (e_zint k)) y
  with Not_found ->
    (* x <= y && 0 <= (a&b) ==> x <= (a >> b) *)
    smp_leq_improved f_lsr x y


(* Rewritting at export *)
let bitk_export k e = F.e_fun ~result:Logic.Bool f_bit_export [e;k]
let export_eq_with_land a b =
  let es = match_fun f_land a in
  if b == e_zero then
    let k,_,es = match_binop_one_extraction f_lsl es in
    (* e1 & ... & en & (1 << k) = 0   <==> !bit_test(e1 & ... & en, k) *)
    e_not (bitk_export k (e_fun f_land es))
  else raise Not_found

(* ACSL Semantics *)
type l_builtin = {
  f: lfun ;
  eq: (term -> term -> term) option ;
  leq: (term -> term -> term) option ;
  smp: term list -> term ;
}

let () =
  Context.register
    begin fun () ->
      begin
        let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in

        (* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
           no creation of [e_fun f_bit_stdlib args] *)
        let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
        let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
        let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot smp_lnot ~leq:(smp_leq_improved f_lnot) in
        let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor ~leq:(smp_leq_improved f_lxor)
            (smp2 f_lxor Integer.logxor) in
        let bi_lor  = mk_builtin "f_lor" f_lor  ~eq:smp_eq_with_lor ~leq:(smp_leq_improved f_lor)
            (smp2 f_lor  Integer.logor) in
        let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
            smp_land in
        let bi_lsl  = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
            (smp_shift Integer.shift_left) in
        let bi_lsr  = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr
            (smp_shift Integer.shift_right) in

        List.iter
          begin fun (_name, { f; eq; leq; smp }) ->
            F.set_builtin f smp ;
            (match eq with
             | None -> ()
             | Some eq -> F.set_builtin_eq f eq);
            (match leq with
             | None -> ()
             | Some leq -> F.set_builtin_leq f leq)
          end
          [bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];

        Lang.For_export.set_builtin_eq f_land export_eq_with_land
      end
    end

(* ACSL Semantics *)
let l_not a   = e_fun f_lnot [a]
let l_xor a b = e_fun f_lxor [a;b]
let l_or  a b = e_fun f_lor  [a;b]
let l_and a b = e_fun f_land [a;b]
let l_lsl a b = e_fun f_lsl [a;b]
let l_lsr a b = e_fun f_lsr [a;b]

(* C Code Semantics *)

(* we need a (forced) conversion to properly encode
   the semantics of C in terms of the semantics in Z(ACSL).
   Typically, lnot(128) becomes (-129), which must be converted
   to obtain an unsigned. *)

let mask_unsigned i m =
  if Ctypes.signed i then m else convert i m

let bnot i x   = mask_unsigned i (l_not x)
let bxor i x y = mask_unsigned i (l_xor x y)

let bor _i  = l_or  (* no needs of range conversion *)
let band _i = l_and (* no needs of range conversion *)
let blsl i x y = overflow i (l_lsl x y) (* mult. by 2^y *)
let blsr _i = l_lsr (* div. by 2^y, never overflow *)

(** Simplifiers *)
let c_int_bounds_ival f  =
  let (umin,umax) = Ctypes.bounds f in
  Ival.inject_range (Some umin) (Some umax)

let max_reduce_quantifiers = 1000

module Dom = struct
  type t = Ival.t Tmap.t
  let is_top_ival = Ival.equal Ival.top

  let top = Tmap.empty

  [@@@ warning "-32"]
  let pretty fmt dom =
    Tmap.iter (fun k v ->
        Format.fprintf fmt "%a: %a,@ " Lang.F.pp_term k Ival.pretty v)
      dom

  let find t dom = Tmap.find t dom

  let get t dom = try find t dom with Not_found -> Ival.top

  let narrow t v dom =
    if Ival.is_bottom v then raise Lang.Contradiction
    else if is_top_ival v then dom
    else Tmap.change (fun _ v old ->
        match old with | None -> Some v
                       | (Some old) as old' ->
                           let v = Ival.narrow v old in
                           if Ival.is_bottom v then raise Lang.Contradiction;
                           if Ival.equal v old then old'
                           else Some v) t v dom

  let add_with_bot t v dom =
    if is_top_ival v then dom else Tmap.add t v dom

  let add t v dom =
    if Ival.is_bottom v then raise Lang.Contradiction;
    add_with_bot t v dom

  let remove t dom = Tmap.remove t dom

  let assume_cmp =
    let module Local = struct
      type t = Integer of Ival.t | Term of Ival.t option
    end in fun cmp t1 t2 dom ->
      let encode t = match Lang.F.repr t with
        | Kint z -> Local.Integer (Ival.inject_singleton z)
        | _ -> Local.Term (try Some (Tmap.find t dom) with Not_found -> None)
      in
      let term_dom = function
        | Some v -> v
        | None -> Ival.top
      in
      match encode t1, encode t2 with