Change SMT-rep of pointers

As part of the changes to support VIP, the SMT backend needs to support
locations/pointers as a pair of allocation id (wrapped integers) and
addresss (integer). This commit makes that change in a trivial way:
by hard-coding every allocation id to be zero in the SMT representation.

backend/cn/indexTerms.ml

@@ -422,6 +422,7 @@ let is_pred_ = function
 (* lit *)
 let sym_ (sym, bt) = IT (Sym sym, bt)
 let z_ n = IT (Const (Z n), BT.Integer)
+let alloc_id_ n = IT (Const (Alloc_id n), BT.Alloc_id)
 let q_ (n,n') = IT (Const (Q (Q.make (Z.of_int n) (Z.of_int n'))), BT.Real)
 let q1_ q = IT (Const (Q q), BT.Real)
 let pointer_ n = IT (Const (Pointer n), BT.Loc)

backend/cn/solver.ml

@@ -207,6 +207,7 @@ module Translate = struct
  match bt with
  | BT.Struct nm -> !^ "struct_" ^^ Sym.pp nm
  | BT.Datatype nm -> !^ "datatype_" ^^ Sym.pp nm
+ | BT.Tuple [BT.Alloc_id; BT.Integer] -> !^ "pointer"
  | BT.Tuple _ -> !^ "tuple_" ^^ Pp.int (bt_id bt)
  | BT.List _ -> !^ "list_" ^^ Pp.int (bt_id bt)
  | BT.Set _ -> !^ "set_" ^^ Pp.int (bt_id bt)
@@ -306,11 +307,7 @@ module Translate = struct
  | Bool -> Z3.Boolean.mk_sort context
  | Integer -> Z3.Arithmetic.Integer.mk_sort context
  | Real -> Z3.Arithmetic.Real.mk_sort context
- | Loc ->
- Z3.Tuple.mk_sort context
- (string (bt_name Loc))
- [string "loc_to_integer"]
- [sort BT.Integer]
+ | Loc -> translate BT.(Tuple [Alloc_id; Integer])
  | Alloc_id ->
  Z3.Tuple.mk_sort context
  (string (bt_name Alloc_id))
@@ -386,17 +383,18 @@ module Translate = struct
  ()
 
 
- let loc_to_integer_fundecl context global =
+ let _loc_to_alloc_id_fundecl context global =
  nth (Z3.Tuple.get_field_decls (sort context global Loc)) 0
 
- let integer_to_loc_fundecl context global =
- Z3.Tuple.get_mk_decl (sort context global Loc)
+ let loc_to_integer_fundecl context global =
+ nth (Z3.Tuple.get_field_decls (sort context global Loc)) 1
 
+ let alloc_id_integer_to_loc_fundecl context global =
+ 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 =
 
  let struct_decls = global.struct_decls in
@@ -410,15 +408,16 @@ module Translate = struct
  Z3.Expr.mk_app context
  (loc_to_integer_fundecl context global) [l]
  in
- let integer_to_loc i =
- 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 alloc_id_integer_to_loc id i =
+ Z3.Expr.mk_app context
+ (alloc_id_integer_to_loc_fundecl context global) [id; i]
+ in
 
  let apply_matching_func sym_role fds args =
  let matching fd = equal_z3sym_table_entry sym_role
@@ -439,7 +438,8 @@ module Translate = struct
  | Const (Q q) ->
  Z3.Arithmetic.Real.mk_numeral_s context (Q.to_string q)
  | Const (Pointer z) ->
- integer_to_loc
+ alloc_id_integer_to_loc
+ (term (alloc_id_ Z.zero))
  (Z3.Arithmetic.Integer.mk_numeral_s context (Z.to_string z))
  | Const (Alloc_id z) ->
  integer_to_alloc_id
@@ -455,7 +455,9 @@ module Translate = struct
  let () = Z3Symbol_Table.add z3sym_table sym (DefaultFunc {bt}) in
  Z3.Expr.mk_const context sym (sort bt)
  | Const Null ->
- integer_to_loc (term (int_ 0))
+ alloc_id_integer_to_loc
+ (term (alloc_id_ Z.zero))
+ (term (int_ 0))
  | Const (CType_const ct) -> uninterp_term context (sort bt) it
  | Unop (uop, t) ->
  begin match uop with
@@ -597,7 +599,7 @@ module Translate = struct
  | Cast (cbt, t) ->
  begin match IT.bt t, cbt with
  | Integer, Loc ->
- integer_to_loc (term t)
+ alloc_id_integer_to_loc (term (alloc_id_ Z.zero)) (term t)
  | Loc, Integer ->
  loc_to_integer (term t)
  | Real, Integer ->
@@ -1139,13 +1141,23 @@ module Eval = struct
 
  | () when
  Z3.FuncDecl.equal func_decl
- (integer_to_loc_fundecl context global) ->
- let i = nth args 0 in
+ (alloc_id_integer_to_loc_fundecl context global) ->
+ let _id = nth args 0 in
+ let i = nth args 1 in
  begin match IT.is_z i with
  | Some z -> pointer_ z
  | _ -> integerToPointerCast_ i
  end
 
+ | () when
+ Z3.FuncDecl.equal func_decl
+ (integer_to_alloc_id_fundecl context global) ->
+ let i = nth args 0 in
+ begin match IT.is_z i with
+ | Some z -> alloc_id_ z
+ | _ -> assert false
+ end
+
  | () when Z3Symbol_Table.mem z3sym_table func_name ->
  begin match Z3Symbol_Table.find z3sym_table func_name with
  | DefaultFunc {bt} ->