summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Assumed.ml7
-rw-r--r--src/Collections.ml71
-rw-r--r--src/Contexts.ml13
-rw-r--r--src/Errors.ml1
-rw-r--r--src/Identifiers.ml32
-rw-r--r--src/InterpreterBorrowsCore.ml5
-rw-r--r--src/InterpreterUtils.ml18
-rw-r--r--src/Invariants.ml3
-rw-r--r--src/Names.ml4
-rw-r--r--src/Print.ml34
-rw-r--r--src/PureTypeCheck.ml5
-rw-r--r--src/Scalars.ml22
-rw-r--r--src/SynthesizeSymbolic.ml8
-rw-r--r--src/TranslateCore.ml10
-rw-r--r--src/Types.ml17
-rw-r--r--src/Values.ml2
-rw-r--r--src/ValuesUtils.ml6
-rw-r--r--src/dune34
18 files changed, 58 insertions, 234 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index b3128b9b..1e8bb669 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -38,13 +38,9 @@ module Sig = struct
(** A few utilities *)
let rvar_id_0 = T.RegionVarId.of_int 0
-
let rvar_0 : T.RegionVarId.id T.region = T.Var rvar_id_0
-
let rg_id_0 = T.RegionGroupId.of_int 0
-
let tvar_id_0 = T.TypeVarId.of_int 0
-
let tvar_0 : T.sty = T.TypeVar tvar_id_0
(** Region 'a of id 0 *)
@@ -218,8 +214,7 @@ module Sig = struct
let inputs =
[
mk_ref_ty rvar_0 (mk_vec_ty tvar_0) is_mut (* &'a (mut) Vec<T> *);
- mk_usize_ty;
- (* usize *)
+ mk_usize_ty (* usize *);
]
in
let output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *) in
diff --git a/src/Collections.ml b/src/Collections.ml
index 614857e6..2cb298a7 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -88,9 +88,7 @@ module type OrderedType = sig
include Map.OrderedType
val to_string : t -> string
-
val pp_t : Format.formatter -> t -> unit
-
val show_t : t -> string
end
@@ -99,9 +97,7 @@ module OrderedString : OrderedType with type t = string = struct
include String
let to_string s = s
-
let pp_t fmt s = Format.pp_print_string fmt s
-
let show_t s = s
end
@@ -109,7 +105,6 @@ module type Map = sig
include Map.S
val add_list : (key * 'a) list -> 'a t -> 'a t
-
val of_list : (key * 'a) list -> 'a t
val to_string : string option -> ('a -> string) -> 'a t -> string
@@ -123,7 +118,6 @@ module type Map = sig
*)
val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
-
val show : ('a -> string) -> 'a t -> string
end
@@ -132,7 +126,6 @@ module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
include Map
let add_list bl m = List.fold_left (fun s (key, e) -> add key e s) m bl
-
let of_list bl = add_list bl empty
let to_string indent_opt a_to_string m =
@@ -177,7 +170,6 @@ module type Set = sig
include Set.S
val add_list : elt list -> t -> t
-
val of_list : elt list -> t
val to_string : string option -> t -> string
@@ -191,7 +183,6 @@ module type Set = sig
*)
val pp : Format.formatter -> t -> unit
-
val show : t -> string
end
@@ -200,7 +191,6 @@ module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
include Set
let add_list bl s = List.fold_left (fun s e -> add e s) s bl
-
let of_list bl = add_list bl empty
let to_string indent_opt m =
@@ -239,79 +229,43 @@ end
*)
module type InjMap = sig
type key
-
type elem
-
type t
val empty : t
-
val is_empty : t -> bool
-
val mem : key -> t -> bool
-
val add : key -> elem -> t -> t
-
val singleton : key -> elem -> t
-
val remove : key -> t -> t
-
val compare : (elem -> elem -> int) -> t -> t -> int
-
val equal : (elem -> elem -> bool) -> t -> t -> bool
-
val iter : (key -> elem -> unit) -> t -> unit
-
val fold : (key -> elem -> 'b -> 'b) -> t -> 'b -> 'b
-
val for_all : (key -> elem -> bool) -> t -> bool
-
val exists : (key -> elem -> bool) -> t -> bool
-
val filter : (key -> elem -> bool) -> t -> t
-
val partition : (key -> elem -> bool) -> t -> t * t
-
val cardinal : t -> int
-
val bindings : t -> (key * elem) list
-
val min_binding : t -> key * elem
-
val min_binding_opt : t -> (key * elem) option
-
val max_binding : t -> key * elem
-
val max_binding_opt : t -> (key * elem) option
-
val choose : t -> key * elem
-
val choose_opt : t -> (key * elem) option
-
val split : key -> t -> t * elem option * t
-
val find : key -> t -> elem
-
val find_opt : key -> t -> elem option
-
val find_first : (key -> bool) -> t -> key * elem
-
val find_first_opt : (key -> bool) -> t -> (key * elem) option
-
val find_last : (key -> bool) -> t -> key * elem
-
val find_last_opt : (key -> bool) -> t -> (key * elem) option
-
val to_seq : t -> (key * elem) Seq.t
-
val to_seq_from : key -> t -> (key * elem) Seq.t
-
val add_seq : (key * elem) Seq.t -> t -> t
-
val of_seq : (key * elem) Seq.t -> t
-
val add_list : (key * elem) list -> t -> t
-
val of_list : (key * elem) list -> t
end
@@ -322,15 +276,11 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
module Set = MakeSet (Elem)
type key = Key.t
-
type elem = Elem.t
-
type t = { map : elem Map.t; elems : Set.t }
let empty = { map = Map.empty; elems = Set.empty }
-
let is_empty m = Map.is_empty m.map
-
let mem k m = Map.mem k m.map
let add k e m =
@@ -345,15 +295,10 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
| Some x -> { map = Map.remove k m.map; elems = Set.remove x m.elems }
let compare f m1 m2 = Map.compare f m1.map m2.map
-
let equal f m1 m2 = Map.equal f m1.map m2.map
-
let iter f m = Map.iter f m.map
-
let fold f m x = Map.fold f m.map x
-
let for_all f m = Map.for_all f m.map
-
let exists f m = Map.exists f m.map
(** Small helper *)
@@ -381,19 +326,12 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
(map_to_t map1, map_to_t map2)
let cardinal m = Map.cardinal m.map
-
let bindings m = Map.bindings m.map
-
let min_binding m = Map.min_binding m.map
-
let min_binding_opt m = Map.min_binding_opt m.map
-
let max_binding m = Map.max_binding m.map
-
let max_binding_opt m = Map.max_binding_opt m.map
-
let choose m = Map.choose m.map
-
let choose_opt m = Map.choose_opt m.map
let split k m =
@@ -403,19 +341,12 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
(l, data, r)
let find k m = Map.find k m.map
-
let find_opt k m = Map.find_opt k m.map
-
let find_first k m = Map.find_first k m.map
-
let find_first_opt k m = Map.find_first_opt k m.map
-
let find_last k m = Map.find_last k m.map
-
let find_last_opt k m = Map.find_last_opt k m.map
-
let to_seq m = Map.to_seq m.map
-
let to_seq_from k m = Map.to_seq_from k m.map
let rec add_seq s m =
@@ -428,8 +359,6 @@ module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
add_seq s m
let of_seq s = add_seq s empty
-
let add_list ls m = List.fold_left (fun m (key, elem) -> add key elem m) m ls
-
let of_list ls = add_list ls empty
end
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 4f1e1506..716326cf 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -62,7 +62,6 @@ let symbolic_value_id_counter, fresh_symbolic_value_id =
SymbolicValueId.fresh_stateful_generator ()
let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
-
let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()
let abstraction_id_counter, fresh_abstraction_id =
@@ -217,14 +216,9 @@ type type_context = {
}
[@@deriving show]
-type fun_context = {
- fun_decls : fun_decl FunDeclId.Map.t;
-}
-[@@deriving show]
+type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
-type global_context = {
- global_decls : global_decl GlobalDeclId.Map.t;
-}
+type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
[@@deriving show]
type eval_ctx = {
@@ -265,7 +259,8 @@ let ctx_lookup_fun_decl (ctx : eval_ctx) (fid : FunDeclId.id) : fun_decl =
FunDeclId.Map.find fid ctx.fun_context.fun_decls
(** TODO: make this more efficient with maps *)
-let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) : global_decl =
+let ctx_lookup_global_decl (ctx : eval_ctx) (gid : GlobalDeclId.id) :
+ global_decl =
GlobalDeclId.Map.find gid ctx.global_context.global_decls
(** Retrieve a variable's value in an environment *)
diff --git a/src/Errors.ml b/src/Errors.ml
index 69a030b1..31a53cf4 100644
--- a/src/Errors.ml
+++ b/src/Errors.ml
@@ -1,3 +1,2 @@
exception IntegerOverflow of unit
-
exception Unimplemented
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 61238aac..9f6a863d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -13,15 +13,10 @@ module type Id = sig
(** Id generator - simply a counter *)
val zero : id
-
val generator_zero : generator
-
val generator_from_incr_id : id -> generator
-
val fresh_stateful_generator : unit -> generator ref * (unit -> id)
-
val mk_stateful_generator : generator -> generator ref * (unit -> id)
-
val incr : id -> id
(* TODO: this should be stateful! - but we may want to be able to duplicate
@@ -30,29 +25,17 @@ module type Id = sig
TODO: change the order of the returned types
*)
val fresh : generator -> id * generator
-
val to_string : id -> string
-
val pp_id : Format.formatter -> id -> unit
-
val show_id : id -> string
-
val id_of_json : Yojson.Basic.t -> (id, string) result
-
val compare_id : id -> id -> int
-
val max : id -> id -> id
-
val min : id -> id -> id
-
val pp_generator : Format.formatter -> generator -> unit
-
val show_generator : generator -> string
-
val to_int : id -> int
-
val of_int : int -> id
-
val nth : 'a list -> id -> 'a
(* TODO: change the signature (invert the index and the list *)
@@ -75,9 +58,7 @@ module type Id = sig
val iteri : (id -> 'a -> unit) -> 'a list -> unit
module Ord : C.OrderedType with type t = id
-
module Set : C.Set with type elt = id
-
module Map : C.Map with type key = id
end
@@ -88,11 +69,9 @@ end
module IdGen () : Id = struct
(* TODO: use Z.t *)
type id = int [@@deriving show]
-
type generator = id [@@deriving show]
let zero = 0
-
let generator_zero = 0
let incr x =
@@ -113,13 +92,9 @@ module IdGen () : Id = struct
(g, fresh)
let fresh_stateful_generator () = mk_stateful_generator 0
-
let fresh gen = (gen, incr gen)
-
let to_string = string_of_int
-
let to_int x = x
-
let of_int x = x
let id_of_json js =
@@ -129,13 +104,9 @@ module IdGen () : Id = struct
| _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
let compare_id = compare
-
let max id0 id1 = if id0 > id1 then id0 else id1
-
let min id0 id1 = if id0 < id1 then id0 else id1
-
let nth v id = List.nth v id
-
let nth_opt v id = List.nth_opt v id
let rec update_nth vec id v =
@@ -158,11 +129,8 @@ module IdGen () : Id = struct
type t = id
let compare = compare
-
let to_string = to_string
-
let pp_t = pp_id
-
let show_t = show_id
end
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index d47989c3..f2f10944 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -582,7 +582,6 @@ let get_first_loan_in_value (v : V.typed_value) : V.loan_content option =
let obj =
object
inherit [_] V.iter_typed_value
-
method! visit_loan_content _ lc = raise (FoundLoanContent lc)
end
in
@@ -597,7 +596,6 @@ let get_first_borrow_in_value (v : V.typed_value) : V.borrow_content option =
let obj =
object
inherit [_] V.iter_typed_value
-
method! visit_borrow_content _ bc = raise (FoundBorrowContent bc)
end
in
@@ -700,7 +698,6 @@ let lookup_intersecting_aproj_borrows_opt (lookup_shared : bool)
let obj =
object
inherit [_] C.iter_eval_ctx as super
-
method! visit_abs _ abs = super#visit_abs (Some abs) abs
method! visit_abstract_shared_borrows abs asb =
@@ -791,7 +788,6 @@ let update_intersecting_aproj_borrows (can_update_shared : bool)
let obj =
object
inherit [_] C.map_eval_ctx as super
-
method! visit_abs _ abs = super#visit_abs (Some abs) abs
method! visit_abstract_shared_borrows abs asb =
@@ -920,7 +916,6 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
let obj =
object
inherit [_] C.map_eval_ctx as super
-
method! visit_abs _ abs = super#visit_abs (Some abs) abs
method! visit_aproj abs sproj =
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 6ef66f1d..fed5ff9b 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -12,33 +12,19 @@ module PA = Print.EvalCtxLlbcAst
(** Some utilities *)
let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
-
let ety_to_string = PA.ety_to_string
-
let rty_to_string = PA.rty_to_string
-
let symbolic_value_to_string = PA.symbolic_value_to_string
-
let borrow_content_to_string = PA.borrow_content_to_string
-
let loan_content_to_string = PA.loan_content_to_string
-
let aborrow_content_to_string = PA.aborrow_content_to_string
-
let aloan_content_to_string = PA.aloan_content_to_string
-
let aproj_to_string = PA.aproj_to_string
-
let typed_value_to_string = PA.typed_value_to_string
-
let typed_avalue_to_string = PA.typed_avalue_to_string
-
let place_to_string = PA.place_to_string
-
let operand_to_string = PA.operand_to_string
-
let statement_to_string ctx = PA.statement_to_string ctx "" " "
-
let statement_to_string_with_tab ctx = PA.statement_to_string ctx " " " "
let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
@@ -211,7 +197,6 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
let obj =
object
inherit [_] V.iter_typed_value
-
method! visit_Bottom _ = raise Found
method! visit_symbolic_value _ s =
@@ -238,7 +223,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
raise Found
else ()
| V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
- | V.SynthRetGivenBack -> ()
+ | V.SynthRetGivenBack ->
+ ()
| V.Global -> ()
end
in
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 81e35de3..ef255010 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -399,7 +399,6 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
let visitor =
object
inherit [_] C.iter_eval_ctx as super
-
method! visit_abs _ abs = super#visit_abs (Some abs) abs
method! visit_typed_value info tv =
@@ -705,9 +704,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
let obj =
object
inherit [_] C.iter_eval_ctx as super
-
method! visit_abs _ abs = super#visit_abs (Some abs) abs
-
method! visit_Symbolic _ sv = add_env_sv sv
method! visit_abstract_shared_borrows abs asb =
diff --git a/src/Names.ml b/src/Names.ml
index 0db5291a..209f8547 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -1,5 +1,4 @@
open Identifiers
-
module Disambiguator = IdGen ()
(** See the comments for [Name] *)
@@ -49,11 +48,8 @@ type name = path_elem list [@@deriving show, ord]
let to_name (ls : string list) : name = List.map (fun s -> Ident s) ls
type module_name = name [@@deriving show, ord]
-
type type_name = name [@@deriving show, ord]
-
type fun_name = name [@@deriving show, ord]
-
type global_name = name [@@deriving show, ord]
(** Filter the disambiguators equal to 0 in a name *)
diff --git a/src/Print.ml b/src/Print.ml
index 6b11a3ff..c10c5989 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -761,11 +761,9 @@ module LlbcAst = struct
global_decl_id_to_string;
}
- let fun_decl_to_ast_formatter
- (type_decls : T.type_decl T.TypeDeclId.Map.t)
+ let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
(fun_decls : A.fun_decl A.FunDeclId.Map.t)
- (global_decls : A.global_decl A.GlobalDeclId.Map.t)
- (fdef : A.fun_decl) :
+ (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) :
ast_formatter =
let rvar_to_string r =
let rvar = T.RegionVarId.nth fdef.signature.region_params r in
@@ -942,7 +940,8 @@ module LlbcAst = struct
| A.Assign (p, rv) ->
indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
| A.AssignGlobal { dst; global } ->
- indent ^ fmt.var_id_to_string dst ^ " := global " ^ fmt.global_decl_id_to_string global
+ indent ^ fmt.var_id_to_string dst ^ " := global "
+ ^ fmt.global_decl_id_to_string global
| A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p
| A.SetDiscriminant (p, variant_id) ->
(* TODO: improve this to lookup the variant name by using the def id *)
@@ -1132,11 +1131,9 @@ module Module = struct
(** Generate an [ast_formatter] by using a definition context in combination
with the variables local to a function's definition *)
- let def_ctx_to_ast_formatter
- (type_context : T.type_decl T.TypeDeclId.Map.t)
+ let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
(fun_context : A.fun_decl A.FunDeclId.Map.t)
- (global_context : A.global_decl A.GlobalDeclId.Map.t)
- (def : A.fun_decl) :
+ (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
PA.ast_formatter =
let rvar_to_string vid =
let var = T.RegionVarId.nth def.signature.region_params vid in
@@ -1188,23 +1185,28 @@ module Module = struct
(** This function pretty-prints a function definition by using a definition
context *)
- let fun_decl_to_string
- (type_context : T.type_decl T.TypeDeclId.Map.t)
+ let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
(fun_context : A.fun_decl A.FunDeclId.Map.t)
- (global_context : A.global_decl A.GlobalDeclId.Map.t)
- (def : A.fun_decl) : string =
- let fmt = def_ctx_to_ast_formatter type_context fun_context global_context def in
+ (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
+ string =
+ let fmt =
+ def_ctx_to_ast_formatter type_context fun_context global_context def
+ in
PA.fun_decl_to_string fmt "" " " def
let module_to_string (m : M.llbc_module) : string =
- let types_defs_map, funs_defs_map, globals_defs_map = M.compute_defs_maps m in
+ let types_defs_map, funs_defs_map, globals_defs_map =
+ M.compute_defs_maps m
+ in
(* The types *)
let type_decls = List.map (type_decl_to_string types_defs_map) m.M.types in
(* The functions *)
let fun_decls =
- List.map (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map) m.M.functions
+ List.map
+ (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
+ m.M.functions
in
(* Put everything together *)
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index 39fb5073..5aefb0be 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -40,7 +40,8 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
type tc_ctx = {
type_decls : type_decl TypeDeclId.Map.t; (** The type declarations *)
- global_decls : A.global_decl A.GlobalDeclId.Map.t; (** The global declarations *)
+ global_decls : A.global_decl A.GlobalDeclId.Map.t;
+ (** The global declarations *)
env : ty VarId.Map.t; (** Environment from variables to types *)
}
@@ -112,7 +113,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
check_texpression ctx body
| Qualif qualif -> (
match qualif.id with
- | Func _ -> () (* TODO *)
+ | Func _ -> () (* TODO *)
| Global _ -> () (* TODO *)
| Proj { adt_id = proj_adt_id; field_id } ->
(* Note we can only project fields of structures (not enumerations) *)
diff --git a/src/Scalars.ml b/src/Scalars.ml
index 3324c24b..03ca506c 100644
--- a/src/Scalars.ml
+++ b/src/Scalars.ml
@@ -4,43 +4,24 @@ open Values
(** The minimum/maximum values an integer type can have depending on its type *)
let i8_min = Z.of_string "-128"
-
let i8_max = Z.of_string "127"
-
let i16_min = Z.of_string "-32768"
-
let i16_max = Z.of_string "32767"
-
let i32_min = Z.of_string "-2147483648"
-
let i32_max = Z.of_string "2147483647"
-
let i64_min = Z.of_string "-9223372036854775808"
-
let i64_max = Z.of_string "9223372036854775807"
-
let i128_min = Z.of_string "-170141183460469231731687303715884105728"
-
let i128_max = Z.of_string "170141183460469231731687303715884105727"
-
let u8_min = Z.of_string "0"
-
let u8_max = Z.of_string "255"
-
let u16_min = Z.of_string "0"
-
let u16_max = Z.of_string "65535"
-
let u32_min = Z.of_string "0"
-
let u32_max = Z.of_string "4294967295"
-
let u64_min = Z.of_string "0"
-
let u64_max = Z.of_string "18446744073709551615"
-
let u128_min = Z.of_string "0"
-
let u128_max = Z.of_string "340282366920938463463374607431768211455"
(** Being a bit conservative about isize/usize: depending on the system,
@@ -48,11 +29,8 @@ let u128_max = Z.of_string "340282366920938463463374607431768211455"
want to take that into account in the future *)
let isize_min = i32_min
-
let isize_max = i32_max
-
let usize_min = u32_min
-
let usize_max = u32_max
(** Check that an integer value is in range *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index fa244649..a2256bdd 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -114,11 +114,9 @@ let synthesize_function_call (call_id : call_id)
in
Some (FunCall (call, expr))
-let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) (expr : expression option)
- : expression option =
- match expr with
- | None -> None
- | Some e -> Some (EvalGlobal (gid, dest, e))
+let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value)
+ (expr : expression option) : expression option =
+ match expr with None -> None | Some e -> Some (EvalGlobal (gid, dest, e))
let synthesize_regular_function_call (fun_id : A.fun_id)
(call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
diff --git a/src/TranslateCore.ml b/src/TranslateCore.ml
index e77445cd..326bb05f 100644
--- a/src/TranslateCore.ml
+++ b/src/TranslateCore.ml
@@ -24,7 +24,7 @@ type global_context = C.global_context [@@deriving show]
type trans_ctx = {
type_context : type_context;
fun_context : fun_context;
- global_context : global_context
+ global_context : global_context;
}
type pure_fun_translation = Pure.fun_decl * Pure.fun_decl list
@@ -46,7 +46,9 @@ let fun_sig_to_string (ctx : trans_ctx) (sg : Pure.fun_sig) : string =
let type_decls = ctx.type_context.type_decls in
let fun_decls = ctx.fun_context.fun_decls in
let global_decls = ctx.global_context.global_decls in
- let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
+ let fmt =
+ PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+ in
PrintPure.fun_sig_to_string fmt sg
let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
@@ -54,7 +56,9 @@ let fun_decl_to_string (ctx : trans_ctx) (def : Pure.fun_decl) : string =
let type_decls = ctx.type_context.type_decls in
let fun_decls = ctx.fun_context.fun_decls in
let global_decls = ctx.global_context.global_decls in
- let fmt = PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params in
+ let fmt =
+ PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
+ in
PrintPure.fun_decl_to_string fmt def
let fun_decl_id_to_string (ctx : trans_ctx) (id : A.FunDeclId.id) : string =
diff --git a/src/Types.ml b/src/Types.ml
index 5ff407c9..5bd172cb 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -1,12 +1,8 @@
open Identifiers
open Names
-
module TypeVarId = IdGen ()
-
module TypeDeclId = IdGen ()
-
module VariantId = IdGen ()
-
module FieldId = IdGen ()
module RegionVarId = IdGen ()
@@ -24,7 +20,6 @@ type ('id, 'name) indexed_var = {
[@@deriving show]
type type_var = (TypeVarId.id, string) indexed_var [@@deriving show]
-
type region_var = (RegionVarId.id, string option) indexed_var [@@deriving show]
(** A region.
@@ -82,13 +77,10 @@ type integer_type =
[@@deriving show, ord]
let all_signed_int_types = [ Isize; I8; I16; I32; I64; I128 ]
-
let all_unsigned_int_types = [ Usize; U8; U16; U32; U64; U128 ]
-
let all_int_types = List.append all_signed_int_types all_unsigned_int_types
type ref_kind = Mut | Shared [@@deriving show, ord]
-
type assumed_ty = Box | Vec | Option [@@deriving show, ord]
(** The variant id for `Option::None` *)
@@ -109,15 +101,10 @@ type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
class ['self] iter_ty_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
-
method visit_'r : 'env -> 'r -> unit = fun _ _ -> ()
-
method visit_id : 'env -> TypeVarId.id -> unit = fun _ _ -> ()
-
method visit_type_id : 'env -> type_id -> unit = fun _ _ -> ()
-
method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-
method visit_ref_kind : 'env -> ref_kind -> unit = fun _ _ -> ()
end
@@ -125,11 +112,8 @@ class ['self] iter_ty_base =
class ['self] map_ty_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
-
method visit_'r : 'env -> 'r -> 'r = fun _ r -> r
-
method visit_id : 'env -> TypeVarId.id -> TypeVarId.id = fun _ id -> id
-
method visit_type_id : 'env -> type_id -> type_id = fun _ id -> id
method visit_integer_type : 'env -> integer_type -> integer_type =
@@ -196,7 +180,6 @@ type ety = erased_region ty [@@deriving show, ord]
*)
type field = { field_name : string option; field_ty : sty } [@@deriving show]
-
type variant = { variant_name : string; fields : field list } [@@deriving show]
type type_decl_kind =
diff --git a/src/Values.ml b/src/Values.ml
index 13cd2580..fb927fb5 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -65,7 +65,7 @@ type sv_kind =
*)
| SynthInputGivenBack
(** The value was given back upon ending one of the input abstractions *)
- | Global (** The value is a global *)
+ | Global (** The value is a global *)
[@@deriving show]
type symbolic_value = {
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 2814615c..bc205622 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -11,7 +11,6 @@ let mk_unit_value : typed_value =
{ value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
let mk_typed_value (ty : ety) (value : value) : typed_value = { value; ty }
-
let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty }
(** Box a value *)
@@ -38,7 +37,6 @@ let borrows_in_value (v : typed_value) : bool =
let obj =
object
inherit [_] iter_typed_value
-
method! visit_borrow_content _env _ = raise Found
end
in
@@ -53,7 +51,6 @@ let inactivated_in_value (v : typed_value) : bool =
let obj =
object
inherit [_] iter_typed_value
-
method! visit_InactivatedMutBorrow _env _ = raise Found
end
in
@@ -68,7 +65,6 @@ let loans_in_value (v : typed_value) : bool =
let obj =
object
inherit [_] iter_typed_value
-
method! visit_loan_content _env _ = raise Found
end
in
@@ -84,9 +80,7 @@ let outer_loans_in_value (v : typed_value) : bool =
let obj =
object
inherit [_] iter_typed_value
-
method! visit_loan_content _env _ = raise Found
-
method! visit_borrow_content _ _ = ()
end
in
diff --git a/src/dune b/src/dune
index ba6c076b..ccf726c9 100644
--- a/src/dune
+++ b/src/dune
@@ -1,21 +1,25 @@
;; core: for Core.Unix.mkdir_p
+
(executable
(name main)
- (preprocess (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
+ (preprocess
+ (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
(libraries ppx_deriving yojson zarith easy_logging core_unix))
(env
- (dev (flags
- :standard
- -safe-string
- -g
- ;-dsource
- -warn-error -5-8-9-11-14-33-20-21-26-27-39
- ))
- (release (flags
- :standard
- -safe-string
- -g
- ;-dsource
- -warn-error -5-8-9-11-14-33-20-21-26-27-39
- )))
+ (dev
+ (flags
+ :standard
+ -safe-string
+ -g
+ ;-dsource
+ -warn-error
+ -5-8-9-11-14-33-20-21-26-27-39))
+ (release
+ (flags
+ :standard
+ -safe-string
+ -g
+ ;-dsource
+ -warn-error
+ -5-8-9-11-14-33-20-21-26-27-39)))