Add logical variable for allocation history

Right now it's added to the map and lost but (a) at least the types are
there and (b) an additionalc context record field will come later.

backend/cn/baseTypes.ml

@@ -5,6 +5,7 @@ type basetype =
  | Bool
  | Integer
  | Real
+ | Alloc_id
  | Loc
  | CType
  | Struct of Sym.t
@@ -47,6 +48,7 @@ let rec pp = function
  | Integer -> !^"integer"
  | Real -> !^"real"
  | Loc -> !^"pointer"
+ | Alloc_id -> !^"alloc_id"
  | CType -> !^"ctype"
  | Struct sym -> !^"struct" ^^^ Sym.pp sym
  | Datatype sym -> !^"datatype" ^^^ Sym.pp sym
@@ -117,11 +119,12 @@ let rec hash = function
  | Bool -> 1
  | Integer -> 2
  | Real -> 3
- | Loc -> 4
- | CType -> 5
- | List _ -> 6
- | Tuple _ -> 7
- | Set _ -> 8
+ | Alloc_id -> 4
+ | Loc -> 5
+ | CType -> 6
+ | List _ -> 7
+ | Tuple _ -> 8
+ | Set _ -> 9
  (* | Option _ -> 8 *)
  | Struct tag -> 1000 + Sym.num tag
  | Datatype tag -> 4000 + Sym.num tag

backend/cn/context.ml

@@ -48,9 +48,15 @@ type t = {
  }
 
 
-let empty = {
+let empty =
+ let alloc_id = Sym.fresh_named "__cn_alloc_history" in
+ let loc_str = __FILE__ ^ ":" ^ string_of_int __LINE__ in
+ let l_info = (Locations.other loc_str, lazy (Pp.string loc_str)) in
+ let bt = (BT.Map(Alloc_id, Record [(Id.id "base", Loc); (Id.id "len", Integer)])) in
+ let logical = SymMap.(empty |> add alloc_id (BaseType bt, l_info)) in
+ {
  computational = SymMap.empty;
- logical = SymMap.empty;
+ logical;
  resources = ([], 0);
  resource_history = IntMap.empty;
  constraints = LCSet.empty;

backend/cn/solver.ml

@@ -311,6 +311,11 @@ module Translate = struct
  (string (bt_name Loc))
  [string "loc_to_integer"] 
  [sort BT.Integer]
+ | Alloc_id ->
+ Z3.Tuple.mk_sort context
+ (string (bt_name Alloc_id))
+ [string "alloc_id_to_integer"]
+ [sort BT.Integer]
  | CType -> (* the ctype type is represented as an uninterpreted sort *)
  Z3.Sort.mk_uninterpreted_s context (bt_name CType)
  | List bt -> (* lists are represented as uninterpreted sorts *)
@@ -388,6 +393,9 @@ module Translate = struct
  Z3.Tuple.get_mk_decl (sort context global Loc)
 
 
+ let integer_to_alloc_id_fundecl context global =
+ Z3.Tuple.get_mk_decl (sort context global Alloc_id)
+
 
  let term ?(warn_lambda=true) context global : IT.t -> expr =
 
@@ -406,6 +414,10 @@ module Translate = struct
  Z3.Expr.mk_app context 
  (integer_to_loc_fundecl context global) [i] 
  in
+ let integer_to_alloc_id i =
+ Z3.Expr.mk_app context
+ (integer_to_alloc_id_fundecl context global) [i]
+ in
 
 
  let apply_matching_func sym_role fds args =
@@ -429,6 +441,9 @@ module Translate = struct
  | Const (Pointer z) -> 
  integer_to_loc
  (Z3.Arithmetic.Integer.mk_numeral_s context (Z.to_string z))
+ | Const (Alloc_id z) ->
+ integer_to_alloc_id
+ (Z3.Arithmetic.Integer.mk_numeral_s context (Z.to_string z))
  | Const (Bool true) -> 
  Z3.Boolean.mk_true context
  | Const (Bool false) -> 

backend/cn/surfaceBaseTypes.ml

@@ -8,6 +8,7 @@ type basetype =
  | Integer
  | Real
  | CType
+ | Alloc_id
  | Loc of Sctypes.t option
  | Struct of Sym.t
  | Datatype of Sym.t
@@ -49,6 +50,7 @@ let rec pp = function
  | Integer -> !^"integer"
  | Real -> !^"real"
  | CType -> !^"ctype"
+ | Alloc_id -> !^"alloc_id"
  | Loc (Some ct) -> !^"pointer" ^^ angles (Sctypes.pp ct)
  | Loc None -> !^"pointer"
  | Struct sym -> !^"struct" ^^^ Sym.pp sym
@@ -114,6 +116,7 @@ let rec of_basetype = function
  | BT.Integer -> Integer
  | BT.Real -> Real
  | BT.CType -> CType
+ | BT.Alloc_id -> Alloc_id
  | BT.Loc -> Loc None
  | BT.Struct tag -> Struct tag
  | BT.Datatype tag -> Datatype tag
@@ -130,6 +133,7 @@ let rec to_basetype = function
  | Integer -> BT.Integer
  | Real -> BT.Real
  | CType -> BT.CType
+ | Alloc_id -> BT.Alloc_id
  | Loc _ -> BT.Loc
  | Struct tag -> BT.Struct tag
  | Datatype tag -> BT.Datatype tag

backend/cn/terms.ml

@@ -5,6 +5,7 @@ type const =
  | Z of Z.t
  | Q of Q.t
  | Pointer of Z.t
+ | Alloc_id of Z.t
  | Bool of bool
  | Unit
  | Null
@@ -146,6 +147,7 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term -
  | Dec -> !^(Z.to_string i)
  | _ -> !^("0X" ^ (Z.format "016X" i))
  end
+ | Alloc_id i -> !^("@" ^ Z.to_string i)
  | Bool true -> !^"true"
  | Bool false -> !^"false"
  | Unit -> !^"void"

backend/cn/wellTyped.ml

@@ -101,6 +101,7 @@ module WBT = struct
  | Bool -> return ()
  | Integer -> return ()
  | Real -> return ()
+ | Alloc_id -> return ()
  | Loc -> return ()
  | CType -> return ()
  | Struct tag -> let@ _struct_decl = get_struct_decl loc tag in return ()
@@ -194,6 +195,8 @@ module WIT = struct
  return (IT (Const (Q q), Real))
  | Const (Pointer p) ->
  return (IT (Const (Pointer p), Loc))
+ | Const (Alloc_id p) ->
+ return (IT (Const (Alloc_id p), BT.Alloc_id))
  | Const (Bool b) ->
  return (IT (Const (Bool b), BT.Bool))
  | Const Unit ->