Source file MemRegion.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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).            *)
(*                                                                        *)
(**************************************************************************)

(* TODO DEVEL MODE *)
[@@@ warning "-32-37-60"]

(* -------------------------------------------------------------------------- *)
(* --- Region Memory Model                                                 --- *)
(* -------------------------------------------------------------------------- *)

open Cil_types
open Sigs
open Definitions

module Wp = Wp_parameters
module F = Lang.F
module L = Qed.Logic

(* -------------------------------------------------------------------------- *)
(* --- Why-3 Region Theory                                                --- *)
(* -------------------------------------------------------------------------- *)

let library = "region"

let cluster_region () =
  Definitions.cluster ~id:"Region" ~title:"Region Index Constructors" ()

(* Index *)
let t_addr = MemAddr.t_addr
let t_index = L.Data( Lang.datatype ~library "index" ,[] )
let f_addrof = Lang.extern_f ~library ~result:t_addr "addrof"
let f_consistent = Lang.extern_fp ~library "consistent"
let f_consistent_range = Lang.extern_fp ~library "consistent_range"

let a_addrof l = F.e_fun f_addrof [l]
let p_consistent l = F.p_call f_consistent [l]
let p_consistent_range l n = F.p_call f_consistent_range [l;n]
let p_range k n ps = F.(p_leq e_zero k :: p_lt k n :: ps)

(* Null *)
let f_inull = Lang.extern_f ~library ~result:t_index "inull"
let l_inull = F.e_fun f_inull []
let p_inull l = F.p_equal MemAddr.null (a_addrof l)

(* Constructors *)
let region_ctor ~result =
  Lang.extern_f ~library ~category:L.Constructor ~result "%s"

let f_addr_var = region_ctor ~result:t_addr "addr_var"
let f_addr_ref = region_ctor ~result:t_addr "addr_ref"
let f_base_var = region_ctor ~result:L.Int "base_var"
let f_base_ref = region_ctor ~result:L.Int "base_ref"
let f_index_var = region_ctor ~result:t_index "index_var"
let f_index_ref = region_ctor ~result:t_index "index_ref"
let f_index_mem = region_ctor ~result:t_index "index_mem"

let a_addr_var x = F.e_fun f_addr_var [x]
let a_addr_ref p = F.e_fun f_addr_ref [p]
let l_index_var x = F.e_fun f_index_var [F.e_int x]
let l_index_mem l k n = F.e_fun f_index_ref [l;k;n]
let l_index_ref l = F.e_fun f_index_ref [l]

(* Shifts *)

let f_shift_index = Lang.extern_f ~library ~result:t_index "shift_index"
let l_shift_index l p = F.e_fun f_shift_index [l;p]

(* Bits *)
let t_bits = L.Int

(* -------------------------------------------------------------------------- *)
(* --- Index Simplifiers                                                  --- *)
(* -------------------------------------------------------------------------- *)

type index_builtin = {
  index: (Lang.lfun -> F.term list -> F.term -> F.term) ;
  addrof : (F.term list -> F.term) ;
  consistent : (F.term list -> F.pred) ;
}

module IndexBuiltin = WpContext.Static
    (struct
      type key = Lang.lfun
      type data = index_builtin
      let name = "MemRegion.INDEXER"
      include Lang.Fun
    end)

(* f enjoys shifting props:
   -  f(l,p,...)+k == f(l,p+k,...)
   - &f(l,p,...) = &l+p
*)
let is_shiftable f =
  ( f == f_shift_index ) || ( f == f_index_mem)

let phi_addrof index =
  match F.repr index with
  | L.Fun(f,[]) when f == f_inull -> MemAddr.null
  | L.Fun(f,[x]) when f == f_index_var -> a_addr_var x
  | L.Fun(f,[l]) when f == f_index_ref -> a_addr_ref (a_addrof l)
  | L.Fun(f,l::p::_) when is_shiftable f -> MemAddr.shift (a_addrof l) p
  | L.Fun(f,es) -> (IndexBuiltin.find f).addrof es
  | _ -> raise Not_found

let phi_shift_index l p =
  if p == F.e_zero then l else
    match F.repr l with
    | L.Fun(f,l::q::w) when is_shiftable f -> F.e_fun f (l::(F.e_add p q)::w)
    | L.Fun(f,es) -> (IndexBuiltin.find f).index f es p
    | _ -> raise Not_found

let phi_consistent index =
  match F.repr index with
  | L.Fun(f,[]) when f == f_inull -> F.e_false
  | L.Fun(f,[x]) when f == f_index_var ->
    F.e_neq x F.e_zero
  | L.Fun(f,[l]) when f == f_index_ref ->
    F.e_prop @@ p_consistent l
  | L.Fun(f,[l;k;n]) when f == f_index_mem ->
    F.e_prop @@ F.p_conj @@ p_range k n [p_consistent l]
  | L.Fun(f,es) ->
    F.e_prop @@ (IndexBuiltin.find f).consistent es
  | _ -> raise Not_found

let phi_consistent_range index sizeof =
  match F.repr index with
  | L.Fun(f,[l;k;n]) when f == f_index_mem ->
    F.e_prop @@ F.p_conj @@ F.[
        p_leq e_zero sizeof ;
        p_leq e_zero k ;
        p_leq (e_add k sizeof) n ;
        p_consistent l ;
      ]
  | _ -> raise Not_found

let () = Context.register
    begin fun () ->
      MemAddr.register f_addr_var
        ~base:(F.e_fun f_base_var) ~offset:(fun _ -> F.e_zero) ;
      MemAddr.register f_addr_ref
        ~base:(F.e_fun f_base_ref) ;
      F.set_builtin_1 f_addrof phi_addrof ;
      F.set_builtin_1 f_consistent phi_consistent ;
      F.set_builtin_2 f_shift_index phi_shift_index ;
      F.set_builtin_2 f_consistent_range phi_consistent_range ;
    end

let cid = ref 0 (* TODO: projectified *)

let constructor ~basename ~params ~index ~addrof ~consistent =
  let id = incr cid ; !cid in
  let lfun = Lang.generated_f ~result:t_index "%s_%d" basename id in
  let ps = List.map F.e_var params in
  let l = F.e_fun lfun ps in
  let k = Lang.freshvar ~basename:"k" L.Int in
  let ofs = F.e_var k in
  (* Must compute properties before registering simplifiers *)
  let p_addrof = F.p_equal (a_addrof l) (addrof ps) in
  let p_consistent = F.p_equiv (p_consistent l) (consistent ps) in
  let p_index = F.p_equal (l_shift_index l ofs) (index lfun ps ofs) in
  IndexBuiltin.define lfun { index ; addrof ; consistent } ;
  fun cluster ->
    begin
      Definitions.define_symbol {
        d_cluster = cluster ;
        d_lfun = lfun ; d_params = params ; d_types = 0 ;
        d_definition = Logic t_index ;
      } ;
      Definitions.define_lemma {
        l_cluster = cluster ;
        l_kind = Admit ;
        l_name = Printf.sprintf "addrof_%s_%d" basename id ;
        l_forall = params ; l_triggers = [] ;
        l_lemma = p_addrof ;
      } ;
      Definitions.define_lemma {
        l_cluster = cluster ;
        l_kind = Admit ;
        l_name = Printf.sprintf "consistent_%s_%d" basename id ;
        l_forall = params ; l_triggers = [] ;
        l_lemma = p_consistent ;
      } ;
      if p_index != F.p_true then
        Definitions.define_lemma {
          l_cluster = cluster ;
          l_kind = Admit ;
          l_name = Printf.sprintf "index_%s_%d" basename id ;
          l_forall = params @ [k] ; l_triggers = [] ;
          l_lemma = p_index ;
        } ;
      lfun
    end

(* -------------------------------------------------------------------------- *)
(* --- Field Index Constructors                                           --- *)
(* -------------------------------------------------------------------------- *)

module FIELD =
struct

  type t = int list (* Overlay offsets *)

  let pretty fmt = function
    | [] -> Format.fprintf fmt "{}"
    | p::ps ->
      begin
        Format.fprintf fmt "@[<hov 2>{%d" p ;
        List.iter (fun p -> Format.fprintf fmt ",@,%d" p) ps ;
        Format.fprintf fmt "}@]" ;
      end

  let compare = Stdlib.compare

  (* Extract constant offset *)
  let offset k =
    let rec walk s a =
      match F.repr a with
      | L.Add es -> List.fold_left walk s es
      | L.Kint z ->
        (try s + Integer.to_int_exn z
         with Z.Overflow -> s)
      | _ -> s
    in walk 0 k

  let builtin_index f es q = match es with
    | [l;p] -> F.e_fun f [l;F.e_add q p]
    | _ -> raise Not_found

  let builtin_addrof = function
    | [l;p] -> MemAddr.shift (a_addrof l) p
    | _ -> raise Not_found

  let builtin_consistent fds = function
    | [l;p] -> F.p_and (p_consistent l)
                 (F.p_any (fun fd -> F.p_equal (F.e_int fd) p) fds)
    | _ -> raise Not_found

end

(* Model Independant Generators *)
module FIELD_GEN = WpContext.StaticGenerator(FIELD)
    (struct
      type key = FIELD.t
      type data = cluster -> Lang.lfun
      let name = "MemRegion.FIELD_GEN"
      let compile fds =
        let l = Lang.freshvar ~basename:"l" t_index in
        let p = Lang.freshvar ~basename:"p" L.Int in
        constructor
          ~basename:"field"
          ~params:[l;p]
          ~index:FIELD.builtin_index
          ~addrof:FIELD.builtin_addrof
          ~consistent:(FIELD.builtin_consistent fds)
    end)

(* Model Dependent Definitions *)
module FIELD_MODEL = WpContext.Generator(FIELD)
    (struct
      type key = FIELD.t
      type data = Lang.lfun
      let name = "MemRegion.FIELD_MODEL"
      let compile fds = FIELD_GEN.get fds @@ cluster_region ()
    end)

let l_field ovl l k =
  let fds = List.map (fun rg -> rg.Layout.ofs) ovl in
  F.e_fun (FIELD_MODEL.get fds) [l;k]

(* -------------------------------------------------------------------------- *)
(* --- Array Index Constructors                                           --- *)
(* -------------------------------------------------------------------------- *)

module ARRAY =
struct

  type t = int * int list
  let compare = Stdlib.compare
  let pretty fmt (s,ds) = Format.fprintf fmt "%d%a" s Layout.Matrix.pretty ds

  (* Coefficient from Matrix dimensions: c_i = \Pi_{i<j} d_j *)
  let coefs s ds =
    let rec walk cs s = function
      | d::ds -> walk (s::cs) (d*s) ds
      | [] -> cs
    in walk [] s ds

  (* All zeroes *)
  let zeroes = List.map (fun _ -> F.e_zero)

  (* Address shift with coefficient c_i for each index k_i *)
  let rec shift a cs ks =
    match cs , ks with
    | c::cs , k::ks -> shift (MemAddr.shift a (F.e_fact c k)) cs ks
    | _ -> a

  (* Address of an array index *)
  let builtin_addrof cs = function
    | l::ks -> shift (a_addrof l) cs ks
    | _ -> raise Not_found

  (* Add conditions (0 <= ki < ni) to [ps].
     WARNING: ns = rev ds *)
  let rec add_range_dims ps ks ns =
    match ks , ns with
    | k::ks , n::ns ->
      add_range_dims F.(p_range k (e_int n) ps) ks ns
    | k::ks , [] ->
      add_range_dims F.(p_equal e_zero k :: ps) ks []
    | [] , _ -> ps

  (* Consistent index.
     WARNING: ns = rev ds *)
  let builtin_consistent ns = function
    | l::ks -> F.p_conj (add_range_dims [p_consistent l] ks ns)
    | _ -> raise Not_found

  (* Extract linear forms *)
  let rec get_linear poly a =
    match F.repr a with
    | L.Add es -> List.fold_left get_linear poly es
    | L.Kint z ->
      (try (Integer.to_int_exn z,F.e_one)::poly
       with Z.Overflow -> (1,a)::poly)
    | L.Times(c,e) ->
      (try (Integer.to_int_exn c,e)::poly
       with Z.Overflow -> (1,a)::poly)
    | _ -> (1,a)::poly

  (* Some of linear form *)
  let rec add_linear s = function
    | (k,e)::poly -> add_linear (F.e_add s (F.e_fact k e)) poly
    | [] -> s

  (* Euclidian division *)
  (* euclid q r ci p = q',r' <-> p + ci.q + r = ci.q' + r' *)
  let rec euclid q r ci = function
    | [] -> q,r
    | (c,k)::poly ->
      let q0 = c / ci in
      let r0 = c mod ci in
      euclid (F.e_add q (F.e_fact q0 k)) ((r0,k)::r) ci poly

  (* Linear offset decomposed on each coefficient *)
  let rec add_linear_index cs ks ks' p =
    match cs , ks with
    | c :: cs , k :: ks ->
      let k' , r = euclid k [] c p in
      add_linear_index cs ks (k'::ks') r
    | _ -> List.rev_append ks' ks , p

  (* Linear offset and remainder delta *)
  let offset cs ks p =
    let ks',r = add_linear_index cs ks [] (get_linear [] p) in
    ks' , add_linear F.e_zero r

  (* Builtin simplifier *)
  let builtin_index cs f es p = match es with
    | l::ks ->
      let ks' , r = offset cs ks p in
      if Qed.Hcons.equal_list F.equal ks ks' then
        raise Not_found
      else
        let l' = F.e_fun f (l :: ks) in
        l_shift_index l' r
    | _ -> raise Not_found

end

module ARRAY_GEN = WpContext.StaticGenerator(ARRAY)
    (struct
      type key = ARRAY.t
      type data = (cluster -> Lang.lfun)
      let name = "MemRegion.ARRAY_GEN"
      let compile (s,ds) =
        let l = Lang.freshvar ~basename:"l" t_index in
        let ks = List.map (fun _ -> Lang.freshvar ~basename:"k" L.Int) ds in
        let cs = ARRAY.coefs s ds in
        let ns = List.rev ds in
        constructor
          ~basename:"array"
          ~params:(l::ks)
          ~index:(ARRAY.builtin_index cs)
          ~addrof:(ARRAY.builtin_addrof cs)
          ~consistent:(ARRAY.builtin_consistent ns)
    end)

module ARRAY_MODEL = WpContext.Generator(ARRAY)
    (struct
      type key = ARRAY.t
      type data = Lang.lfun
      let name = "MemRegion.ARRAY_MODEL"
      let compile dim = ARRAY_GEN.get dim @@ cluster_region ()
    end)

let l_array s ds l ks = F.e_fun (ARRAY_MODEL.get (s,ds)) (l::ks)

(* -------------------------------------------------------------------------- *)
(* --- Model Context                                                      --- *)
(* -------------------------------------------------------------------------- *)

let datatype = "MemRegion"

let configure () =
  begin
    let orig_pointer = Context.push Lang.pointer t_index in
    let orig_null = Context.push Cvalues.null p_inull in
    let rollback () =
      Context.pop Lang.pointer orig_pointer ;
      Context.pop Cvalues.null orig_null
    in
    rollback
  end

let configure_ia =
  let no_binder = { bind = fun _ f v -> f v } in
  fun _vertex -> no_binder

let hypotheses p = p

let error msg = Warning.error ~source:"Region Model" msg

(* -------------------------------------------------------------------------- *)
(* --- Region Maps                                                        --- *)
(* -------------------------------------------------------------------------- *)

let map () =
  RegionAnalysis.get
    begin match WpContext.get_scope () with
      | WpContext.Global -> None
      | WpContext.Kf kf -> Some kf
    end

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

open Layout

type region = Region.region
type index = F.term

let pp_index = F.pp_term
let pp_region = Region.R.pretty
let pp_value = Value.pretty pp_region
let pp_args fmt = function
  | [] -> ()
  | k::ks ->
    F.pp_term fmt k ;
    List.iter (fun k -> Format.fprintf fmt "@,,%a" F.pp_term k) ks

let pp_field fmt k =
  if F.is_atomic k then
    Format.fprintf fmt "@,+%a" F.pp_term k
  else
    Format.fprintf fmt "@,+(%a)" F.pp_term k

let pp_delta fmt k =
  if k != F.e_zero then pp_field fmt k

type loc =
  | GarbledMix (* any possible location *)
  | Index of index (* unqualified address *)
  | Lref of region * index * region
  | Lmem of region * index * root * region value
  | Lraw of region * index * root * region option
  | Lfld of region * index * F.term * region overlay
  | Larr of region * index * F.term * F.term list * int * int list
  (* For Lxxx locations:
     - index: start index inside the chunk
     - term: additional shift index
     - term list: array index from start *)

(* -------------------------------------------------------------------------- *)
(* --- Loc Basics                                                         --- *)
(* -------------------------------------------------------------------------- *)

let null = Index l_inull

let vars = function
  | GarbledMix -> F.Vars.empty
  | Index l | Lref(_,l,_) | Lmem(_,l,_,_) | Lraw(_,l,_,_) -> F.vars l
  | Lfld(_,l,k,_) ->
    F.Vars.union (F.vars l) (F.vars k)
  | Larr(_,l,k,ks,_,_) ->
    Qed.Hcons.fold_list F.Vars.union F.vars F.Vars.empty (l::k::ks)

let occurs x = function
  | GarbledMix -> false
  | Index l | Lref(_,l,_) | Lmem(_,l,_,_) | Lraw(_,l,_,_) -> F.occurs x l
  | Lfld(_,l,k,_) ->
    F.occurs x l || F.occurs x k
  | Larr(_,l,k,ks,_,_) ->
    List.exists (F.occurs x) (l::k::ks)

let pretty fmt = function
  | GarbledMix -> Format.pp_print_string fmt "garbled-mix"
  | Index l ->
    Format.fprintf fmt "@[<hov 2>Index(%a)@]" pp_index l
  | Lref(r,l,r') ->
    Format.fprintf fmt "@[<hov 2>Ref@,{%a->%a}@,(%a)@]"
      pp_region r pp_region r' pp_index l
  | Lmem(r,l,_,v) ->
    Format.fprintf fmt "@[<hov 2>Mem@,{%a:@,%a}@,(%a)@]"
      pp_region r pp_value v pp_index l
  | Lraw(r,l,_,None) ->
    Format.fprintf fmt "@[<hov 2>Raw@,{%a}@,(%a)"
      pp_region r pp_index l
  | Lraw(r,l,_,Some r') ->
    Format.fprintf fmt "@[<hov 2>Raw@,{%a->%a}@,(%a)"
      pp_region r pp_region r' pp_index l
  | Lfld(r,l,k,_) ->
    Format.fprintf fmt "@[<hov 2>Field@,{%a}@,(%a%a)@]"
      pp_region r pp_index l pp_field k
  | Larr(r,l,k,ks,_,_) ->
    Format.fprintf fmt "@[<hov 2>Index@,{%a}@,@[<hov 2>(%a[%a]%a)@]@]"
      pp_region r pp_index l pp_args ks pp_delta k

(* -------------------------------------------------------------------------- *)
(* --- Loc Constructors                                                   --- *)
(* -------------------------------------------------------------------------- *)

let rec index map (r:region) (l:index)  (ofs:F.term) (len:int) =
  index_chunk map r l ofs len (Region.chunk map r)

and index_chunk map (r:region) l ofs len = function
  | Mref r' -> Lref(r,l_shift_index l ofs,r')
  | Mraw(m,p) -> Lraw(r,l_shift_index l ofs,m,p)
  | Mmem(m,v) -> Lmem(r,l_shift_index l ofs,m,v)
  | Mcomp(_,[{ofs=0;reg;dim}]) -> index_dim map reg l ofs len dim
  | Mcomp(_,overlay) -> index_field map r l ofs len overlay

and index_field map r l ofs len overlay =
  try
    let k = FIELD.offset ofs in
    let rg = List.find (Layout.Range.included k len) overlay in
    let fd = F.e_int k in
    let l' = l_field overlay l fd in
    index_dim map rg.reg l' (F.e_sub ofs fd) len rg.dim
  with Not_found ->
    Lfld(r,l,ofs,overlay)

and index_dim map r l ofs len = function
  | Raw s | Dim(s,[]) ->
    index map r (l_index_mem l F.e_zero (F.e_int s)) ofs len
  | Dim(s,ds) ->
    index_array map r l (ARRAY.zeroes ds) ofs len s ds

and index_array map r l ks ofs len s ds =
  let cs = ARRAY.coefs s ds in
  let ks,ofs = ARRAY.offset cs ks ofs in
  if len <= s then
    let l' = l_array s ds l ks in
    index map r l' ofs len
  else
    Larr(r,l,ofs,ks,s,ds)

and shift_index_loc map loc ofs len =
  match loc with
  | GarbledMix -> GarbledMix
  | Index l -> Index (l_shift_index l ofs)
  | Lref(r,l,r') -> Lref(r,l_shift_index l ofs,r')
  | Lmem(r,l,m,v) -> Lmem(r,l_shift_index l ofs,m,v)
  | Lraw(r,l,m,p) -> Lraw(r,l_shift_index l ofs,m,p)
  | Lfld(r,l,k,overlay) -> index_field map r l (F.e_add k ofs) len overlay
  | Larr(r,l,k,ks,s,ds) -> index_array map r l ks (F.e_add k ofs) len s ds

let cvar x =
  let map = map () in
  let region = Region.of_cvar map x in
  let id = if Cil.isConstType x.vtype then - x.vid else x.vid in
  index map region (l_index_var id) F.e_zero (Cil.bitsSizeOf x.vtype)

let field loc fd =
  let map = map () in
  let ofs,len = Region.field_offset map fd in
  shift_index_loc map loc (F.e_int ofs) len

let shift loc obj n =
  let map = map () in
  let s = Ctypes.bits_sizeof_object obj in
  shift_index_loc map loc (F.e_fact s n) s

let pointer_loc l = Index l
let pointer_val = function
  | GarbledMix -> error "Can not obtain address of Garbled-Mix location"
  | Index l | Lref(_,l,_) | Lmem(_,l,_,_) | Lraw(_,l,_,_) -> l
  | Lfld(_,l,k,overlay) -> l_field overlay l k
  | Larr(_,l,k,ks,s,ds) -> l_shift_index (l_array s ds l ks) k

let loc_of_index re ty l =
  index (map()) re l F.e_zero (Cil.bitsSizeOf ty)

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

type chunk =
  | Mu_alloc
  | Mu_raw of region * root
  | Mu_mem of region * root * region value

module Chunk =
struct

  type t = chunk
  let self = "region"

  let id = function
    | Mu_raw(r,_) | Mu_mem(r,_,_) -> Region.id r
    | Mu_alloc -> Region.noid

  let hash m = id m
  let compare m m' =
    if m==m then 0 else Stdlib.compare (id m) (id m')
  let equal m m' = m==m' || (id m = id m')

  let tau_of_value = function
    | Int _ -> L.Int
    | Float _ -> L.Real
    | Pointer _ -> t_index

  let tau_of_chunk = function
    | Mu_alloc -> MemMemory.t_malloc
    | Mu_raw _ -> t_bits
    | Mu_mem(_,root,v) ->
      let value = tau_of_value v in
      if Root.indexed root then L.Array(t_addr,value) else value

  let basename_of_chunk = function
    | Mu_raw _ -> "B"
    | Mu_mem(_,root,Int _) -> if Root.indexed root then "M" else "V"
    | Mu_mem(_,root,Float _) -> if Root.indexed root then "Mf" else "F"
    | Mu_mem(_,root,Pointer _) -> if Root.indexed root then "Mp" else "M"
    | Mu_alloc -> "A"

  let is_framed = function
    | Mu_raw(_,root) | Mu_mem(_,root,_) -> Root.framed root
    | Mu_alloc -> false

  let pretty fmt mu = Format.pp_print_string fmt (basename_of_chunk mu)

end

module Heap =
struct
  include Qed.Collection.Make(Chunk)
  let empty = Set.empty
  let of_raw r rt = Set.singleton (Mu_raw(r,rt))
  let of_mem r rt v = Set.singleton (Mu_mem(r,rt,v))

  let rec of_region map r =
    match Region.chunk map r with
    | Mref _ -> Set.empty
    | Mraw(rt,_) -> of_raw r rt
    | Mmem(rt,v) -> of_mem r rt v
    | Mcomp(_,overlay) -> of_overlay map overlay

  and of_range map { reg } = of_region map reg

  and of_overlay map ovl =
    Qed.Hcons.fold_list Set.union (of_range map) empty ovl

end
module Sigma = Sigma.Make(Chunk)(Heap)

type sigma = Sigma.t
type domain = Sigma.domain

let value_footprint _obj = function
  | GarbledMix | Index _ -> error "Can not compute Garbled-mix domain"
  | Lref _ -> Heap.empty
  | Lraw(r,_,rt,_) -> Heap.of_raw r rt
  | Lmem(r,_,rt,v) -> Heap.of_mem r rt v
  | Lfld(_,_,_,ovl) -> Heap.of_overlay (map()) ovl
  | Larr(r,_,_,_,_,_) -> Heap.of_region (map()) r

let init_footprint _ _ = Heap.empty

let is_well_formed _s = Lang.F.p_true

let region_of_loc = function
  | (GarbledMix | Index _) as l -> error "Can not find region of %a" pretty l
  | Lref(r,_,_) | Lraw(r,_,_,_) | Lmem(r,_,_,_)
  | Lfld(r,_,_,_) | Larr(r,_,_,_,_,_) -> r

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

module MODEL =
struct

  module Chunk = Chunk
  module Sigma = Sigma
  let name = "MemRegion.LOADER"
  type nonrec loc = loc
  let field = field
  let shift = shift
  let sizeof obj = Lang.F.e_int (Ctypes.bits_sizeof_object obj)
  let value_footprint = value_footprint
  let init_footprint = init_footprint
  let frames _ _ _ = []

  let to_addr l = a_addrof (pointer_val l)
  let to_region_pointer l = Region.id (region_of_loc l) , pointer_val l
  let of_region_pointer r obj l =
    let map = map () in
    index map (Region.region map r) l F.e_zero (Ctypes.bits_sizeof_object obj)

  let load_mem sigma r rt v l =
    let m = Sigma.value sigma (Mu_mem(r,rt,v)) in
    if Root.indexed rt then F.e_get m (a_addrof l) else m

  let load_int sigma i = function
    | Lmem(r,l,rt,(Int i0 as v)) when i = i0 -> load_mem sigma r rt v l
    | l -> error "Can not load %a value from %a" Ctypes.pp_int i pretty l

  let load_float sigma f = function
    | Lmem(r,l,rt,(Float f0 as v)) when f = f0 -> load_mem sigma r rt v l
    | l -> error "Can not load %a value from %a" Ctypes.pp_float f pretty l

  let load_pointer sigma ty = function
    | Lmem(r,l,rt,(Pointer r' as v)) ->
      loc_of_index r' ty (load_mem sigma r rt v l)
    | Lref(_,l,r') ->
      loc_of_index r' ty (l_index_ref l)
    | l -> error "Can not load pointer value from %a" pretty l

  let havoc obj loc ~length (chunk:chunk) ~fresh ~current =
    match chunk with
    | Mu_alloc -> fresh
    | Mu_raw _ -> error "Can not havoc raw memories"
    | Mu_mem(_,root,_) ->
      if Layout.Root.indexed root then
        let addr = to_addr loc in
        let offset = F.e_fact (Ctypes.bits_sizeof_object obj) length in
        F.e_fun MemMemory.f_havoc [fresh;current;addr;offset]
      else
        fresh

  let eqmem obj loc chunk m1 m2 =
    match chunk with
    | Mu_alloc -> error "Can not compare allocation tables"
    | Mu_raw _ -> error "Can not compare raw memories"
    | Mu_mem(_,root,_) ->
      if Layout.Root.indexed root then
        let addr = to_addr loc in
        let offset = F.e_int (Ctypes.bits_sizeof_object obj) in
        F.p_call MemMemory.p_eqmem [m1;m2;addr;offset]
      else F.p_equal m1 m2

  let eqmem_forall obj loc chunk m1 m2 =
    match chunk with
    | Mu_alloc -> error "Can not compare allocation tables"
    | Mu_raw _ -> error "Can not compare raw memories"
    | Mu_mem(_,root,_) ->
      if Layout.Root.indexed root then
        let xp = Lang.freshvar ~basename:"p" t_addr in
        let p = F.e_var xp in
        let a = to_addr loc in
        let n = F.e_int (Ctypes.bits_sizeof_object obj) in
        let separated = F.p_call MemAddr.p_separated [ p ; F.e_one ; a ; n ] in
        let equal = F.p_equal (F.e_get m1 p) (F.e_get m2 p) in
        [xp],separated,equal
      else [],F.p_true,F.p_equal m1 m2

  let last _ = error "Can not compute last valid index"

  let store_mem sigma r rt v l value =
    let c = Mu_mem(r,rt,v) in
    if Root.indexed rt then
      c , F.e_set (Sigma.value sigma c) (a_addrof l) value
    else c , value

  let store_int sigma i loc value =
    match loc with
    | Lmem(r,l,rt,(Int i0 as v)) when i = i0 -> store_mem sigma r rt v l value
    | _ -> error "Can not store %a value into %a" Ctypes.pp_int i pretty loc

  let store_float sigma f loc value =
    match loc with
    | Lmem(r,l,rt,(Float f0 as v)) when f = f0 -> store_mem sigma r rt v l value
    | _ -> error "Can not store %a value into %a" Ctypes.pp_float f pretty loc

  let store_pointer sigma _ty loc value =
    match loc with
    | Lmem(r,l,rt,(Pointer _ as v)) -> store_mem sigma r rt v l value
    | _ -> error "Can not store pointer values into %a" pretty loc

  let set_init_atom _ _ _ = assert false
  let set_init _obj _loc ~length _chunk ~current =
    let _ = length in
    let _ = current in
    assert false
  let is_init_atom _ _ = assert false
  let is_init_range _ _ _ _ = assert false
  let monotonic_init _ _ = assert false

end

module LOADER = MemLoader.Make(MODEL)

let load = LOADER.load
let load_init = LOADER.load_init
let load_value = LOADER.load_value

let stored = LOADER.stored
let stored_init = LOADER.stored_init
let copied = LOADER.copied
let copied_init = LOADER.copied_init
let assigned = LOADER.assigned
let initialized = LOADER.initialized

let domain = LOADER.domain

(* -------------------------------------------------------------------------- *)
(* ---  Loc Segments                                                      --- *)
(* -------------------------------------------------------------------------- *)

type segment = loc rloc

let region_of_sloc = function Rloc(_,l) | Rrange(l,_,_,_) -> region_of_loc l

let disjoint_region s1 s2 =
  let map = map () in
  let c1 = Region.chunks map (region_of_sloc s1) in
  let c2 = Region.chunks map (region_of_sloc s2) in
  not (Qed.Intset.intersect c1 c2)


let addrof = MODEL.to_addr
let sizeof = MODEL.sizeof

let included s1 s2 =
  if disjoint_region s1 s2 then F.p_false else
    MemAddr.included ~shift ~addrof ~sizeof s1 s2

let separated s1 s2 =
  if disjoint_region s1 s2 then F.p_true else
    MemAddr.separated ~shift ~addrof ~sizeof s1 s2

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

type state = unit

let state _ = ()
let iter _ _ = ()
let lookup _ _ = Mterm
let updates _ _ = Bag.empty
let apply _ _ = ()

let literal ~eid _ = ignore eid ; GarbledMix

let base_addr _l = GarbledMix
let base_offset l = MemAddr.offset (addrof l)
let block_length _s _obj _l = F.e_zero

let cast _ _l = GarbledMix
let loc_of_int _ _ = GarbledMix
let int_of_loc _ _ = F.e_zero

let not_yet_pointer () = error "Pointer comparison not yet implemented"

let is_null _ = not_yet_pointer ()
let loc_eq _ _ = not_yet_pointer ()
let loc_lt _ _ = not_yet_pointer ()
let loc_leq _ _ = not_yet_pointer ()
let loc_neq _ _ = not_yet_pointer ()
let loc_diff _ _ _ = not_yet_pointer ()

let frame _sigma = []
let alloc sigma _xs = sigma
let scope _seq _s _xs = []
let valid _sigma _acs _l = error "Validity not yet implemented"
let invalid _sigma _l = error "Validity not yet implemented"
let global _sigma _p = F.p_true