From 0679240bc4ff7c72dd607cbb0ff879d1f65b979b Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Mon, 14 Aug 2023 20:38:26 +0100 Subject: [PATCH] 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 | 13 ++++++++----- backend/cn/context.ml | 10 ++++++++-- backend/cn/solver.ml | 15 +++++++++++++++ backend/cn/surfaceBaseTypes.ml | 4 ++++ backend/cn/terms.ml | 2 ++ backend/cn/wellTyped.ml | 3 +++ 6 files changed, 40 insertions(+), 7 deletions(-) diff --git a/backend/cn/baseTypes.ml b/backend/cn/baseTypes.ml index ecd27c4bf..8f0a1d321 100644 --- a/backend/cn/baseTypes.ml +++ b/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 diff --git a/backend/cn/context.ml b/backend/cn/context.ml index 8d5a89d47..30b5327b2 100644 --- a/backend/cn/context.ml +++ b/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; diff --git a/backend/cn/solver.ml b/backend/cn/solver.ml index da2d2923d..025e95b10 100644 --- a/backend/cn/solver.ml +++ b/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) -> diff --git a/backend/cn/surfaceBaseTypes.ml b/backend/cn/surfaceBaseTypes.ml index 2568f294d..271b6483d 100644 --- a/backend/cn/surfaceBaseTypes.ml +++ b/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 diff --git a/backend/cn/terms.ml b/backend/cn/terms.ml index 5754679d1..1af6b4d6e 100644 --- a/backend/cn/terms.ml +++ b/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" diff --git a/backend/cn/wellTyped.ml b/backend/cn/wellTyped.ml index ce7b4c4d9..3856b93b7 100644 --- a/backend/cn/wellTyped.ml +++ b/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 ->