summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Assumed.ml6
-rw-r--r--compiler/Collections.ml379
-rw-r--r--compiler/Contexts.ml1
-rw-r--r--compiler/Crates.ml91
-rw-r--r--compiler/Errors.ml3
-rw-r--r--compiler/Expressions.ml119
-rw-r--r--compiler/ExpressionsUtils.ml11
-rw-r--r--compiler/Identifiers.ml140
-rw-r--r--compiler/InterpreterStatements.ml18
-rw-r--r--compiler/InterpreterUtils.ml6
-rw-r--r--compiler/LlbcAst.ml190
-rw-r--r--compiler/LlbcAstUtils.ml61
-rw-r--r--compiler/LlbcOfJson.ml918
-rw-r--r--compiler/Logging.ml138
-rw-r--r--compiler/Meta.ml45
-rw-r--r--compiler/Names.ml81
-rw-r--r--compiler/OfJsonBasic.ml75
-rw-r--r--compiler/PrimitiveValues.ml42
-rw-r--r--compiler/Print.ml732
-rw-r--r--compiler/PrintPure.ml2
-rw-r--r--compiler/Pure.ml6
-rw-r--r--compiler/PureMicroPasses.ml26
-rw-r--r--compiler/Scalars.ml60
-rw-r--r--compiler/Types.ml209
-rw-r--r--compiler/TypesUtils.ml164
-rw-r--r--compiler/Utils.ml7
-rw-r--r--compiler/Values.ml2
-rw-r--r--compiler/dune9
-rw-r--r--compiler/dune-project2
29 files changed, 57 insertions, 3486 deletions
diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index cb089c08..7fba3c5c 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -6,9 +6,9 @@
Semantically speaking, we thus handle [Box::free] as a value drop and
not as a function call, and thus never need its signature.
- TODO: implementing the concrete evaluation functions for the assumed
- functions is really annoying (see
- [InterpreterStatements.eval_non_local_function_call_concrete]).
+ TODO: implementing the concrete evaluation functions for the
+ assumed functions is really annoying (see
+ {!InterpreterStatements.eval_non_local_function_call_concrete}),
I think it should be possible, in most situations, to write bodies which
model the behaviour of those unsafe functions. For instance, [Box::deref_mut]
should simply be:
diff --git a/compiler/Collections.ml b/compiler/Collections.ml
index 0933b3e4..0b24004f 100644
--- a/compiler/Collections.ml
+++ b/compiler/Collections.ml
@@ -1,378 +1 @@
-(** The following file redefines several modules like Map or Set. *)
-
-module F = Format
-
-module List = struct
- include List
-
- (** Split a list at a given index.
-
- [split_at ls i] splits [ls] into two lists where the first list has
- length [i].
-
- Raise [Failure] if the list is too short.
- *)
- let rec split_at (ls : 'a list) (i : int) =
- if i < 0 then raise (Invalid_argument "split_at take positive integers")
- else if i = 0 then ([], ls)
- else
- match ls with
- | [] ->
- raise
- (Failure "The int given to split_at should be <= the list's length")
- | x :: ls' ->
- let ls1, ls2 = split_at ls' (i - 1) in
- (x :: ls1, ls2)
-
- (** Pop the last element of a list
-
- Raise [Failure] if the list is empty.
- *)
- let rec pop_last (ls : 'a list) : 'a list * 'a =
- match ls with
- | [] -> raise (Failure "The list is empty")
- | [ x ] -> ([], x)
- | x :: ls ->
- let ls, last = pop_last ls in
- (x :: ls, last)
-
- (** Return the n first elements of the list *)
- let prefix (n : int) (ls : 'a list) : 'a list = fst (split_at ls n)
-
- (** Iter and link the iterations.
-
- Iterate over a list, but call a function between every two elements
- (but not before the first element, and not after the last).
- *)
- let iter_link (link : unit -> unit) (f : 'a -> unit) (ls : 'a list) : unit =
- let rec iter ls =
- match ls with
- | [] -> ()
- | [ x ] -> f x
- | x :: y :: ls ->
- f x;
- link ();
- iter (y :: ls)
- in
- iter ls
-
- (** Fold and link the iterations.
-
- Similar to {!iter_link} but for fold left operations.
- *)
- let fold_left_link (link : unit -> unit) (f : 'a -> 'b -> 'a) (init : 'a)
- (ls : 'b list) : 'a =
- let rec fold (acc : 'a) (ls : 'b list) : 'a =
- match ls with
- | [] -> acc
- | [ x ] -> f acc x
- | x :: y :: ls ->
- let acc = f acc x in
- link ();
- fold acc (y :: ls)
- in
- fold init ls
-
- let to_cons_nil (ls : 'a list) : 'a =
- match ls with
- | [ x ] -> x
- | _ -> raise (Failure "The list should have length exactly one")
-
- let pop (ls : 'a list) : 'a * 'a list =
- match ls with
- | x :: ls' -> (x, ls')
- | _ -> raise (Failure "The list should have length > 0")
-end
-
-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
-
-(** Ordered string *)
-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
-
-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
-
- (** "Simple" pretty printing function.
-
- Is useful when we need to customize a bit [show_t], but without using
- something as burdensome as [pp_t].
-
- [to_string (Some indent) m] prints [m] by breaking line after every binding
- and inserting [indent].
- *)
- val to_string : string option -> ('a -> string) -> 'a t -> string
-
- val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
- val show : ('a -> string) -> 'a t -> string
-end
-
-module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
- module Map = Map.Make (Ord)
- 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 =
- let indent, break =
- match indent_opt with Some indent -> (indent, "\n") | None -> ("", " ")
- in
- let sep = "," ^ break in
- let ls =
- Map.fold
- (fun key v ls ->
- (indent ^ Ord.to_string key ^ " -> " ^ a_to_string v) :: ls)
- m []
- in
- match ls with
- | [] -> "{}"
- | _ -> "{" ^ break ^ String.concat sep (List.rev ls) ^ break ^ "}"
-
- let pp (pp_a : Format.formatter -> 'a -> unit) (fmt : Format.formatter)
- (m : 'a t) : unit =
- let pp_string = F.pp_print_string fmt in
- let pp_space () = F.pp_print_space fmt () in
- pp_string "{";
- F.pp_open_box fmt 2;
- Map.iter
- (fun key x ->
- Ord.pp_t fmt key;
- pp_space ();
- pp_string "->";
- pp_space ();
- pp_a fmt x;
- pp_string ",";
- F.pp_print_break fmt 1 0)
- m;
- F.pp_close_box fmt ();
- F.pp_print_break fmt 0 0;
- pp_string "}"
-
- let show show_a m = to_string None show_a m
-end
-
-module type Set = sig
- include Set.S
-
- val add_list : elt list -> t -> t
- val of_list : elt list -> t
-
- (** "Simple" pretty printing function.
-
- Is useful when we need to customize a bit [show_t], but without using
- something as burdensome as [pp_t].
-
- [to_string (Some indent) s] prints [s] by breaking line after every element
- and inserting [indent].
- *)
- val to_string : string option -> t -> string
-
- val pp : Format.formatter -> t -> unit
- val show : t -> string
- val pairwise_distinct : elt list -> bool
-end
-
-module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
- module Set = Set.Make (Ord)
- 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 =
- let indent, break =
- match indent_opt with Some indent -> (indent, "\n") | None -> ("", " ")
- in
- let sep = "," ^ break in
- let ls = Set.fold (fun v ls -> (indent ^ Ord.to_string v) :: ls) m [] in
- match ls with
- | [] -> "{}"
- | _ -> "{" ^ break ^ String.concat sep (List.rev ls) ^ break ^ "}"
-
- let pp (fmt : Format.formatter) (m : t) : unit =
- let pp_string = F.pp_print_string fmt in
- pp_string "{";
- F.pp_open_box fmt 2;
- Set.iter
- (fun x ->
- Ord.pp_t fmt x;
- pp_string ",";
- F.pp_print_break fmt 1 0)
- m;
- F.pp_close_box fmt ();
- F.pp_print_break fmt 0 0;
- pp_string "}"
-
- let show s = to_string None s
-
- let pairwise_distinct ls =
- let s = ref empty in
- let rec check ls =
- match ls with
- | [] -> true
- | x :: ls' ->
- if mem x !s then false
- else (
- s := add x !s;
- check ls')
- in
- check ls
-end
-
-(** A map where the bindings are injective (i.e., if two keys are distinct,
- their bindings are distinct).
-
- This is useful for instance when generating mappings from our internal
- identifiers to names (i.e., strings) when generating code, in order to
- make sure that we don't have potentially dangerous collisions.
- *)
-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
-
-(** See {!InjMap} *)
-module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
- InjMap with type key = Key.t with type elem = Elem.t = struct
- module Map = MakeMap (Key)
- 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 =
- assert (not (Set.mem e m.elems));
- { map = Map.add k e m.map; elems = Set.add e m.elems }
-
- let singleton k e = { map = Map.singleton k e; elems = Set.singleton e }
-
- let remove k m =
- match Map.find_opt k m.map with
- | None -> m
- | 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 *)
- let bindings_to_elems_set (bls : (key * elem) list) : Set.t =
- let elems = List.map snd bls in
- let elems = List.fold_left (fun s e -> Set.add e s) Set.empty elems in
- elems
-
- (** Small helper *)
- let map_to_elems_set (map : elem Map.t) : Set.t =
- bindings_to_elems_set (Map.bindings map)
-
- (** Small helper *)
- let map_to_t (map : elem Map.t) : t =
- let elems = map_to_elems_set map in
- { map; elems }
-
- let filter f m =
- let map = Map.filter f m.map in
- let elems = map_to_elems_set map in
- { map; elems }
-
- let partition f m =
- let map1, map2 = Map.partition f m.map in
- (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 =
- let l, data, r = Map.split k m.map in
- let l = map_to_t l in
- let r = map_to_t r in
- (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 =
- (* Note that it is important to check that we don't add bindings mapping
- * to the same element *)
- match s () with
- | Seq.Nil -> m
- | Seq.Cons ((k, e), s) ->
- let m = add k e m in
- 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
+include Charon.Collections
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 510976f4..52815859 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -1,4 +1,5 @@
open Types
+open Expressions
open Values
open LlbcAst
module V = Values
diff --git a/compiler/Crates.ml b/compiler/Crates.ml
index eb47a8e1..81f42cea 100644
--- a/compiler/Crates.ml
+++ b/compiler/Crates.ml
@@ -1,90 +1 @@
-open Types
-open LlbcAst
-
-type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
-[@@deriving show]
-
-type type_declaration_group = TypeDeclId.id g_declaration_group
-[@@deriving show]
-
-type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
-
-(** Module declaration. Globals cannot be mutually recursive. *)
-type declaration_group =
- | Type of type_declaration_group
- | Fun of fun_declaration_group
- | Global of GlobalDeclId.id
-[@@deriving show]
-
-(** LLBC crate *)
-type llbc_crate = {
- name : string;
- declarations : declaration_group list;
- types : type_decl list;
- functions : fun_decl list;
- globals : global_decl list;
-}
-
-let compute_defs_maps (c : llbc_crate) :
- type_decl TypeDeclId.Map.t
- * fun_decl FunDeclId.Map.t
- * global_decl GlobalDeclId.Map.t =
- let types_map =
- List.fold_left
- (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
- TypeDeclId.Map.empty c.types
- in
- let funs_map =
- List.fold_left
- (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
- FunDeclId.Map.empty c.functions
- in
- let globals_map =
- List.fold_left
- (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
- GlobalDeclId.Map.empty c.globals
- in
- (types_map, funs_map, globals_map)
-
-(** Split a module's declarations between types, functions and globals *)
-let split_declarations (decls : declaration_group list) :
- type_declaration_group list
- * fun_declaration_group list
- * GlobalDeclId.id list =
- let rec split decls =
- match decls with
- | [] -> ([], [], [])
- | d :: decls' -> (
- let types, funs, globals = split decls' in
- match d with
- | Type decl -> (decl :: types, funs, globals)
- | Fun decl -> (types, decl :: funs, globals)
- | Global decl -> (types, funs, decl :: globals))
- in
- split decls
-
-(** Split a module's declarations into three maps from type/fun/global ids to
- declaration groups.
- *)
-let split_declarations_to_group_maps (decls : declaration_group list) :
- type_declaration_group TypeDeclId.Map.t
- * fun_declaration_group FunDeclId.Map.t
- * GlobalDeclId.Set.t =
- let module G (M : Map.S) = struct
- let add_group (map : M.key g_declaration_group M.t)
- (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
- match group with
- | NonRec id -> M.add id group map
- | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
-
- let create_map (groups : M.key g_declaration_group list) :
- M.key g_declaration_group M.t =
- List.fold_left add_group M.empty groups
- end in
- let types, funs, globals = split_declarations decls in
- let module TG = G (TypeDeclId.Map) in
- let types = TG.create_map types in
- let module FG = G (FunDeclId.Map) in
- let funs = FG.create_map funs in
- let globals = GlobalDeclId.Set.of_list globals in
- (types, funs, globals)
+include Charon.Crates
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 31a53cf4..58dd3a0b 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,2 +1 @@
-exception IntegerOverflow of unit
-exception Unimplemented
+include Charon.Errors
diff --git a/compiler/Expressions.ml b/compiler/Expressions.ml
index 1fca7284..06bca9e5 100644
--- a/compiler/Expressions.ml
+++ b/compiler/Expressions.ml
@@ -1,118 +1 @@
-open Types
-open Values
-
-type field_proj_kind =
- | ProjAdt of TypeDeclId.id * VariantId.id option
- | ProjOption of VariantId.id
- (** Option is an assumed type, coming from the standard library *)
- | ProjTuple of int
-[@@deriving show]
-(* arity of the tuple *)
-
-type projection_elem =
- | Deref
- | DerefBox
- | Field of field_proj_kind * FieldId.id
-[@@deriving show]
-
-type projection = projection_elem list [@@deriving show]
-type place = { var_id : VarId.id; projection : projection } [@@deriving show]
-type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show]
-
-type unop =
- | Not
- | Neg
- | Cast of integer_type * integer_type
- (** Cast an integer from a source type to a target type *)
-[@@deriving show, ord]
-
-(** A binary operation
-
- Note that we merge checked binops and unchecked binops: we perform a
- micro-pass on the MIR AST to remove the assertions introduced by rustc,
- and later extract the binops which can fail (addition, substraction, etc.)
- or have preconditions (division, remainder...) to monadic functions.
- *)
-type binop =
- | BitXor
- | BitAnd
- | BitOr
- | Eq
- | Lt
- | Le
- | Ne
- | Ge
- | Gt
- | Div
- | Rem
- | Add
- | Sub
- | Mul
- | Shl
- | Shr
-[@@deriving show, ord]
-
-let all_binops =
- [
- BitXor;
- BitAnd;
- BitOr;
- Eq;
- Lt;
- Le;
- Ne;
- Ge;
- Gt;
- Div;
- Rem;
- Add;
- Sub;
- Mul;
- Shl;
- Shr;
- ]
-
-type operand =
- | Copy of place
- | Move of place
- | Constant of ety * primitive_value
-[@@deriving show]
-
-(** An aggregated ADT.
-
- Note that ADTs are desaggregated at some point in MIR. For instance, if
- we have in Rust:
- {[
- let ls = Cons(hd, tl);
- ]}
-
- In MIR we have (yes, the discriminant update happens *at the end* for some
- reason):
- {[
- (ls as Cons).0 = move hd;
- (ls as Cons).1 = move tl;
- discriminant(ls) = 0; // assuming [Cons] is the variant of index 0
- ]}
-
- Note that in our semantics, we handle both cases (in case of desaggregated
- initialization, [ls] is initialized to [⊥], then this [⊥] is expanded to
- [Cons (⊥, ⊥)] upon the first assignment, at which point we can initialize
- the field 0, etc.).
- *)
-type aggregate_kind =
- | AggregatedTuple
- | AggregatedOption of VariantId.id * ety
- (* TODO: AggregatedOption should be merged with AggregatedAdt *)
- | AggregatedAdt of
- TypeDeclId.id * VariantId.id option * erased_region list * ety list
-[@@deriving show]
-
-(* TODO: move the aggregate kind to operands *)
-type rvalue =
- | Use of operand
- | Ref of place * borrow_kind
- | UnaryOp of unop * operand
- | BinaryOp of binop * operand * operand
- | Discriminant of place
- | Aggregate of aggregate_kind * operand list
-[@@deriving show]
+include Charon.Expressions
diff --git a/compiler/ExpressionsUtils.ml b/compiler/ExpressionsUtils.ml
index c3ccfb15..7dfef101 100644
--- a/compiler/ExpressionsUtils.ml
+++ b/compiler/ExpressionsUtils.ml
@@ -1,10 +1 @@
-module E = Expressions
-
-let unop_can_fail (unop : E.unop) : bool =
- match unop with Neg | Cast _ -> true | Not -> false
-
-let binop_can_fail (binop : E.binop) : bool =
- match binop with
- | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
- | Div | Rem | Add | Sub | Mul -> true
- | Shl | Shr -> raise Errors.Unimplemented
+include Charon.ExpressionsUtils
diff --git a/compiler/Identifiers.ml b/compiler/Identifiers.ml
index b022b18d..513d0eaa 100644
--- a/compiler/Identifiers.ml
+++ b/compiler/Identifiers.ml
@@ -1,139 +1 @@
-module C = Collections
-
-(** Signature for a module describing an identifier.
-
- We often need identifiers (for definitions, variables, etc.) and in
- order to make sure we don't mix them, we use a generative functor
- (see {!IdGen}).
-*)
-module type Id = sig
- type id
-
- (** Id generator - simply a counter *)
- type generator
-
- 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
- contexts...
- Maybe we could have a [fresh] and a [global_fresh]
- 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 *)
-
- val nth_opt : 'a list -> id -> 'a option
-
- (** Update the nth element of the list.
-
- Raises [Invalid_argument] if the identifier is out of range.
- *)
- val update_nth : 'a list -> id -> 'a -> 'a list
-
- val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list
-
- (** Same as {!mapi}, but where the indices start with 1.
-
- TODO: generalize to [map_from_i]
- *)
- val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
-
- 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
-
-(** Generative functor for identifiers.
-
- See {!Id}.
-*)
-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 =
- (* Identifiers should never overflow (because max_int is a really big
- * value - but we really want to make sure we detect overflows if
- * they happen *)
- if x = max_int then raise (Errors.IntegerOverflow ()) else x + 1
-
- let generator_from_incr_id id = incr id
-
- let mk_stateful_generator g =
- let g = ref g in
- let fresh () =
- let id = !g in
- g := incr id;
- id
- in
- (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 =
- (* TODO: check boundaries ? *)
- match js with
- | `Int i -> Ok i
- | _ -> 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 =
- match (vec, id) with
- | [], _ -> raise (Invalid_argument "Out of range")
- | _ :: vec', 0 -> v :: vec'
- | x :: vec', _ -> x :: update_nth vec' (id - 1) v
-
- let mapi = List.mapi
-
- let mapi_from1 f ls =
- let rec aux i ls =
- match ls with [] -> [] | x :: ls' -> f i x :: aux (i + 1) ls'
- in
- aux 1 ls
-
- let iteri = List.iteri
-
- module Ord = struct
- type t = id
-
- let compare = compare
- let to_string = to_string
- let pp_t = pp_id
- let show_t = show_id
- end
-
- module Set = C.MakeSet (Ord)
- module Map = C.MakeMap (Ord)
-end
+include Charon.Identifiers
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index f935734e..308f561c 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -315,7 +315,7 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id)
let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
=
fun ctx ->
- let ret_vid = V.VarId.zero in
+ let ret_vid = E.VarId.zero in
let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
cc cf ctx
@@ -334,7 +334,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
(* List the local variables, but the return variable *)
- let ret_vid = V.VarId.zero in
+ let ret_vid = E.VarId.zero in
let rec list_locals env =
match env with
| [] -> raise (Failure "Inconsistent environment")
@@ -345,12 +345,12 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
if var.index <> ret_vid then var.index :: locals else locals
| C.Frame :: _ -> []
in
- let locals : V.VarId.id list = list_locals ctx.env in
+ let locals : E.VarId.id list = list_locals ctx.env in
(* Debug *)
log#ldebug
(lazy
("ctx_pop_frame: locals in which to drop the outer loans: ["
- ^ String.concat "," (List.map V.VarId.to_string locals)
+ ^ String.concat "," (List.map E.VarId.to_string locals)
^ "]"));
(* Move the return value out of the return variable *)
@@ -447,7 +447,7 @@ let eval_box_new_concrete (config : C.config)
let box_v = mk_typed_value box_ty box_v in
(* Move this value to the return variable *)
- let dest = mk_place_from_var_id V.VarId.zero in
+ let dest = mk_place_from_var_id E.VarId.zero in
let cf_assign = assign_to_place config box_v dest in
(* Continue *)
@@ -496,7 +496,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
raise (Failure "Unreachable")
| Ok borrowed_value ->
(* Move and continue *)
- let destp = mk_place_from_var_id V.VarId.zero in
+ let destp = mk_place_from_var_id E.VarId.zero in
assign_to_place config borrowed_value destp cf
in
@@ -595,7 +595,7 @@ let eval_non_local_function_call_concrete (config : C.config)
let cc = push_frame in
(* Create and push the return variable *)
- let ret_vid = V.VarId.zero in
+ let ret_vid = E.VarId.zero in
let ret_ty =
get_non_local_function_return_type fid region_params type_params
in
@@ -604,7 +604,7 @@ let eval_non_local_function_call_concrete (config : C.config)
(* Create and push the input variables *)
let input_vars =
- V.VarId.mapi_from1
+ E.VarId.mapi_from1
(fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v))
args_vl
in
@@ -922,7 +922,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
(* Compose and apply *)
comp cc cf_eval_st cf ctx
-and eval_global (config : C.config) (dest : V.VarId.id)
+and eval_global (config : C.config) (dest : E.VarId.id)
(gid : LA.GlobalDeclId.id) : st_cm_fun =
fun cf ctx ->
let global = C.ctx_lookup_global_decl ctx gid in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index e6033e9e..578ee5ef 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -30,12 +30,12 @@ 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 =
sv0.V.sv_id = sv1.V.sv_id
-let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
+let mk_var (index : E.VarId.id) (name : string option) (var_ty : T.ety) : A.var
=
{ A.index; name; var_ty }
(** Small helper - TODO: move *)
-let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
+let mk_place_from_var_id (var_id : E.VarId.id) : E.place =
{ var_id; projection = [] }
(** Create a fresh symbolic value *)
@@ -124,7 +124,7 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
(** Generic borrow content: concrete or abstract *)
type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
-type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id option
+type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of E.VarId.id option
(** Utility exception *)
exception FoundBorrowContent of V.borrow_content
diff --git a/compiler/LlbcAst.ml b/compiler/LlbcAst.ml
index 1b08f1ea..f4d26e18 100644
--- a/compiler/LlbcAst.ml
+++ b/compiler/LlbcAst.ml
@@ -1,46 +1,6 @@
-open Names
open Types
open Values
-open Expressions
-open Identifiers
-module FunDeclId = IdGen ()
-module GlobalDeclId = IdGen ()
-open Meta
-
-(** A variable, as used in a function definition *)
-type var = {
- index : VarId.id; (** Unique variable identifier *)
- name : string option;
- var_ty : ety;
- (** The variable type - erased type, because variables are not used
- ** in function signatures: they are only used to declare the list of
- ** variables manipulated by a function body *)
-}
-[@@deriving show]
-
-type assumed_fun_id =
- | Replace (** [core::mem::replace] *)
- | BoxNew
- | BoxDeref (** [core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref] *)
- | BoxDerefMut
- (** [core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut] *)
- | BoxFree
- | VecNew
- | VecPush
- | VecInsert
- | VecLen
- | VecIndex (** [core::ops::index::Index::index<alloc::vec::Vec<T>, usize>] *)
- | VecIndexMut
- (** [core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>] *)
-[@@deriving show, ord]
-
-type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
-[@@deriving show, ord]
-
-type global_assignment = { dst : VarId.id; global : GlobalDeclId.id }
-[@@deriving show]
-
-type assertion = { cond : operand; expected : bool } [@@deriving show]
+include Charon.LlbcAst
type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
[@@deriving show]
@@ -48,17 +8,6 @@ type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
[@@deriving show]
-(** A function signature, as used when declaring functions *)
-type fun_sig = {
- region_params : region_var list;
- num_early_bound_regions : int;
- regions_hierarchy : region_var_groups;
- type_params : type_var list;
- inputs : sty list;
- output : sty;
-}
-[@@deriving show]
-
(** A function signature, after instantiation *)
type inst_fun_sig = {
regions_hierarchy : abs_region_groups;
@@ -66,140 +15,3 @@ type inst_fun_sig = {
output : rty;
}
[@@deriving show]
-
-type call = {
- func : fun_id;
- region_args : erased_region list;
- type_args : ety list;
- args : operand list;
- dest : place;
-}
-[@@deriving show]
-
-(** Ancestor for [typed_value] iter visitor *)
-class ['self] iter_statement_base =
- object (_self : 'self)
- inherit [_] VisitorsRuntime.iter
-
- method visit_global_assignment : 'env -> global_assignment -> unit =
- fun _ _ -> ()
-
- method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
- method visit_place : 'env -> place -> unit = fun _ _ -> ()
- method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
- method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
- method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
- method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
- method visit_call : 'env -> call -> unit = fun _ _ -> ()
- method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
- method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
- end
-
-(** Ancestor for [typed_value] map visitor *)
-class ['self] map_statement_base =
- object (_self : 'self)
- inherit [_] VisitorsRuntime.map
-
- method visit_global_assignment
- : 'env -> global_assignment -> global_assignment =
- fun _ x -> x
-
- method visit_meta : 'env -> meta -> meta = fun _ x -> x
- method visit_place : 'env -> place -> place = fun _ x -> x
- method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
- method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
- method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
- method visit_operand : 'env -> operand -> operand = fun _ x -> x
- method visit_call : 'env -> call -> call = fun _ x -> x
-
- method visit_integer_type : 'env -> integer_type -> integer_type =
- fun _ x -> x
-
- method visit_scalar_value : 'env -> scalar_value -> scalar_value =
- fun _ x -> x
- end
-
-type statement = {
- meta : meta; (** The statement meta-data *)
- content : raw_statement; (** The statement itself *)
-}
-
-and raw_statement =
- | Assign of place * rvalue
- | AssignGlobal of global_assignment
- | FakeRead of place
- | SetDiscriminant of place * VariantId.id
- | Drop of place
- | Assert of assertion
- | Call of call
- | Panic
- | Return
- | Break of int
- (** Break to (outer) loop. The [int] identifies the loop to break to:
- * 0: break to the first outer loop (the current loop)
- * 1: break to the second outer loop
- * ...
- *)
- | Continue of int
- (** Continue to (outer) loop. The loop identifier works
- the same way as for {!Break} *)
- | Nop
- | Sequence of statement * statement
- | Switch of operand * switch_targets
- | Loop of statement
-
-and switch_targets =
- | If of statement * statement (** Gives the "if" and "else" blocks *)
- | SwitchInt of integer_type * (scalar_value list * statement) list * statement
- (** The targets for a switch over an integer are:
- - the list [(matched values, statement to execute)]
- We need a list for the matched values in case we do something like this:
- [switch n { 0 | 1 => ..., _ => ... }]
- - the "otherwise" statement
- Also note that we precise the type of the integer (uint32, int64, etc.)
- which we switch on. *)
-[@@deriving
- show,
- visitors
- {
- name = "iter_statement";
- variety = "iter";
- ancestors = [ "iter_statement_base" ];
- nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
- concrete = true;
- },
- visitors
- {
- name = "map_statement";
- variety = "map";
- ancestors = [ "map_statement_base" ];
- nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
- concrete = true;
- }]
-
-type fun_body = {
- meta : meta;
- arg_count : int;
- locals : var list;
- body : statement;
-}
-[@@deriving show]
-
-type fun_decl = {
- def_id : FunDeclId.id;
- meta : meta;
- name : fun_name;
- signature : fun_sig;
- body : fun_body option;
- is_global_decl_body : bool;
-}
-[@@deriving show]
-
-type global_decl = {
- def_id : GlobalDeclId.id;
- meta : meta;
- body_id : FunDeclId.id;
- name : global_name;
- ty : ety;
-}
-[@@deriving show]
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 46711d0a..1111c297 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -1,25 +1,5 @@
open LlbcAst
-open Utils
-module T = Types
-
-(** Check if a {!type:LlbcAst.statement} contains loops *)
-let statement_has_loops (st : statement) : bool =
- let obj =
- object
- inherit [_] iter_statement
- method! visit_Loop _ _ = raise Found
- end
- in
- try
- obj#visit_statement () st;
- false
- with Found -> true
-
-(** Check if a {!type:LlbcAst.fun_decl} contains loops *)
-let fun_decl_has_loops (fd : fun_decl) : bool =
- match fd.body with
- | Some body -> statement_has_loops body.body
- | None -> false
+include Charon.LlbcAstUtils
let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
fun_sig =
@@ -32,42 +12,3 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
match fun_id with
| Regular id -> (FunDeclId.Map.find id fun_decls).name
| Assumed aid -> Assumed.get_assumed_name aid
-
-(** Small utility: list the transitive parents of a region var group.
- We don't do that in an efficient manner, but it doesn't matter.
-
- TODO: rename to "list_ancestors_..."
-
- This list *doesn't* include the current region.
- *)
-let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
- T.RegionGroupId.Set.t =
- let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
- let parents =
- List.fold_left
- (fun s gid ->
- (* Compute the parents *)
- let parents = list_parent_region_groups sg gid in
- (* Parents U current region *)
- let parents = T.RegionGroupId.Set.add gid parents in
- (* Make the union with the accumulator *)
- T.RegionGroupId.Set.union s parents)
- T.RegionGroupId.Set.empty rg.parents
- in
- parents
-
-(** Small utility: same as {!list_parent_region_groups}, but returns an ordered list. *)
-let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id)
- : T.RegionGroupId.id list =
- let pset = list_parent_region_groups sg gid in
- let parents =
- List.filter
- (fun (rg : T.region_var_group) -> T.RegionGroupId.Set.mem rg.id pset)
- sg.regions_hierarchy
- in
- let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in
- parents
-
-let fun_body_get_input_vars (fbody : fun_body) : var list =
- let locals = List.tl fbody.locals in
- Collections.List.prefix fbody.arg_count locals
diff --git a/compiler/LlbcOfJson.ml b/compiler/LlbcOfJson.ml
index ad4cd5e4..dd8692a8 100644
--- a/compiler/LlbcOfJson.ml
+++ b/compiler/LlbcOfJson.ml
@@ -1,917 +1 @@
-(** Functions to load LLBC ASTs from json.
-
- Initially, we used [ppx_derive_yojson] to automate this.
- However, [ppx_derive_yojson] expects formatting to be slightly
- different from what [serde_rs] generates (because it uses [Yojson.Safe.t]
- and not [Yojson.Basic.t]).
-
- TODO: we should check all that the integer values are in the proper range
- *)
-
-open Yojson.Basic
-open Names
-open OfJsonBasic
-open Identifiers
-open Meta
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module S = Scalars
-module E = Expressions
-module A = LlbcAst
-module TU = TypesUtils
-module AU = LlbcAstUtils
-module LocalFileId = IdGen ()
-module VirtualFileId = IdGen ()
-
-(** The default logger *)
-let log = Logging.llbc_of_json_logger
-
-(** A file identifier *)
-type file_id = LocalId of LocalFileId.id | VirtualId of VirtualFileId.id
-[@@deriving show, ord]
-
-module OrderedIdToFile : Collections.OrderedType with type t = file_id = struct
- type t = file_id
-
- let compare fid0 fid1 = compare_file_id fid0 fid1
-
- let to_string id =
- match id with
- | LocalId id -> "Local " ^ LocalFileId.to_string id
- | VirtualId id -> "Virtual " ^ VirtualFileId.to_string id
-
- let pp_t fmt x = Format.pp_print_string fmt (to_string x)
- let show_t x = to_string x
-end
-
-module IdToFile = Collections.MakeMap (OrderedIdToFile)
-
-type id_to_file_map = file_name IdToFile.t
-
-let file_id_of_json (js : json) : (file_id, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("LocalId", id) ] ->
- let* id = LocalFileId.id_of_json id in
- Ok (LocalId id)
- | `Assoc [ ("VirtualId", id) ] ->
- let* id = VirtualFileId.id_of_json id in
- Ok (VirtualId id)
- | _ -> Error "")
-
-let file_name_of_json (js : json) : (file_name, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Virtual", name) ] ->
- let* name = string_of_json name in
- Ok (Virtual name)
- | `Assoc [ ("Local", name) ] ->
- let* name = string_of_json name in
- Ok (Local name)
- | _ -> Error "")
-
-(** Deserialize a map from file id to file name.
-
- In the serialized LLBC, the files in the loc spans are refered to by their
- ids, in order to save space. In a functional language like OCaml this is
- not necessary: we thus replace the file ids by the file name themselves in
- the AST.
- The "id to file" map is thus only used in the deserialization process.
- *)
-let id_to_file_of_json (js : json) : (id_to_file_map, string) result =
- combine_error_msgs js __FUNCTION__
- ((* The map is stored as a list of pairs (key, value): we deserialize
- * this list then convert it to a map *)
- let* key_values =
- list_of_json (pair_of_json file_id_of_json file_name_of_json) js
- in
- Ok (IdToFile.of_list key_values))
-
-let loc_of_json (js : json) : (loc, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("line", line); ("col", col) ] ->
- let* line = int_of_json line in
- let* col = int_of_json col in
- Ok { line; col }
- | _ -> Error "")
-
-let span_of_json (id_to_file : id_to_file_map) (js : json) :
- (span, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("file_id", file_id); ("beg", beg_loc); ("end", end_loc) ] ->
- let* file_id = file_id_of_json file_id in
- let file = IdToFile.find file_id id_to_file in
- let* beg_loc = loc_of_json beg_loc in
- let* end_loc = loc_of_json end_loc in
- Ok { file; beg_loc; end_loc }
- | _ -> Error "")
-
-let meta_of_json (id_to_file : id_to_file_map) (js : json) :
- (meta, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("span", span); ("generated_from_span", generated_from_span) ] ->
- let* span = span_of_json id_to_file span in
- let* generated_from_span =
- option_of_json (span_of_json id_to_file) generated_from_span
- in
- Ok { span; generated_from_span }
- | _ -> Error "")
-
-let path_elem_of_json (js : json) : (path_elem, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Ident", name) ] ->
- let* name = string_of_json name in
- Ok (Ident name)
- | `Assoc [ ("Disambiguator", d) ] ->
- let* d = Disambiguator.id_of_json d in
- Ok (Disambiguator d)
- | _ -> Error "")
-
-let name_of_json (js : json) : (name, string) result =
- combine_error_msgs js __FUNCTION__ (list_of_json path_elem_of_json js)
-
-let fun_name_of_json (js : json) : (fun_name, string) result =
- combine_error_msgs js __FUNCTION__ (name_of_json js)
-
-let type_var_of_json (js : json) : (T.type_var, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("index", index); ("name", name) ] ->
- let* index = T.TypeVarId.id_of_json index in
- let* name = string_of_json name in
- Ok { T.index; name }
- | _ -> Error "")
-
-let region_var_of_json (js : json) : (T.region_var, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("index", index); ("name", name) ] ->
- let* index = T.RegionVarId.id_of_json index in
- let* name = string_option_of_json name in
- Ok { T.index; name }
- | _ -> Error "")
-
-let region_of_json (js : json) : (T.RegionVarId.id T.region, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `String "Static" -> Ok T.Static
- | `Assoc [ ("Var", rid) ] ->
- let* rid = T.RegionVarId.id_of_json rid in
- Ok (T.Var rid)
- | _ -> Error "")
-
-let erased_region_of_json (js : json) : (T.erased_region, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with `String "Erased" -> Ok T.Erased | _ -> Error "")
-
-let integer_type_of_json (js : json) : (T.integer_type, string) result =
- match js with
- | `String "Isize" -> Ok T.Isize
- | `String "I8" -> Ok T.I8
- | `String "I16" -> Ok T.I16
- | `String "I32" -> Ok T.I32
- | `String "I64" -> Ok T.I64
- | `String "I128" -> Ok T.I128
- | `String "Usize" -> Ok T.Usize
- | `String "U8" -> Ok T.U8
- | `String "U16" -> Ok T.U16
- | `String "U32" -> Ok T.U32
- | `String "U64" -> Ok T.U64
- | `String "U128" -> Ok T.U128
- | _ -> Error ("integer_type_of_json failed on: " ^ show js)
-
-let ref_kind_of_json (js : json) : (T.ref_kind, string) result =
- match js with
- | `String "Mut" -> Ok T.Mut
- | `String "Shared" -> Ok T.Shared
- | _ -> Error ("ref_kind_of_json failed on: " ^ show js)
-
-let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `String "Box" -> Ok T.Box
- | `String "Vec" -> Ok T.Vec
- | `String "Option" -> Ok T.Option
- | _ -> Error "")
-
-let type_id_of_json (js : json) : (T.type_id, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Adt", id) ] ->
- let* id = T.TypeDeclId.id_of_json id in
- Ok (T.AdtId id)
- | `String "Tuple" -> Ok T.Tuple
- | `Assoc [ ("Assumed", aty) ] ->
- let* aty = assumed_ty_of_json aty in
- Ok (T.Assumed aty)
- | _ -> Error "")
-
-let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
- ('r T.ty, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Adt", `List [ id; regions; types ]) ] ->
- let* id = type_id_of_json id in
- let* regions = list_of_json r_of_json regions in
- let* types = list_of_json (ty_of_json r_of_json) types in
- (* Sanity check *)
- (match id with T.Tuple -> assert (List.length regions = 0) | _ -> ());
- Ok (T.Adt (id, regions, types))
- | `Assoc [ ("TypeVar", `List [ id ]) ] ->
- let* id = T.TypeVarId.id_of_json id in
- Ok (T.TypeVar id)
- | `String "Bool" -> Ok Bool
- | `String "Char" -> Ok Char
- | `String "`Never" -> Ok Never
- | `Assoc [ ("Integer", `List [ int_ty ]) ] ->
- let* int_ty = integer_type_of_json int_ty in
- Ok (T.Integer int_ty)
- | `String "Str" -> Ok Str
- | `Assoc [ ("Array", `List [ ty ]) ] ->
- let* ty = ty_of_json r_of_json ty in
- Ok (T.Array ty)
- | `Assoc [ ("Slice", `List [ ty ]) ] ->
- let* ty = ty_of_json r_of_json ty in
- Ok (T.Slice ty)
- | `Assoc [ ("Ref", `List [ region; ty; ref_kind ]) ] ->
- let* region = r_of_json region in
- let* ty = ty_of_json r_of_json ty in
- let* ref_kind = ref_kind_of_json ref_kind in
- Ok (T.Ref (region, ty, ref_kind))
- | _ -> Error "")
-
-let sty_of_json (js : json) : (T.sty, string) result =
- combine_error_msgs js __FUNCTION__ (ty_of_json region_of_json js)
-
-let ety_of_json (js : json) : (T.ety, string) result =
- combine_error_msgs js __FUNCTION__ (ty_of_json erased_region_of_json js)
-
-let field_of_json (id_to_file : id_to_file_map) (js : json) :
- (T.field, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("meta", meta); ("name", name); ("ty", ty) ] ->
- let* meta = meta_of_json id_to_file meta in
- let* name = option_of_json string_of_json name in
- let* ty = sty_of_json ty in
- Ok { T.meta; field_name = name; field_ty = ty }
- | _ -> Error "")
-
-let variant_of_json (id_to_file : id_to_file_map) (js : json) :
- (T.variant, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("meta", meta); ("name", name); ("fields", fields) ] ->
- let* meta = meta_of_json id_to_file meta in
- let* name = string_of_json name in
- let* fields = list_of_json (field_of_json id_to_file) fields in
- Ok { T.meta; variant_name = name; fields }
- | _ -> Error "")
-
-let type_decl_kind_of_json (id_to_file : id_to_file_map) (js : json) :
- (T.type_decl_kind, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Struct", fields) ] ->
- let* fields = list_of_json (field_of_json id_to_file) fields in
- Ok (T.Struct fields)
- | `Assoc [ ("Enum", variants) ] ->
- let* variants = list_of_json (variant_of_json id_to_file) variants in
- Ok (T.Enum variants)
- | `String "Opaque" -> Ok T.Opaque
- | _ -> Error "")
-
-let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
- let* id = T.RegionGroupId.id_of_json id in
- let* regions = list_of_json T.RegionVarId.id_of_json regions in
- let* parents = list_of_json T.RegionGroupId.id_of_json parents in
- Ok { T.id; regions; parents }
- | _ -> Error "")
-
-let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result
- =
- combine_error_msgs js __FUNCTION__ (list_of_json region_var_group_of_json js)
-
-let type_decl_of_json (id_to_file : id_to_file_map) (js : json) :
- (T.type_decl, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("def_id", def_id);
- ("meta", meta);
- ("name", name);
- ("region_params", region_params);
- ("type_params", type_params);
- ("regions_hierarchy", regions_hierarchy);
- ("kind", kind);
- ] ->
- let* def_id = T.TypeDeclId.id_of_json def_id in
- let* meta = meta_of_json id_to_file meta in
- let* name = name_of_json name in
- let* region_params = list_of_json region_var_of_json region_params in
- let* type_params = list_of_json type_var_of_json type_params in
- let* kind = type_decl_kind_of_json id_to_file kind in
- let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
- Ok
- {
- T.def_id;
- meta;
- name;
- region_params;
- type_params;
- kind;
- regions_hierarchy;
- }
- | _ -> Error "")
-
-let var_of_json (js : json) : (A.var, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] ->
- let* index = V.VarId.id_of_json index in
- let* name = string_option_of_json name in
- let* var_ty = ety_of_json ty in
- Ok { A.index; name; var_ty }
- | _ -> Error "")
-
-let big_int_of_json (js : json) : (V.big_int, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Int i -> Ok (Z.of_int i)
- | `String is -> Ok (Z.of_string is)
- | _ -> Error "")
-
-(** Deserialize a {!V.scalar_value} from JSON and **check the ranges**.
-
- Note that in practice we also check that the values are in range
- in the interpreter functions. Still, it doesn't cost much to be
- a bit conservative.
- *)
-let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
- let res =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Isize", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = Isize }
- | `Assoc [ ("I8", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = I8 }
- | `Assoc [ ("I16", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = I16 }
- | `Assoc [ ("I32", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = I32 }
- | `Assoc [ ("I64", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = I64 }
- | `Assoc [ ("I128", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = I128 }
- | `Assoc [ ("Usize", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = Usize }
- | `Assoc [ ("U8", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = U8 }
- | `Assoc [ ("U16", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = U16 }
- | `Assoc [ ("U32", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = U32 }
- | `Assoc [ ("U64", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = U64 }
- | `Assoc [ ("U128", `List [ bi ]) ] ->
- let* bi = big_int_of_json bi in
- Ok { PV.value = bi; int_ty = U128 }
- | _ -> Error "")
- in
- match res with
- | Error _ -> res
- | Ok sv ->
- if not (S.check_scalar_value_in_range sv) then (
- log#serror ("Scalar value not in range: " ^ PV.show_scalar_value sv);
- raise
- (Failure ("Scalar value not in range: " ^ PV.show_scalar_value sv)));
- res
-
-let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] ->
- let* def_id = T.TypeDeclId.id_of_json def_id in
- let* opt_variant_id =
- option_of_json T.VariantId.id_of_json opt_variant_id
- in
- Ok (E.ProjAdt (def_id, opt_variant_id))
- | `Assoc [ ("ProjTuple", i) ] ->
- let* i = int_of_json i in
- Ok (E.ProjTuple i)
- | `Assoc [ ("ProjOption", variant_id) ] ->
- let* variant_id = T.VariantId.id_of_json variant_id in
- Ok (E.ProjOption variant_id)
- | _ -> Error "")
-
-let projection_elem_of_json (js : json) : (E.projection_elem, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `String "Deref" -> Ok E.Deref
- | `String "DerefBox" -> Ok E.DerefBox
- | `Assoc [ ("Field", `List [ proj_kind; field_id ]) ] ->
- let* proj_kind = field_proj_kind_of_json proj_kind in
- let* field_id = T.FieldId.id_of_json field_id in
- Ok (E.Field (proj_kind, field_id))
- | _ -> Error ("projection_elem_of_json failed on:" ^ show js))
-
-let projection_of_json (js : json) : (E.projection, string) result =
- combine_error_msgs js __FUNCTION__ (list_of_json projection_elem_of_json js)
-
-let place_of_json (js : json) : (E.place, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("var_id", var_id); ("projection", projection) ] ->
- let* var_id = V.VarId.id_of_json var_id in
- let* projection = projection_of_json projection in
- Ok { E.var_id; projection }
- | _ -> Error "")
-
-let borrow_kind_of_json (js : json) : (E.borrow_kind, string) result =
- match js with
- | `String "Shared" -> Ok E.Shared
- | `String "Mut" -> Ok E.Mut
- | `String "TwoPhaseMut" -> Ok E.TwoPhaseMut
- | _ -> Error ("borrow_kind_of_json failed on:" ^ show js)
-
-let unop_of_json (js : json) : (E.unop, string) result =
- match js with
- | `String "Not" -> Ok E.Not
- | `String "Neg" -> Ok E.Neg
- | `Assoc [ ("Cast", `List [ src_ty; tgt_ty ]) ] ->
- let* src_ty = integer_type_of_json src_ty in
- let* tgt_ty = integer_type_of_json tgt_ty in
- Ok (E.Cast (src_ty, tgt_ty))
- | _ -> Error ("unop_of_json failed on:" ^ show js)
-
-let binop_of_json (js : json) : (E.binop, string) result =
- match js with
- | `String "BitXor" -> Ok E.BitXor
- | `String "BitAnd" -> Ok E.BitAnd
- | `String "BitOr" -> Ok E.BitOr
- | `String "Eq" -> Ok E.Eq
- | `String "Lt" -> Ok E.Lt
- | `String "Le" -> Ok E.Le
- | `String "Ne" -> Ok E.Ne
- | `String "Ge" -> Ok E.Ge
- | `String "Gt" -> Ok E.Gt
- | `String "Div" -> Ok E.Div
- | `String "Rem" -> Ok E.Rem
- | `String "Add" -> Ok E.Add
- | `String "Sub" -> Ok E.Sub
- | `String "Mul" -> Ok E.Mul
- | `String "Shl" -> Ok E.Shl
- | `String "Shr" -> Ok E.Shr
- | _ -> Error ("binop_of_json failed on:" ^ show js)
-
-let primitive_value_of_json (js : json) : (V.primitive_value, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Scalar", scalar_value) ] ->
- let* scalar_value = scalar_value_of_json scalar_value in
- Ok (PV.Scalar scalar_value)
- | `Assoc [ ("Bool", v) ] ->
- let* v = bool_of_json v in
- Ok (PV.Bool v)
- | `Assoc [ ("Char", v) ] ->
- let* v = char_of_json v in
- Ok (PV.Char v)
- | `Assoc [ ("String", v) ] ->
- let* v = string_of_json v in
- Ok (PV.String v)
- | _ -> Error "")
-
-let operand_of_json (js : json) : (E.operand, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Copy", place) ] ->
- let* place = place_of_json place in
- Ok (E.Copy place)
- | `Assoc [ ("Move", place) ] ->
- let* place = place_of_json place in
- Ok (E.Move place)
- | `Assoc [ ("Const", `List [ ty; cv ]) ] ->
- let* ty = ety_of_json ty in
- let* cv = primitive_value_of_json cv in
- Ok (E.Constant (ty, cv))
- | _ -> Error "")
-
-let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `String "AggregatedTuple" -> Ok E.AggregatedTuple
- | `Assoc [ ("AggregatedOption", `List [ variant_id; ty ]) ] ->
- let* variant_id = T.VariantId.id_of_json variant_id in
- let* ty = ety_of_json ty in
- Ok (E.AggregatedOption (variant_id, ty))
- | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ]
- ->
- let* id = T.TypeDeclId.id_of_json id in
- let* opt_variant_id =
- option_of_json T.VariantId.id_of_json opt_variant_id
- in
- let* regions = list_of_json erased_region_of_json regions in
- let* tys = list_of_json ety_of_json tys in
- Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys))
- | _ -> Error "")
-
-let rvalue_of_json (js : json) : (E.rvalue, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Use", op) ] ->
- let* op = operand_of_json op in
- Ok (E.Use op)
- | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] ->
- let* place = place_of_json place in
- let* borrow_kind = borrow_kind_of_json borrow_kind in
- Ok (E.Ref (place, borrow_kind))
- | `Assoc [ ("UnaryOp", `List [ unop; op ]) ] ->
- let* unop = unop_of_json unop in
- let* op = operand_of_json op in
- Ok (E.UnaryOp (unop, op))
- | `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] ->
- let* binop = binop_of_json binop in
- let* op1 = operand_of_json op1 in
- let* op2 = operand_of_json op2 in
- Ok (E.BinaryOp (binop, op1, op2))
- | `Assoc [ ("Discriminant", place) ] ->
- let* place = place_of_json place in
- Ok (E.Discriminant place)
- | `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] ->
- let* aggregate_kind = aggregate_kind_of_json aggregate_kind in
- let* ops = list_of_json operand_of_json ops in
- Ok (E.Aggregate (aggregate_kind, ops))
- | _ -> Error "")
-
-let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result =
- match js with
- | `String "Replace" -> Ok A.Replace
- | `String "BoxNew" -> Ok A.BoxNew
- | `String "BoxDeref" -> Ok A.BoxDeref
- | `String "BoxDerefMut" -> Ok A.BoxDerefMut
- | `String "BoxFree" -> Ok A.BoxFree
- | `String "VecNew" -> Ok A.VecNew
- | `String "VecPush" -> Ok A.VecPush
- | `String "VecInsert" -> Ok A.VecInsert
- | `String "VecLen" -> Ok A.VecLen
- | `String "VecIndex" -> Ok A.VecIndex
- | `String "VecIndexMut" -> Ok A.VecIndexMut
- | _ -> Error ("assumed_fun_id_of_json failed on:" ^ show js)
-
-let fun_id_of_json (js : json) : (A.fun_id, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Regular", id) ] ->
- let* id = A.FunDeclId.id_of_json id in
- Ok (A.Regular id)
- | `Assoc [ ("Assumed", fid) ] ->
- let* fid = assumed_fun_id_of_json fid in
- Ok (A.Assumed fid)
- | _ -> Error "")
-
-let assertion_of_json (js : json) : (A.assertion, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("cond", cond); ("expected", expected) ] ->
- let* cond = operand_of_json cond in
- let* expected = bool_of_json expected in
- Ok { A.cond; expected }
- | _ -> Error "")
-
-let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("region_params", region_params);
- ("num_early_bound_regions", num_early_bound_regions);
- ("regions_hierarchy", regions_hierarchy);
- ("type_params", type_params);
- ("inputs", inputs);
- ("output", output);
- ] ->
- let* region_params = list_of_json region_var_of_json region_params in
- let* num_early_bound_regions = int_of_json num_early_bound_regions in
- let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
- let* type_params = list_of_json type_var_of_json type_params in
- let* inputs = list_of_json sty_of_json inputs in
- let* output = sty_of_json output in
- Ok
- {
- A.region_params;
- num_early_bound_regions;
- regions_hierarchy;
- type_params;
- inputs;
- output;
- }
- | _ -> Error "")
-
-let call_of_json (js : json) : (A.call, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("func", func);
- ("region_args", region_args);
- ("type_args", type_args);
- ("args", args);
- ("dest", dest);
- ] ->
- let* func = fun_id_of_json func in
- let* region_args = list_of_json erased_region_of_json region_args in
- let* type_args = list_of_json ety_of_json type_args in
- let* args = list_of_json operand_of_json args in
- let* dest = place_of_json dest in
- Ok { A.func; region_args; type_args; args; dest }
- | _ -> Error "")
-
-let rec statement_of_json (id_to_file : id_to_file_map) (js : json) :
- (A.statement, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("meta", meta); ("content", content) ] ->
- let* meta = meta_of_json id_to_file meta in
- let* content = raw_statement_of_json id_to_file content in
- Ok { A.meta; content }
- | _ -> Error "")
-
-and raw_statement_of_json (id_to_file : id_to_file_map) (js : json) :
- (A.raw_statement, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
- let* place = place_of_json place in
- let* rvalue = rvalue_of_json rvalue in
- Ok (A.Assign (place, rvalue))
- | `Assoc [ ("AssignGlobal", `List [ dst; global ]) ] ->
- let* dst = V.VarId.id_of_json dst in
- let* global = A.GlobalDeclId.id_of_json global in
- Ok (A.AssignGlobal { dst; global })
- | `Assoc [ ("FakeRead", place) ] ->
- let* place = place_of_json place in
- Ok (A.FakeRead place)
- | `Assoc [ ("SetDiscriminant", `List [ place; variant_id ]) ] ->
- let* place = place_of_json place in
- let* variant_id = T.VariantId.id_of_json variant_id in
- Ok (A.SetDiscriminant (place, variant_id))
- | `Assoc [ ("Drop", place) ] ->
- let* place = place_of_json place in
- Ok (A.Drop place)
- | `Assoc [ ("Assert", assertion) ] ->
- let* assertion = assertion_of_json assertion in
- Ok (A.Assert assertion)
- | `Assoc [ ("Call", call) ] ->
- let* call = call_of_json call in
- Ok (A.Call call)
- | `String "Panic" -> Ok A.Panic
- | `String "Return" -> Ok A.Return
- | `Assoc [ ("Break", i) ] ->
- let* i = int_of_json i in
- Ok (A.Break i)
- | `Assoc [ ("Continue", i) ] ->
- let* i = int_of_json i in
- Ok (A.Continue i)
- | `String "Nop" -> Ok A.Nop
- | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json id_to_file st1 in
- let* st2 = statement_of_json id_to_file st2 in
- Ok (A.Sequence (st1, st2))
- | `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
- let* op = operand_of_json op in
- let* tgt = switch_targets_of_json id_to_file tgt in
- Ok (A.Switch (op, tgt))
- | `Assoc [ ("Loop", st) ] ->
- let* st = statement_of_json id_to_file st in
- Ok (A.Loop st)
- | _ -> Error "")
-
-and switch_targets_of_json (id_to_file : id_to_file_map) (js : json) :
- (A.switch_targets, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("If", `List [ st1; st2 ]) ] ->
- let* st1 = statement_of_json id_to_file st1 in
- let* st2 = statement_of_json id_to_file st2 in
- Ok (A.If (st1, st2))
- | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
- let* int_ty = integer_type_of_json int_ty in
- let* tgts =
- list_of_json
- (pair_of_json
- (list_of_json scalar_value_of_json)
- (statement_of_json id_to_file))
- tgts
- in
- let* otherwise = statement_of_json id_to_file otherwise in
- Ok (A.SwitchInt (int_ty, tgts, otherwise))
- | _ -> Error "")
-
-let fun_body_of_json (id_to_file : id_to_file_map) (js : json) :
- (A.fun_body, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("meta", meta);
- ("arg_count", arg_count);
- ("locals", locals);
- ("body", body);
- ] ->
- let* meta = meta_of_json id_to_file meta in
- let* arg_count = int_of_json arg_count in
- let* locals = list_of_json var_of_json locals in
- let* body = statement_of_json id_to_file body in
- Ok { A.meta; arg_count; locals; body }
- | _ -> Error "")
-
-let fun_decl_of_json (id_to_file : id_to_file_map) (js : json) :
- (A.fun_decl, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("def_id", def_id);
- ("meta", meta);
- ("name", name);
- ("signature", signature);
- ("body", body);
- ] ->
- let* def_id = A.FunDeclId.id_of_json def_id in
- let* meta = meta_of_json id_to_file meta in
- let* name = fun_name_of_json name in
- let* signature = fun_sig_of_json signature in
- let* body = option_of_json (fun_body_of_json id_to_file) body in
- Ok
- { A.def_id; meta; name; signature; body; is_global_decl_body = false }
- | _ -> Error "")
-
-(* Strict type for the number of function declarations (see {!global_to_fun_id} below) *)
-type global_id_converter = { fun_count : int } [@@deriving show]
-
-(** Converts a global id to its corresponding function id.
- To do so, it adds the global id to the number of function declarations :
- We have the bijection [global_fun_id <=> global_id + fun_id_count].
-*)
-let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) :
- A.FunDeclId.id =
- A.FunDeclId.of_int (A.GlobalDeclId.to_int gid + conv.fun_count)
-
-(* Converts a global declaration to a function declaration.
- *)
-let global_decl_of_json (id_to_file : id_to_file_map) (js : json)
- (gid_conv : global_id_converter) :
- (A.global_decl * A.fun_decl, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("def_id", def_id);
- ("meta", meta);
- ("name", name);
- ("ty", ty);
- ("body", body);
- ] ->
- let* global_id = A.GlobalDeclId.id_of_json def_id in
- let fun_id = global_to_fun_id gid_conv global_id in
- let* meta = meta_of_json id_to_file meta in
- let* name = fun_name_of_json name in
- let* ty = ety_of_json ty in
- let* body = option_of_json (fun_body_of_json id_to_file) body in
- let signature : A.fun_sig =
- {
- region_params = [];
- num_early_bound_regions = 0;
- regions_hierarchy = [];
- type_params = [];
- inputs = [];
- output = TU.ety_no_regions_to_sty ty;
- }
- in
- Ok
- ( { A.def_id = global_id; meta; body_id = fun_id; name; ty },
- {
- A.def_id = fun_id;
- meta;
- name;
- signature;
- body;
- is_global_decl_body = true;
- } )
- | _ -> Error "")
-
-let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
- (js : json) : ('id Crates.g_declaration_group, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("NonRec", `List [ id ]) ] ->
- let* id = id_of_json id in
- Ok (Crates.NonRec id)
- | `Assoc [ ("Rec", `List [ ids ]) ] ->
- let* ids = list_of_json id_of_json ids in
- Ok (Crates.Rec ids)
- | _ -> Error "")
-
-let type_declaration_group_of_json (js : json) :
- (Crates.type_declaration_group, string) result =
- combine_error_msgs js __FUNCTION__
- (g_declaration_group_of_json T.TypeDeclId.id_of_json js)
-
-let fun_declaration_group_of_json (js : json) :
- (Crates.fun_declaration_group, string) result =
- combine_error_msgs js __FUNCTION__
- (g_declaration_group_of_json A.FunDeclId.id_of_json js)
-
-let global_declaration_group_of_json (js : json) :
- (A.GlobalDeclId.id, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("NonRec", `List [ id ]) ] ->
- let* id = A.GlobalDeclId.id_of_json id in
- Ok id
- | `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals"
- | _ -> Error "")
-
-let declaration_group_of_json (js : json) :
- (Crates.declaration_group, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc [ ("Type", `List [ decl ]) ] ->
- let* decl = type_declaration_group_of_json decl in
- Ok (Crates.Type decl)
- | `Assoc [ ("Fun", `List [ decl ]) ] ->
- let* decl = fun_declaration_group_of_json decl in
- Ok (Crates.Fun decl)
- | `Assoc [ ("Global", `List [ decl ]) ] ->
- let* id = global_declaration_group_of_json decl in
- Ok (Crates.Global id)
- | _ -> Error "")
-
-let length_of_json_list (js : json) : (int, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `List jsl -> Ok (List.length jsl)
- | _ -> Error ("not a list: " ^ show js))
-
-let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
- combine_error_msgs js __FUNCTION__
- (match js with
- | `Assoc
- [
- ("name", name);
- ("id_to_file", id_to_file);
- ("declarations", declarations);
- ("types", types);
- ("functions", functions);
- ("globals", globals);
- ] ->
- (* We first deserialize the declaration groups (which simply contain ids)
- * and all the declarations *butù* the globals *)
- let* name = string_of_json name in
- let* id_to_file = id_to_file_of_json id_to_file in
- let* declarations =
- list_of_json declaration_group_of_json declarations
- in
- let* types = list_of_json (type_decl_of_json id_to_file) types in
- let* functions = list_of_json (fun_decl_of_json id_to_file) functions in
- (* When deserializing the globals, we split the global declarations
- * between the globals themselves and their bodies, which are simply
- * functions with no arguments. We add the global bodies to the list
- * of function declarations: the (fresh) ids we use for those bodies
- * are simply given by: [num_functions + global_id] *)
- let gid_conv = { fun_count = List.length functions } in
- let* globals =
- list_of_json
- (fun js -> global_decl_of_json id_to_file js gid_conv)
- globals
- in
- let globals, global_bodies = List.split globals in
- Ok
- {
- Crates.name;
- declarations;
- types;
- functions = functions @ global_bodies;
- globals;
- }
- | _ -> Error "")
+include Charon.LlbcOfJson
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index e83f25f8..7b95f41d 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -1,17 +1,8 @@
-module H = Easy_logging.Handlers
-module L = Easy_logging.Logging
-
-let _ = L.make_logger "MainLogger" Debug [ Cli Debug ]
-
-(** The main logger *)
-let main_log = L.get_logger "MainLogger"
+include Charon.Logging
(** Below, we create subgloggers for various submodules, so that we can precisely
toggle logging on/off, depending on which information we need *)
-(** Logger for LlbcOfJson *)
-let llbc_of_json_logger = L.get_logger "MainLogger.LlbcOfJson"
-
(** Logger for PrePasses *)
let pre_passes_log = L.get_logger "MainLogger.PrePasses"
@@ -50,130 +41,3 @@ let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
(** Logger for Invariants *)
let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
-
-(** Terminal colors - TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-type color =
- | Default
- | Black
- | Red
- | Green
- | Yellow
- | Blue
- | Magenta
- | Cyan
- | Gray
- | White
- | LRed
- | LGreen
- | LYellow
- | LBlue
- | LMagenta
- | LCyan
- | LGray
-
-(** Terminal styles - TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-type format = Bold | Underline | Invert | Fg of color | Bg of color
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-let to_fg_code c =
- match c with
- | Default -> 39
- | Black -> 30
- | Red -> 31
- | Green -> 32
- | Yellow -> 33
- | Blue -> 34
- | Magenta -> 35
- | Cyan -> 36
- | Gray -> 90
- | White -> 97
- | LRed -> 91
- | LGreen -> 92
- | LYellow -> 93
- | LBlue -> 94
- | LMagenta -> 95
- | LCyan -> 96
- | LGray -> 37
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-let to_bg_code c =
- match c with
- | Default -> 49
- | Black -> 40
- | Red -> 41
- | Green -> 42
- | Yellow -> 43
- | Blue -> 44
- | Magenta -> 45
- | Cyan -> 46
- | Gray -> 100
- | White -> 107
- | LRed -> 101
- | LGreen -> 102
- | LYellow -> 103
- | LBlue -> 104
- | LMagenta -> 105
- | LCyan -> 106
- | LGray -> 47
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-let style_to_codes s =
- match s with
- | Bold -> (1, 21)
- | Underline -> (4, 24)
- | Invert -> (7, 27)
- | Fg c -> (to_fg_code c, to_fg_code Default)
- | Bg c -> (to_bg_code c, to_bg_code Default)
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly)
- I made a minor modifications, though. *)
-let level_to_color (lvl : L.level) =
- match lvl with
- | L.Flash -> LMagenta
- | Error -> LRed
- | Warning -> LYellow
- | Info -> LGreen
- | Trace -> Cyan
- | Debug -> LBlue
- | NoLevel -> Default
-
-(** [format styles str] formats [str] to the given [styles] -
- TODO: comes from {{: http://ocamlverse.net/content/documentation_guidelines.html}[easy_logging]}
- (did not manage to reuse the module directly)
-*)
-let rec format styles str =
- match styles with
- | (_ as s) :: styles' ->
- let set, reset = style_to_codes s in
- Printf.sprintf "\027[%dm%s\027[%dm" set (format styles' str) reset
- | [] -> str
-
-(** TODO: comes from {{: http://ocamlverse.net/content/documentation_guidelines.html}[easy_logging]}
- (did not manage to reuse the module directly) *)
-let format_tags (tags : string list) =
- match tags with
- | [] -> ""
- | _ ->
- let elems_str = String.concat " | " tags in
- "[" ^ elems_str ^ "] "
-
-(* Change the formatters *)
-let main_logger_handler =
- (* TODO: comes from easy_logging *)
- let formatter (item : L.log_item) : string =
- let item_level_fmt =
- format [ Fg (level_to_color item.level) ] (L.show_level item.level)
- and item_msg_fmt =
- match item.level with
- | Flash -> format [ Fg Black; Bg LMagenta ] item.msg
- | _ -> item.msg
- in
-
- Format.pp_set_max_indent Format.str_formatter 200;
- Format.sprintf "@[[%-15s] %s%s@]" item_level_fmt (format_tags item.tags)
- item_msg_fmt
- in
- (* There should be exactly one handler *)
- let handlers = main_log#get_handlers in
- List.iter (fun h -> H.set_formatter h formatter) handlers;
- match handlers with [ handler ] -> handler | _ -> failwith "Unexpected"
diff --git a/compiler/Meta.ml b/compiler/Meta.ml
index f0e4ca04..b8a3d1e0 100644
--- a/compiler/Meta.ml
+++ b/compiler/Meta.ml
@@ -1,44 +1 @@
-(** Meta data like code spans *)
-
-(** A line location *)
-type loc = {
- line : int; (** The (1-based) line number. *)
- col : int; (** The (0-based) column offset. *)
-}
-[@@deriving show]
-
-type file_name =
- | Virtual of string (** A remapped path (namely paths into stdlib) *)
- | Local of string
- (** A local path (a file coming from the current crate for instance) *)
-[@@deriving show]
-
-(** Span data *)
-type span = { file : file_name; beg_loc : loc; end_loc : loc } [@@deriving show]
-
-type meta = {
- span : span;
- (** The source code span.
-
- If this meta information is for a statement/terminator coming from a macro
- expansion/inlining/etc., this span is (in case of macros) for the macro
- before expansion (i.e., the location the code where the user wrote the call
- to the macro).
-
- Ex:
- {[
- // Below, we consider the spans for the statements inside `test`
-
- // the statement we consider, which gets inlined in `test`
- VV
- macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
-
- fn test() {
- macro!(); // <-- `span` refers to this location
- }
- ]}
- *)
- generated_from_span : span option;
- (** Where the code actually comes from, in case of macro expansion/inlining/etc. *)
-}
-[@@deriving show]
+include Charon.Meta
diff --git a/compiler/Names.ml b/compiler/Names.ml
index a27db161..97dbc180 100644
--- a/compiler/Names.ml
+++ b/compiler/Names.ml
@@ -1,80 +1 @@
-open Identifiers
-module Disambiguator = IdGen ()
-
-(** See the comments for [Name] *)
-type path_elem = Ident of string | Disambiguator of Disambiguator.id
-[@@deriving show, ord]
-
-(** A name such as: [std::collections::vector] (which would be represented as
- [[Ident "std"; Ident "collections"; Ident "vector"]])
-
-
- A name really is a list of strings. However, we sometimes need to
- introduce unique indices to disambiguate. This mostly happens because
- of "impl" blocks in Rust:
- {[
- impl<T> List<T> {
- ...
- }
- ]}
-
- A type in Rust can have several "impl" blocks, and those blocks can
- contain items with similar names. For this reason, we need to disambiguate
- them with unique indices. Rustc calls those "disambiguators". In rustc, this
- gives names like this:
- - [betree_main::betree::NodeIdCounter{impl#0}::new]
- - note that impl blocks can be nested, and macros sometimes generate
- weird names (which require disambiguation):
- [betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}]
-
- Finally, the paths used by rustc are a lot more precise and explicit than
- those we expose in LLBC: for instance, every identifier belongs to a specific
- namespace (value namespace, type namespace, etc.), and is coupled with a
- disambiguator.
-
- On our side, we want to stay high-level and simple: we use string identifiers
- as much as possible, insert disambiguators only when necessary (whenever
- we find an "impl" block, typically) and check that the disambiguator is useless
- in the other situations (i.e., the disambiguator is always equal to 0).
-
- Moreover, the items are uniquely disambiguated by their (integer) ids
- ([TypeDeclId.id], etc.), and when extracting the code we have to deal with
- name clashes anyway. Still, we might want to be more precise in the future.
-
- Also note that the first path element in the name is always the crate name.
- *)
-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 *)
-let filter_disambiguators_zero (n : name) : name =
- let pred (pe : path_elem) : bool =
- match pe with Ident _ -> true | Disambiguator d -> d <> Disambiguator.zero
- in
- List.filter pred n
-
-(** Filter the disambiguators in a name *)
-let filter_disambiguators (n : name) : name =
- let pred (pe : path_elem) : bool =
- match pe with Ident _ -> true | Disambiguator _ -> false
- in
- List.filter pred n
-
-let as_ident (pe : path_elem) : string =
- match pe with
- | Ident s -> s
- | Disambiguator _ -> raise (Failure "Improper variant")
-
-let path_elem_to_string (pe : path_elem) : string =
- match pe with
- | Ident s -> s
- | Disambiguator d -> "{" ^ Disambiguator.to_string d ^ "}"
-
-let name_to_string (name : name) : string =
- String.concat "::" (List.map path_elem_to_string name)
+include Charon.Names
diff --git a/compiler/OfJsonBasic.ml b/compiler/OfJsonBasic.ml
deleted file mode 100644
index 07daf03d..00000000
--- a/compiler/OfJsonBasic.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-(** This module defines various basic utilities for json deserialization.
-
- *)
-
-open Yojson.Basic
-
-type json = t
-
-let ( let* ) o f = match o with Error e -> Error e | Ok x -> f x
-
-let combine_error_msgs js msg res : ('a, string) result =
- match res with
- | Ok x -> Ok x
- | Error e -> Error ("[" ^ msg ^ "]" ^ " failed on: " ^ show js ^ "\n\n" ^ e)
-
-let bool_of_json (js : json) : (bool, string) result =
- match js with
- | `Bool b -> Ok b
- | _ -> Error ("bool_of_json: not a bool: " ^ show js)
-
-let int_of_json (js : json) : (int, string) result =
- match js with
- | `Int i -> Ok i
- | _ -> Error ("int_of_json: not an int: " ^ show js)
-
-let char_of_json (js : json) : (char, string) result =
- match js with
- | `String c ->
- if String.length c = 1 then Ok c.[0]
- else Error ("char_of_json: stricly more than one character in: " ^ show js)
- | _ -> Error ("char_of_json: not a char: " ^ show js)
-
-let rec of_json_list (a_of_json : json -> ('a, string) result) (jsl : json list)
- : ('a list, string) result =
- match jsl with
- | [] -> Ok []
- | x :: jsl' ->
- let* x = a_of_json x in
- let* jsl' = of_json_list a_of_json jsl' in
- Ok (x :: jsl')
-
-let pair_of_json (a_of_json : json -> ('a, string) result)
- (b_of_json : json -> ('b, string) result) (js : json) :
- ('a * 'b, string) result =
- match js with
- | `List [ a; b ] ->
- let* a = a_of_json a in
- let* b = b_of_json b in
- Ok (a, b)
- | _ -> Error ("pair_of_json failed on: " ^ show js)
-
-let list_of_json (a_of_json : json -> ('a, string) result) (js : json) :
- ('a list, string) result =
- combine_error_msgs js "list_of_json"
- (match js with
- | `List jsl -> of_json_list a_of_json jsl
- | _ -> Error ("not a list: " ^ show js))
-
-let string_of_json (js : json) : (string, string) result =
- match js with
- | `String str -> Ok str
- | _ -> Error ("string_of_json: not a string: " ^ show js)
-
-let option_of_json (a_of_json : json -> ('a, string) result) (js : json) :
- ('a option, string) result =
- combine_error_msgs js "option_of_json"
- (match js with
- | `Null -> Ok None
- | _ ->
- let* x = a_of_json js in
- Ok (Some x))
-
-let string_option_of_json (js : json) : (string option, string) result =
- combine_error_msgs js "string_option_of_json"
- (option_of_json string_of_json js)
diff --git a/compiler/PrimitiveValues.ml b/compiler/PrimitiveValues.ml
index 0bf37256..0eacca9e 100644
--- a/compiler/PrimitiveValues.ml
+++ b/compiler/PrimitiveValues.ml
@@ -1,41 +1 @@
-(** The primitive values. *)
-
-open Types
-
-(** We use big integers to store the integer values (this way we don't have
- to think about the bounds, nor architecture issues - Rust allows to
- manipulate 128-bit integers for instance).
- *)
-type big_int = Z.t
-
-let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
- match json with
- | `Int i -> Ok (Z.of_int i)
- | `Intlit is -> Ok (Z.of_string is)
- | _ -> Error "not an integer or an integer literal"
-
-let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
-
-let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
- Format.pp_print_string fmt (Z.to_string bi)
-
-let show_big_int (bi : big_int) : string = Z.to_string bi
-
-(** A scalar value
-
- Note that we use unbounded integers everywhere.
- We then harcode the boundaries for the different types.
- *)
-type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
-
-(** A primitive value.
-
- Can be used by operands (in which case it represents a constant) or by
- the interpreter to represent a concrete, primitive value.
- *)
-type primitive_value =
- | Scalar of scalar_value
- | Bool of bool
- | Char of char
- | String of string
-[@@deriving show]
+include Charon.PrimitiveValues
diff --git a/compiler/Print.ml b/compiler/Print.ml
index cc25c780..3f15bd32 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,226 +1,8 @@
-open Names
-module T = Types
-module TU = TypesUtils
+include Charon.Print
module V = Values
module VU = ValuesUtils
-module E = Expressions
-module A = LlbcAst
module C = Contexts
-let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
- match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
-
-let name_to_string (name : name) : string = Names.name_to_string name
-let fun_name_to_string (name : fun_name) : string = name_to_string name
-let global_name_to_string (name : global_name) : string = name_to_string name
-
-(** Pretty-printing for types *)
-module Types = struct
- let type_var_to_string (tv : T.type_var) : string = tv.name
-
- let region_var_to_string (rv : T.region_var) : string =
- match rv.name with
- | Some name -> name
- | None -> T.RegionVarId.to_string rv.index
-
- let region_var_id_to_string (rid : T.RegionVarId.id) : string =
- "rv@" ^ T.RegionVarId.to_string rid
-
- let region_id_to_string (rid : T.RegionId.id) : string =
- "r@" ^ T.RegionId.to_string rid
-
- let region_to_string (rid_to_string : 'rid -> string) (r : 'rid T.region) :
- string =
- match r with Static -> "'static" | Var rid -> rid_to_string rid
-
- let erased_region_to_string (_ : T.erased_region) : string = "'_"
-
- let ref_kind_to_string (rk : T.ref_kind) : string =
- match rk with Mut -> "Mut" | Shared -> "Shared"
-
- let assumed_ty_to_string (_ : T.assumed_ty) : string = "Box"
-
- type 'r type_formatter = {
- r_to_string : 'r -> string;
- type_var_id_to_string : T.TypeVarId.id -> string;
- type_decl_id_to_string : T.TypeDeclId.id -> string;
- }
-
- type stype_formatter = T.RegionVarId.id T.region type_formatter
- type rtype_formatter = T.RegionId.id T.region type_formatter
- type etype_formatter = T.erased_region type_formatter
-
- let integer_type_to_string = function
- | T.Isize -> "isize"
- | T.I8 -> "i8"
- | T.I16 -> "i16"
- | T.I32 -> "i32"
- | T.I64 -> "i64"
- | T.I128 -> "i128"
- | T.Usize -> "usize"
- | T.U8 -> "u8"
- | T.U16 -> "u16"
- | T.U32 -> "u32"
- | T.U64 -> "u64"
- | T.U128 -> "u128"
-
- let type_id_to_string (fmt : 'r type_formatter) (id : T.type_id) : string =
- match id with
- | T.AdtId id -> fmt.type_decl_id_to_string id
- | T.Tuple -> ""
- | T.Assumed aty -> (
- match aty with
- | Box -> "alloc::boxed::Box"
- | Vec -> "alloc::vec::Vec"
- | Option -> "core::option::Option")
-
- let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r T.ty) : string =
- match ty with
- | T.Adt (id, regions, tys) ->
- let is_tuple = match id with T.Tuple -> true | _ -> false in
- let params = params_to_string fmt is_tuple regions tys in
- type_id_to_string fmt id ^ params
- | T.TypeVar tv -> fmt.type_var_id_to_string tv
- | T.Bool -> "bool"
- | T.Char -> "char"
- | T.Never -> "⊥"
- | T.Integer int_ty -> integer_type_to_string int_ty
- | T.Str -> "str"
- | T.Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]"
- | T.Slice sty -> "[" ^ ty_to_string fmt sty ^ "]"
- | T.Ref (r, rty, ref_kind) -> (
- match ref_kind with
- | T.Mut ->
- "&" ^ fmt.r_to_string r ^ " mut (" ^ ty_to_string fmt rty ^ ")"
- | T.Shared ->
- "&" ^ fmt.r_to_string r ^ " (" ^ ty_to_string fmt rty ^ ")")
-
- and params_to_string (fmt : 'r type_formatter) (is_tuple : bool)
- (regions : 'r list) (types : 'r T.ty list) : string =
- let regions = List.map fmt.r_to_string regions in
- let types = List.map (ty_to_string fmt) types in
- let params = String.concat ", " (List.append regions types) in
- if is_tuple then "(" ^ params ^ ")"
- else if List.length regions + List.length types > 0 then "<" ^ params ^ ">"
- else ""
-
- let sty_to_string (fmt : stype_formatter) (ty : T.sty) : string =
- ty_to_string fmt ty
-
- let rty_to_string (fmt : rtype_formatter) (ty : T.rty) : string =
- ty_to_string fmt ty
-
- let ety_to_string (fmt : etype_formatter) (ty : T.ety) : string =
- ty_to_string fmt ty
-
- let field_to_string fmt (f : T.field) : string =
- match f.field_name with
- | Some field_name -> field_name ^ " : " ^ ty_to_string fmt f.field_ty
- | None -> ty_to_string fmt f.field_ty
-
- let variant_to_string fmt (v : T.variant) : string =
- v.variant_name ^ "("
- ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
- ^ ")"
-
- let type_decl_to_string (type_decl_id_to_string : T.TypeDeclId.id -> string)
- (def : T.type_decl) : string =
- let regions = def.region_params in
- let types = def.type_params in
- let rid_to_string rid =
- match List.find_opt (fun rv -> rv.T.index = rid) regions with
- | Some rv -> region_var_to_string rv
- | None -> failwith "Unreachable"
- in
- let r_to_string = region_to_string rid_to_string in
- let type_var_id_to_string id =
- match List.find_opt (fun tv -> tv.T.index = id) types with
- | Some tv -> type_var_to_string tv
- | None -> failwith "Unreachable"
- in
- let fmt = { r_to_string; type_var_id_to_string; type_decl_id_to_string } in
- let name = name_to_string def.name in
- let params =
- if List.length regions + List.length types > 0 then
- let regions = List.map region_var_to_string regions in
- let types = List.map type_var_to_string types in
- let params = String.concat ", " (List.append regions types) in
- "<" ^ params ^ ">"
- else ""
- in
- match def.kind with
- | T.Struct fields ->
- if List.length fields > 0 then
- let fields =
- String.concat ","
- (List.map (fun f -> "\n " ^ field_to_string fmt f) fields)
- in
- "struct " ^ name ^ params ^ "{" ^ fields ^ "}"
- else "struct " ^ name ^ params ^ "{}"
- | T.Enum variants ->
- let variants =
- List.map (fun v -> "| " ^ variant_to_string fmt v) variants
- in
- let variants = String.concat "\n" variants in
- "enum " ^ name ^ params ^ " =\n" ^ variants
- | T.Opaque -> "opaque type " ^ name ^ params
-
- let type_ctx_to_adt_variant_to_string_fun
- (ctx : T.type_decl T.TypeDeclId.Map.t) :
- T.TypeDeclId.id -> T.VariantId.id -> string =
- fun def_id variant_id ->
- let def = T.TypeDeclId.Map.find def_id ctx in
- match def.kind with
- | Struct _ | Opaque -> failwith "Unreachable"
- | Enum variants ->
- let variant = T.VariantId.nth variants variant_id in
- name_to_string def.name ^ "::" ^ variant.variant_name
-
- let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) :
- T.TypeDeclId.id -> T.VariantId.id option -> string list option =
- fun def_id opt_variant_id ->
- let def = T.TypeDeclId.Map.find def_id ctx in
- let fields = TU.type_decl_get_fields def opt_variant_id in
- (* There are two cases: either all the fields have names, or none of them
- * has names *)
- let has_names =
- List.exists (fun f -> Option.is_some f.T.field_name) fields
- in
- if has_names then
- let fields = List.map (fun f -> Option.get f.T.field_name) fields in
- Some fields
- else None
-
- let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t)
- :
- T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option
- =
- fun def_id opt_variant_id field_id ->
- let def = T.TypeDeclId.Map.find def_id ctx in
- let fields = TU.type_decl_get_fields def opt_variant_id in
- let field = T.FieldId.nth fields field_id in
- field.T.field_name
-end
-
-module PT = Types (* local module *)
-
-(** Pretty-printing for primitive values *)
-module PrimitiveValues = struct
- let big_int_to_string (bi : V.big_int) : string = Z.to_string bi
-
- let scalar_value_to_string (sv : V.scalar_value) : string =
- big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty
-
- let primitive_value_to_string (cv : V.primitive_value) : string =
- match cv with
- | Scalar sv -> scalar_value_to_string sv
- | Bool b -> Bool.to_string b
- | Char c -> String.make 1 c
- | String s -> s
-end
-
-module PPV = PrimitiveValues (* local module *)
-
(** Pretty-printing for values *)
module Values = struct
type value_formatter = {
@@ -229,7 +11,7 @@ module Values = struct
type_var_id_to_string : T.TypeVarId.id -> string;
type_decl_id_to_string : T.TypeDeclId.id -> string;
adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
- var_id_to_string : V.VarId.id -> string;
+ var_id_to_string : E.VarId.id -> string;
adt_field_names :
T.TypeDeclId.id -> T.VariantId.id option -> string list option;
}
@@ -255,8 +37,8 @@ module Values = struct
PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
}
- let var_id_to_string (id : V.VarId.id) : string =
- "var@" ^ V.VarId.to_string id
+ let var_id_to_string (id : E.VarId.id) : string =
+ "var@" ^ E.VarId.to_string id
let symbolic_value_id_to_string (id : V.SymbolicValueId.id) : string =
"s@" ^ V.SymbolicValueId.to_string id
@@ -522,413 +304,6 @@ end
module PV = Values (* local module *)
-(** Pretty-printing for LLBC AST (generic functions) *)
-module LlbcAst = struct
- let var_to_string (var : A.var) : string =
- match var.name with
- | None -> V.VarId.to_string var.index
- | Some name -> name
-
- type ast_formatter = {
- rvar_to_string : T.RegionVarId.id -> string;
- r_to_string : T.RegionId.id -> string;
- type_var_id_to_string : T.TypeVarId.id -> string;
- type_decl_id_to_string : T.TypeDeclId.id -> string;
- adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
- adt_field_to_string :
- T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option;
- var_id_to_string : V.VarId.id -> string;
- adt_field_names :
- T.TypeDeclId.id -> T.VariantId.id option -> string list option;
- fun_decl_id_to_string : A.FunDeclId.id -> string;
- global_decl_id_to_string : A.GlobalDeclId.id -> string;
- }
-
- let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
- {
- PT.r_to_string = PT.erased_region_to_string;
- PT.type_var_id_to_string = fmt.type_var_id_to_string;
- PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
- }
-
- let ast_to_rtype_formatter (fmt : ast_formatter) : PT.rtype_formatter =
- {
- PT.r_to_string = PT.region_to_string fmt.r_to_string;
- PT.type_var_id_to_string = fmt.type_var_id_to_string;
- PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
- }
-
- let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter =
- {
- PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
- PT.type_var_id_to_string = fmt.type_var_id_to_string;
- PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
- }
-
- 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) :
- ast_formatter =
- let rvar_to_string r =
- let rvar = T.RegionVarId.nth fdef.signature.region_params r in
- PT.region_var_to_string rvar
- in
- let r_to_string r = PT.region_id_to_string r in
-
- let type_var_id_to_string vid =
- let var = T.TypeVarId.nth fdef.signature.type_params vid in
- PT.type_var_to_string var
- in
- let type_decl_id_to_string def_id =
- let def = T.TypeDeclId.Map.find def_id type_decls in
- name_to_string def.name
- in
- let adt_variant_to_string =
- PT.type_ctx_to_adt_variant_to_string_fun type_decls
- in
- let var_id_to_string vid =
- let var = V.VarId.nth (Option.get fdef.body).locals vid in
- var_to_string var
- in
- let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_decls in
- let adt_field_to_string =
- PT.type_ctx_to_adt_field_to_string_fun type_decls
- in
- let fun_decl_id_to_string def_id =
- let def = A.FunDeclId.Map.find def_id fun_decls in
- fun_name_to_string def.name
- in
- let global_decl_id_to_string def_id =
- let def = A.GlobalDeclId.Map.find def_id global_decls in
- global_name_to_string def.name
- in
- {
- rvar_to_string;
- r_to_string;
- type_var_id_to_string;
- type_decl_id_to_string;
- adt_variant_to_string;
- var_id_to_string;
- adt_field_names;
- adt_field_to_string;
- fun_decl_id_to_string;
- global_decl_id_to_string;
- }
-
- let rec projection_to_string (fmt : ast_formatter) (inside : string)
- (p : E.projection) : string =
- match p with
- | [] -> inside
- | pe :: p' -> (
- let s = projection_to_string fmt inside p' in
- match pe with
- | E.Deref -> "*(" ^ s ^ ")"
- | E.DerefBox -> "deref_box(" ^ s ^ ")"
- | E.Field (E.ProjOption variant_id, fid) ->
- assert (variant_id = T.option_some_id);
- assert (fid = T.FieldId.zero);
- "(" ^ s ^ " as Option::Some)." ^ T.FieldId.to_string fid
- | E.Field (E.ProjTuple _, fid) ->
- "(" ^ s ^ ")." ^ T.FieldId.to_string fid
- | E.Field (E.ProjAdt (adt_id, opt_variant_id), fid) -> (
- let field_name =
- match fmt.adt_field_to_string adt_id opt_variant_id fid with
- | Some field_name -> field_name
- | None -> T.FieldId.to_string fid
- in
- match opt_variant_id with
- | None -> "(" ^ s ^ ")." ^ field_name
- | Some variant_id ->
- let variant_name =
- fmt.adt_variant_to_string adt_id variant_id
- in
- "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
-
- let place_to_string (fmt : ast_formatter) (p : E.place) : string =
- let var = fmt.var_id_to_string p.E.var_id in
- projection_to_string fmt var p.E.projection
-
- let unop_to_string (unop : E.unop) : string =
- match unop with
- | E.Not -> "¬"
- | E.Neg -> "-"
- | E.Cast (src, tgt) ->
- "cast<"
- ^ PT.integer_type_to_string src
- ^ ","
- ^ PT.integer_type_to_string tgt
- ^ ">"
-
- let binop_to_string (binop : E.binop) : string =
- match binop with
- | E.BitXor -> "^"
- | E.BitAnd -> "&"
- | E.BitOr -> "|"
- | E.Eq -> "=="
- | E.Lt -> "<"
- | E.Le -> "<="
- | E.Ne -> "!="
- | E.Ge -> ">="
- | E.Gt -> ">"
- | E.Div -> "/"
- | E.Rem -> "%"
- | E.Add -> "+"
- | E.Sub -> "-"
- | E.Mul -> "*"
- | E.Shl -> "<<"
- | E.Shr -> ">>"
-
- let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
- match op with
- | E.Copy p -> "copy " ^ place_to_string fmt p
- | E.Move p -> "move " ^ place_to_string fmt p
- | E.Constant (ty, cv) ->
- "("
- ^ PPV.primitive_value_to_string cv
- ^ " : "
- ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
- ^ ")"
-
- let rvalue_to_string (fmt : ast_formatter) (rv : E.rvalue) : string =
- match rv with
- | E.Use op -> operand_to_string fmt op
- | E.Ref (p, bk) -> (
- let p = place_to_string fmt p in
- match bk with
- | E.Shared -> "&" ^ p
- | E.Mut -> "&mut " ^ p
- | E.TwoPhaseMut -> "&two-phase " ^ p)
- | E.UnaryOp (unop, op) ->
- unop_to_string unop ^ " " ^ operand_to_string fmt op
- | E.BinaryOp (binop, op1, op2) ->
- operand_to_string fmt op1 ^ " " ^ binop_to_string binop ^ " "
- ^ operand_to_string fmt op2
- | E.Discriminant p -> "discriminant(" ^ place_to_string fmt p ^ ")"
- | E.Aggregate (akind, ops) -> (
- let ops = List.map (operand_to_string fmt) ops in
- match akind with
- | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
- | E.AggregatedOption (variant_id, _ty) ->
- if variant_id == T.option_none_id then (
- assert (ops == []);
- "@Option::None")
- else if variant_id == T.option_some_id then (
- assert (List.length ops == 1);
- let op = List.hd ops in
- "@Option::Some(" ^ op ^ ")")
- else raise (Failure "Unreachable")
- | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) ->
- let adt_name = fmt.type_decl_id_to_string def_id in
- let variant_name =
- match opt_variant_id with
- | None -> adt_name
- | Some variant_id ->
- adt_name ^ "::" ^ fmt.adt_variant_to_string def_id variant_id
- in
- let fields =
- match fmt.adt_field_names def_id opt_variant_id with
- | None -> "(" ^ String.concat ", " ops ^ ")"
- | Some field_names ->
- let fields = List.combine field_names ops in
- let fields =
- List.map
- (fun (field, value) -> field ^ " = " ^ value ^ ";")
- fields
- in
- let fields = String.concat " " fields in
- "{ " ^ fields ^ " }"
- in
- variant_name ^ " " ^ fields)
-
- let rec statement_to_string (fmt : ast_formatter) (indent : string)
- (indent_incr : string) (st : A.statement) : string =
- raw_statement_to_string fmt indent indent_incr st.content
-
- and raw_statement_to_string (fmt : ast_formatter) (indent : string)
- (indent_incr : string) (st : A.raw_statement) : string =
- match st with
- | 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
- | 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 *)
- indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", "
- ^ T.VariantId.to_string variant_id
- ^ ")"
- | A.Drop p -> indent ^ "drop " ^ place_to_string fmt p
- | A.Assert a ->
- let cond = operand_to_string fmt a.A.cond in
- if a.A.expected then indent ^ "assert(" ^ cond ^ ")"
- else indent ^ "assert(¬" ^ cond ^ ")"
- | A.Call call ->
- let ty_fmt = ast_to_etype_formatter fmt in
- let t_params =
- if List.length call.A.type_args > 0 then
- "<"
- ^ String.concat ","
- (List.map (PT.ty_to_string ty_fmt) call.A.type_args)
- ^ ">"
- else ""
- in
- let args = List.map (operand_to_string fmt) call.A.args in
- let args = "(" ^ String.concat ", " args ^ ")" in
- let name_args =
- match call.A.func with
- | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ t_params
- | A.Assumed fid -> (
- match fid with
- | A.Replace -> "core::mem::replace" ^ t_params
- | A.BoxNew -> "alloc::boxed::Box" ^ t_params ^ "::new"
- | A.BoxDeref ->
- "core::ops::deref::Deref<Box" ^ t_params ^ ">::deref"
- | A.BoxDerefMut ->
- "core::ops::deref::DerefMut" ^ t_params ^ "::deref_mut"
- | A.BoxFree -> "alloc::alloc::box_free" ^ t_params
- | A.VecNew -> "alloc::vec::Vec" ^ t_params ^ "::new"
- | A.VecPush -> "alloc::vec::Vec" ^ t_params ^ "::push"
- | A.VecInsert -> "alloc::vec::Vec" ^ t_params ^ "::insert"
- | A.VecLen -> "alloc::vec::Vec" ^ t_params ^ "::len"
- | A.VecIndex ->
- "core::ops::index::Index<alloc::vec::Vec" ^ t_params
- ^ ">::index"
- | A.VecIndexMut ->
- "core::ops::index::IndexMut<alloc::vec::Vec" ^ t_params
- ^ ">::index_mut")
- in
- let dest = place_to_string fmt call.A.dest in
- indent ^ dest ^ " := move " ^ name_args ^ args
- | A.Panic -> indent ^ "panic"
- | A.Return -> indent ^ "return"
- | A.Break i -> indent ^ "break " ^ string_of_int i
- | A.Continue i -> indent ^ "continue " ^ string_of_int i
- | A.Nop -> indent ^ "nop"
- | A.Sequence (st1, st2) ->
- statement_to_string fmt indent indent_incr st1
- ^ ";\n"
- ^ statement_to_string fmt indent indent_incr st2
- | A.Switch (op, tgts) -> (
- let op = operand_to_string fmt op in
- match tgts with
- | A.If (true_st, false_st) ->
- let inner_indent = indent ^ indent_incr in
- let inner_to_string =
- statement_to_string fmt inner_indent indent_incr
- in
- let true_st = inner_to_string true_st in
- let false_st = inner_to_string false_st in
- indent ^ "if (" ^ op ^ ") {\n" ^ true_st ^ "\n" ^ indent ^ "}\n"
- ^ indent ^ "else {\n" ^ false_st ^ "\n" ^ indent ^ "}"
- | A.SwitchInt (_ty, branches, otherwise) ->
- let indent1 = indent ^ indent_incr in
- let indent2 = indent1 ^ indent_incr in
- let inner_to_string2 =
- statement_to_string fmt indent2 indent_incr
- in
- let branches =
- List.map
- (fun (svl, be) ->
- let svl =
- List.map
- (fun sv -> "| " ^ PPV.scalar_value_to_string sv)
- svl
- in
- let svl = String.concat " " svl in
- indent1 ^ svl ^ " => {\n" ^ inner_to_string2 be ^ "\n"
- ^ indent1 ^ "}")
- branches
- in
- let branches = String.concat "\n" branches in
- let branches =
- branches ^ "\n" ^ indent1 ^ "_ => {\n"
- ^ inner_to_string2 otherwise ^ "\n" ^ indent1 ^ "}"
- in
- indent ^ "switch (" ^ op ^ ") {\n" ^ branches ^ "\n" ^ indent ^ "}")
- | A.Loop loop_st ->
- indent ^ "loop {\n"
- ^ statement_to_string fmt (indent ^ indent_incr) indent_incr loop_st
- ^ "\n" ^ indent ^ "}"
-
- let var_to_string (v : A.var) : string =
- match v.name with None -> PV.var_id_to_string v.index | Some name -> name
-
- let fun_decl_to_string (fmt : ast_formatter) (indent : string)
- (indent_incr : string) (def : A.fun_decl) : string =
- let sty_fmt = ast_to_stype_formatter fmt in
- let sty_to_string = PT.sty_to_string sty_fmt in
- let ety_fmt = ast_to_etype_formatter fmt in
- let ety_to_string = PT.ety_to_string ety_fmt in
- let sg = def.signature in
-
- (* Function name *)
- let name = fun_name_to_string def.A.name in
-
- (* Region/type parameters *)
- let regions = sg.region_params in
- let types = sg.type_params in
- let params =
- if List.length regions + List.length types = 0 then ""
- else
- let regions = List.map PT.region_var_to_string regions in
- let types = List.map PT.type_var_to_string types in
- "<" ^ String.concat "," (List.append regions types) ^ ">"
- in
-
- (* Return type *)
- let ret_ty = sg.output in
- let ret_ty =
- if TU.ty_is_unit ret_ty then "" else " -> " ^ sty_to_string ret_ty
- in
-
- (* We print the declaration differently if it is opaque (no body) or transparent
- * (we have access to a body) *)
- match def.body with
- | None ->
- (* Arguments *)
- let input_tys = sg.inputs in
- let args = List.map sty_to_string input_tys in
- let args = String.concat ", " args in
-
- (* Put everything together *)
- indent ^ "opaque fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty
- | Some body ->
- (* Arguments *)
- let inputs = List.tl body.locals in
- let inputs, _aux_locals =
- Collections.List.split_at inputs body.arg_count
- in
- let args = List.combine inputs sg.inputs in
- let args =
- List.map
- (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty)
- args
- in
- let args = String.concat ", " args in
-
- (* All the locals (with erased regions) *)
- let locals =
- List.map
- (fun var ->
- indent ^ indent_incr ^ var_to_string var ^ " : "
- ^ ety_to_string var.var_ty ^ ";")
- body.locals
- in
- let locals = String.concat "\n" locals in
-
- (* Body *)
- let body =
- statement_to_string fmt (indent ^ indent_incr) indent_incr body.body
- in
-
- (* Put everything together *)
- indent ^ "fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty ^ " {\n"
- ^ locals ^ "\n\n" ^ body ^ "\n" ^ indent ^ "}"
-end
-
-module PA = LlbcAst (* local module *)
-
(** Pretty-printing for contexts *)
module Contexts = struct
let binder_to_string (bv : C.binder) : string =
@@ -1129,105 +504,6 @@ end
module PC = Contexts (* local module *)
-(** Pretty-printing for ASTs (functions based on a definition context) *)
-module Module = struct
- (** This function pretty-prints a type definition by using a definition
- context *)
- let type_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
- (def : T.type_decl) : string =
- let type_decl_id_to_string (id : T.TypeDeclId.id) : string =
- let def = T.TypeDeclId.Map.find id type_context in
- name_to_string def.name
- in
- PT.type_decl_to_string type_decl_id_to_string def
-
- (** 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)
- (fun_context : A.fun_decl A.FunDeclId.Map.t)
- (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
- PT.region_var_to_string var
- in
- let r_to_string vid =
- (* TODO: we might want something more informative *)
- PT.region_id_to_string vid
- in
- let type_var_id_to_string vid =
- let var = T.TypeVarId.nth def.signature.type_params vid in
- PT.type_var_to_string var
- in
- let type_decl_id_to_string def_id =
- let def = T.TypeDeclId.Map.find def_id type_context in
- name_to_string def.name
- in
- let fun_decl_id_to_string def_id =
- let def = A.FunDeclId.Map.find def_id fun_context in
- fun_name_to_string def.name
- in
- let global_decl_id_to_string def_id =
- let def = A.GlobalDeclId.Map.find def_id global_context in
- global_name_to_string def.name
- in
- let var_id_to_string vid =
- let var = V.VarId.nth (Option.get def.body).locals vid in
- PA.var_to_string var
- in
- let adt_variant_to_string =
- PT.type_ctx_to_adt_variant_to_string_fun type_context
- in
- let adt_field_to_string =
- PT.type_ctx_to_adt_field_to_string_fun type_context
- in
- let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_context in
- {
- rvar_to_string;
- r_to_string;
- type_var_id_to_string;
- type_decl_id_to_string;
- adt_variant_to_string;
- adt_field_to_string;
- var_id_to_string;
- adt_field_names;
- fun_decl_id_to_string;
- global_decl_id_to_string;
- }
-
- (** 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)
- (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
- PA.fun_decl_to_string fmt "" " " def
-
- let module_to_string (m : Crates.llbc_crate) : string =
- let types_defs_map, funs_defs_map, globals_defs_map =
- Crates.compute_defs_maps m
- in
-
- (* The types *)
- let type_decls =
- List.map (type_decl_to_string types_defs_map) m.Crates.types
- in
-
- (* The functions *)
- let fun_decls =
- List.map
- (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
- m.Crates.functions
- in
-
- (* Put everything together *)
- let all_defs = List.append type_decls fun_decls in
- String.concat "\n\n" all_defs
-end
-
(** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *)
module EvalCtxLlbcAst = struct
let ety_to_string (ctx : C.eval_ctx) (t : T.ety) : string =
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 67353547..0b2e3a62 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -223,7 +223,7 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
* use indices of the variables in the original LLBC program, while
* regular places use indices for the pure variables: we want to make
* this explicit, otherwise it is confusing. *)
- let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in
+ let name = name ^ "^" ^ E.VarId.to_string p.var_id ^ "llbc" in
mprojection_to_string fmt name p.projection
let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ae4cba22..f9c693c6 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1,7 +1,7 @@
open Identifiers
open Names
-module T = Types
module PV = PrimitiveValues
+module T = Types
module V = Values
module E = Expressions
module A = LlbcAst
@@ -18,7 +18,7 @@ module GlobalDeclId = A.GlobalDeclId
for group of regions 0, etc.) *)
module SynthPhaseId = IdGen ()
-(** Pay attention to the fact that we also define a {!Values.VarId} module in Values *)
+(** Pay attention to the fact that we also define a {!E.VarId} module in Values *)
module VarId = IdGen ()
type integer_type = T.integer_type [@@deriving show, ord]
@@ -156,7 +156,7 @@ type mprojection = mprojection_elem list [@@deriving show]
we introduce.
*)
type mplace = {
- var_id : V.VarId.id;
+ var_id : E.VarId.id;
name : string option;
projection : mprojection;
}
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 5da07e55..81879883 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -104,7 +104,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
type pn_ctx = {
pure_vars : string VarId.Map.t;
(** Information about the pure variables used in the synthesized program *)
- llbc_vars : string V.VarId.Map.t;
+ llbc_vars : string E.VarId.Map.t;
(** Information about the LLBC variables used in the original program *)
}
@@ -237,14 +237,14 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
ctx0.pure_vars ctx1.pure_vars
in
let llbc_vars =
- V.VarId.Map.fold
- (fun id name ctx -> V.VarId.Map.add id name ctx)
+ E.VarId.Map.fold
+ (fun id name ctx -> E.VarId.Map.add id name ctx)
ctx0.llbc_vars ctx1.llbc_vars
in
{ pure_vars; llbc_vars }
in
let empty_ctx =
- { pure_vars = VarId.Map.empty; llbc_vars = V.VarId.Map.empty }
+ { pure_vars = VarId.Map.empty; llbc_vars = E.VarId.Map.empty }
in
let merge_ctxs_ls (ctxs : pn_ctx list) : pn_ctx =
List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) empty_ctx ctxs
@@ -281,7 +281,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| None ->
if Option.is_some mp then
match
- V.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars
+ E.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars
with
| None -> v
| Some basename -> { v with basename = Some basename }
@@ -300,9 +300,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
(* Register an mplace the first time we find one *)
let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx =
- match (V.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
+ match (E.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
| None, Some name ->
- let llbc_vars = V.VarId.Map.add mp.var_id name ctx.llbc_vars in
+ let llbc_vars = E.VarId.Map.add mp.var_id name ctx.llbc_vars in
{ ctx with llbc_vars }
| _ -> ctx
in
@@ -318,11 +318,11 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
{ ctx with pure_vars }
in
(* Similar to [add_pure_var_constraint], but for LLBC variables *)
- let add_llbc_var_constraint (var_id : V.VarId.id) (name : string)
+ let add_llbc_var_constraint (var_id : E.VarId.id) (name : string)
(ctx : pn_ctx) : pn_ctx =
let llbc_vars =
- if V.VarId.Map.mem var_id ctx.llbc_vars then ctx.llbc_vars
- else V.VarId.Map.add var_id name ctx.llbc_vars
+ if E.VarId.Map.mem var_id ctx.llbc_vars then ctx.llbc_vars
+ else E.VarId.Map.add var_id name ctx.llbc_vars
in
{ ctx with llbc_vars }
in
@@ -399,7 +399,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
| Some { var_id; name; projection = [] } -> (
if Option.is_some name then add (Option.get name) ctx
else
- match V.VarId.Map.find_opt var_id ctx.llbc_vars with
+ match E.VarId.Map.find_opt var_id ctx.llbc_vars with
| None -> ctx
| Some name -> add name ctx)
| _ -> ctx
@@ -500,7 +500,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let name =
match name with
| Some name -> Some name
- | None -> V.VarId.Map.find_opt var_id ctx.llbc_vars
+ | None -> E.VarId.Map.find_opt var_id ctx.llbc_vars
in
match name with
| None -> ctx
@@ -530,7 +530,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
let ctx =
{
pure_vars = VarId.Map.of_list input_names;
- llbc_vars = V.VarId.Map.empty;
+ llbc_vars = E.VarId.Map.empty;
}
in
let _, body_exp = update_texpression body.body ctx in
diff --git a/compiler/Scalars.ml b/compiler/Scalars.ml
index 03ca506c..8a1e981b 100644
--- a/compiler/Scalars.ml
+++ b/compiler/Scalars.ml
@@ -1,59 +1 @@
-open Types
-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,
- the values are encoded as 32-bit values or 64-bit values - we may
- 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 *)
-let check_int_in_range (int_ty : integer_type) (i : big_int) : bool =
- match int_ty with
- | Isize -> Z.leq isize_min i && Z.leq i isize_max
- | I8 -> Z.leq i8_min i && Z.leq i i8_max
- | I16 -> Z.leq i16_min i && Z.leq i i16_max
- | I32 -> Z.leq i32_min i && Z.leq i i32_max
- | I64 -> Z.leq i64_min i && Z.leq i i64_max
- | I128 -> Z.leq i128_min i && Z.leq i i128_max
- | Usize -> Z.leq usize_min i && Z.leq i usize_max
- | U8 -> Z.leq u8_min i && Z.leq i u8_max
- | U16 -> Z.leq u16_min i && Z.leq i u16_max
- | U32 -> Z.leq u32_min i && Z.leq i u32_max
- | U64 -> Z.leq u64_min i && Z.leq i u64_max
- | U128 -> Z.leq u128_min i && Z.leq i u128_max
-
-(** Check that a scalar value is correct (the integer value it contains is in range) *)
-let check_scalar_value_in_range (v : scalar_value) : bool =
- check_int_in_range v.int_ty v.value
-
-(** Make a scalar value, while checking the value is in range *)
-let mk_scalar (int_ty : integer_type) (i : big_int) :
- (scalar_value, unit) result =
- if check_int_in_range int_ty i then Ok { value = i; int_ty } else Error ()
+include Charon.Scalars
diff --git a/compiler/Types.ml b/compiler/Types.ml
index 326ef76f..c76b6ffa 100644
--- a/compiler/Types.ml
+++ b/compiler/Types.ml
@@ -1,208 +1 @@
-open Identifiers
-open Names
-open Meta
-module TypeVarId = IdGen ()
-module TypeDeclId = IdGen ()
-module VariantId = IdGen ()
-module FieldId = IdGen ()
-
-(** Region variable ids. Used in function signatures. *)
-module RegionVarId = IdGen ()
-
-(** Region ids. Used for symbolic executions. *)
-module RegionId = IdGen ()
-
-module RegionGroupId = IdGen ()
-
-type ('id, 'name) indexed_var = {
- index : 'id; (** Unique index identifying the variable *)
- name : 'name; (** Variable name *)
-}
-[@@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.
-
- Regions are used in function signatures (in which case we use region variable
- ids) and in symbolic variables and projections (in which case we use region
- ids).
- *)
-type 'rid region =
- | Static (** Static region *)
- | Var of 'rid (** Non-static region *)
-[@@deriving show, ord]
-
-(** The type of erased regions.
-
- We could use unit, but having a dedicated type makes things more explicit.
- *)
-type erased_region = Erased [@@deriving show, ord]
-
-(** A group of regions.
-
- Results from a lifetime analysis: we group the regions with the same
- lifetime together, and compute the hierarchy between the regions.
- This is necessary to introduce the proper abstraction with the
- proper constraints, when evaluating a function call in symbolic mode.
-*)
-type ('id, 'r) g_region_group = {
- id : 'id;
- regions : 'r list;
- parents : 'id list;
-}
-[@@deriving show]
-
-type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
-
-type region_var_group = (RegionGroupId.id, RegionVarId.id) g_region_group
-[@@deriving show]
-
-type region_var_groups = (RegionGroupId.id, RegionVarId.id) g_region_groups
-[@@deriving show]
-
-type integer_type =
- | Isize
- | I8
- | I16
- | I32
- | I64
- | I128
- | Usize
- | U8
- | U16
- | U32
- | U64
- | U128
-[@@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] *)
-let option_none_id = VariantId.of_int 0
-
-(** The variant id for [Option::Some] *)
-let option_some_id = VariantId.of_int 1
-
-(** Type identifier for ADTs.
-
- ADTs are very general in our encoding: they account for "regular" ADTs,
- tuples and also assumed types.
-*)
-type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
-[@@deriving show, ord]
-
-(** Ancestor for iter visitor for [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
-
-(** Ancestor for map visitor for [ty] *)
-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 =
- fun _ ity -> ity
-
- method visit_ref_kind : 'env -> ref_kind -> ref_kind = fun _ rk -> rk
- end
-
-type 'r ty =
- | Adt of type_id * 'r list * 'r ty list
- (** {!Adt} encodes ADTs, tuples and assumed types *)
- | TypeVar of TypeVarId.id
- | Bool
- | Char
- | Never
- | Integer of integer_type
- | Str
- | Array of 'r ty (* TODO: there should be a constant with the array *)
- | Slice of 'r ty
- | Ref of 'r * 'r ty * ref_kind
-[@@deriving
- show,
- ord,
- visitors
- {
- name = "iter_ty";
- variety = "iter";
- ancestors = [ "iter_ty_base" ];
- nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
- concrete = true;
- polymorphic = false;
- },
- visitors
- {
- name = "map_ty";
- variety = "map";
- ancestors = [ "map_ty_base" ];
- nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
- concrete = true;
- polymorphic = false;
- }]
-(* TODO: group Bool, Char, etc. in Constant *)
-
-(** Generic type with regions *)
-type 'r gr_ty = 'r region ty [@@deriving show, ord]
-
-(** *S*ignature types.
-
- Used in function signatures and type definitions.
- *)
-type sty = RegionVarId.id gr_ty [@@deriving show, ord]
-
-(** Type with *R*egions.
-
- Used to project borrows/loans inside of abstractions, during symbolic
- execution.
- *)
-type rty = RegionId.id gr_ty [@@deriving show, ord]
-
-(** Type with *E*rased regions.
-
- Used in function bodies, "regular" value types, etc.
- *)
-type ety = erased_region ty [@@deriving show, ord]
-
-type field = { meta : meta; field_name : string option; field_ty : sty }
-[@@deriving show]
-
-type variant = { meta : meta; variant_name : string; fields : field list }
-[@@deriving show]
-
-type type_decl_kind =
- | Struct of field list
- | Enum of variant list
- | Opaque
- (** An opaque type: either a local type marked as opaque, or an external type *)
-[@@deriving show]
-
-type type_decl = {
- def_id : TypeDeclId.id;
- meta : meta;
- name : type_name;
- region_params : region_var list;
- type_params : type_var list;
- kind : type_decl_kind;
- regions_hierarchy : region_var_groups;
- (** Stores the hierarchy between the regions (which regions have the
- same lifetime, which lifetime should end before which other lifetime,
- etc.) *)
-}
-[@@deriving show]
+include Charon.Types
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index 7531dd8b..c7f0fbc3 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -1,130 +1,7 @@
open Types
-open Utils
+include Charon.TypesUtils
module TA = TypesAnalysis
-let type_decl_is_opaque (d : type_decl) : bool =
- match d.kind with Struct _ | Enum _ -> false | Opaque -> true
-
-(** Retrieve the list of fields for the given variant of a {!Types.type_decl}.
-
- Raises [Invalid_argument] if the arguments are incorrect.
- *)
-let type_decl_get_fields (def : type_decl)
- (opt_variant_id : VariantId.id option) : field list =
- match (def.kind, opt_variant_id) with
- | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
- | Struct fields, None -> fields
- | _ ->
- let opt_variant_id =
- match opt_variant_id with None -> "None" | Some _ -> "Some"
- in
- raise
- (Invalid_argument
- ("The variant id should be [Some] if and only if the definition is \
- an enumeration:\n\
- - def: " ^ show_type_decl def ^ "\n- opt_variant_id: "
- ^ opt_variant_id))
-
-(** Return [true] if a {!Types.ty} is actually [unit] *)
-let ty_is_unit (ty : 'r ty) : bool =
- match ty with Adt (Tuple, [], []) -> true | _ -> false
-
-let ty_is_adt (ty : 'r ty) : bool =
- match ty with Adt (_, _, _) -> true | _ -> false
-
-let ty_as_adt (ty : 'r ty) : type_id * 'r list * 'r ty list =
- match ty with
- | Adt (id, regions, tys) -> (id, regions, tys)
- | _ -> failwith "Unreachable"
-
-let ty_is_custom_adt (ty : 'r ty) : bool =
- match ty with Adt (AdtId _, _, _) -> true | _ -> false
-
-let ty_as_custom_adt (ty : 'r ty) : TypeDeclId.id * 'r list * 'r ty list =
- match ty with
- | Adt (AdtId id, regions, tys) -> (id, regions, tys)
- | _ -> failwith "Unreachable"
-
-(** The unit type *)
-let mk_unit_ty : 'r ty = Adt (Tuple, [], [])
-
-(** The usize type *)
-let mk_usize_ty : 'r ty = Integer Usize
-
-(** Deconstruct a type of the form [Box<T>] to retrieve the [T] inside *)
-let ty_get_box (box_ty : ety) : ety =
- match box_ty with
- | Adt (Assumed Box, [], [ boxed_ty ]) -> boxed_ty
- | _ -> failwith "Not a boxed type"
-
-(** Deconstruct a type of the form [&T] or [&mut T] to retrieve the [T] (and
- the borrow kind, etc.)
- *)
-let ty_get_ref (ty : 'r ty) : 'r * 'r ty * ref_kind =
- match ty with
- | Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
- | _ -> failwith "Not a ref type"
-
-let mk_ref_ty (r : 'r) (ty : 'r ty) (ref_kind : ref_kind) : 'r ty =
- Ref (r, ty, ref_kind)
-
-(** Make a box type *)
-let mk_box_ty (ty : 'r ty) : 'r ty = Adt (Assumed Box, [], [ ty ])
-
-(** Make a vec type *)
-let mk_vec_ty (ty : 'r ty) : 'r ty = Adt (Assumed Vec, [], [ ty ])
-
-(** Check if a region is in a set of regions *)
-let region_in_set (r : RegionId.id region) (rset : RegionId.Set.t) : bool =
- match r with Static -> false | Var id -> RegionId.Set.mem id rset
-
-(** Return the set of regions in an rty *)
-let rty_regions (ty : rty) : RegionId.Set.t =
- let s = ref RegionId.Set.empty in
- let add_region (r : RegionId.id region) =
- match r with Static -> () | Var rid -> s := RegionId.Set.add rid !s
- in
- let obj =
- object
- inherit [_] iter_ty
- method! visit_'r _env r = add_region r
- end
- in
- (* Explore the type *)
- obj#visit_ty () ty;
- (* Return the set of accumulated regions *)
- !s
-
-let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool =
- let ty_regions = rty_regions ty in
- not (RegionId.Set.disjoint ty_regions regions)
-
-(** Convert an {!Types.ety}, containing no region variables, to an {!Types.rty}
- or an {!Types.sty}.
-
- In practice, it is the identity.
- *)
-let rec ety_no_regions_to_gr_ty (ty : ety) : 'a gr_ty =
- match ty with
- | Adt (type_id, regions, tys) ->
- assert (regions = []);
- Adt (type_id, [], List.map ety_no_regions_to_gr_ty tys)
- | TypeVar v -> TypeVar v
- | Bool -> Bool
- | Char -> Char
- | Never -> Never
- | Integer int_ty -> Integer int_ty
- | Str -> Str
- | Array ty -> Array (ety_no_regions_to_gr_ty ty)
- | Slice ty -> Slice (ety_no_regions_to_gr_ty ty)
- | Ref (_, _, _) ->
- failwith
- "Can't convert a ref with erased regions to a ref with non-erased \
- regions"
-
-let ety_no_regions_to_rty (ty : ety) : rty = ety_no_regions_to_gr_ty ty
-let ety_no_regions_to_sty (ty : ety) : sty = ety_no_regions_to_gr_ty ty
-
(** Retuns true if the type contains borrows.
Note that we can't simply explore the type and look for regions: sometimes
@@ -149,42 +26,3 @@ let ty_has_nested_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
let ty_has_borrow_under_mut (infos : TA.type_infos) (ty : 'r ty) : bool =
let info = TA.analyze_ty infos ty in
info.TA.contains_borrow_under_mut
-
-(** Check if a {!Types.ty} contains regions from a given set *)
-let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool =
- let obj =
- object
- inherit [_] iter_ty as super
-
- method! visit_Adt env type_id regions tys =
- List.iter (fun r -> if region_in_set r rset then raise Found) regions;
- super#visit_Adt env type_id regions tys
-
- method! visit_Ref env r ty rkind =
- if region_in_set r rset then raise Found
- else super#visit_Ref env r ty rkind
- end
- in
- try
- obj#visit_ty () ty;
- false
- with Found -> true
-
-(** Return true if a type is "primitively copyable".
- *
- * "primitively copyable" means that copying instances of this type doesn't
- * require calling dedicated functions defined through the Copy trait. It
- * is the case for types like integers, shared borrows, etc.
- *
- * Generally, ADTs are not copyable. However, some of the primitive ADTs are
- * like `Option`.
- *)
-let rec ty_is_primitively_copyable (ty : 'r ty) : bool =
- match ty with
- | Adt (Assumed Option, _, tys) -> List.for_all ty_is_primitively_copyable tys
- | Adt ((AdtId _ | Assumed (Box | Vec)), _, _) -> false
- | Adt (Tuple, _, tys) -> List.for_all ty_is_primitively_copyable tys
- | TypeVar _ | Never | Str | Array _ | Slice _ -> false
- | Bool | Char | Integer _ -> true
- | Ref (_, _, Mut) -> false
- | Ref (_, _, Shared) -> true
diff --git a/compiler/Utils.ml b/compiler/Utils.ml
index 9a79eb55..987ac317 100644
--- a/compiler/Utils.ml
+++ b/compiler/Utils.ml
@@ -1,6 +1 @@
-(** Utility exception
-
- When looking for something while exploring a term, it can be easier to
- just throw an exception to signal we found what we were looking for.
- *)
-exception Found
+include Charon.Utils
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 7d6623aa..6245608d 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -1,11 +1,11 @@
open Identifiers
open Types
+module PrimitiveValues = PrimitiveValues
(* TODO(SH): I often write "abstract" (value, borrow content, etc.) while I should
* write "abstraction" (because those values are not abstract, they simply are
* inside abstractions) *)
-module VarId = IdGen ()
module BorrowId = IdGen ()
module SymbolicValueId = IdGen ()
module AbstractionId = IdGen ()
diff --git a/compiler/dune b/compiler/dune
index f0fd2102..d3f5eaec 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -1,12 +1,8 @@
-;; core: for Core.Unix.mkdir_p
-
(executable
(name driver)
(public_name aeneas_driver)
(package aeneas)
- (preprocess
- (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries ppx_deriving yojson zarith easy_logging core_unix aeneas)
+ (libraries aeneas)
(modules Driver))
(library
@@ -14,7 +10,7 @@
(public_name aeneas) ;; The name as revealed to the projects importing this library
(preprocess
(pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries ppx_deriving yojson zarith easy_logging core_unix)
+ (libraries charon core_unix)
(modules
Assumed
Collections
@@ -44,7 +40,6 @@
Logging
Meta
Names
- OfJsonBasic
PrePasses
Print
PrintPure
diff --git a/compiler/dune-project b/compiler/dune-project
index f8b418f2..650eeec0 100644
--- a/compiler/dune-project
+++ b/compiler/dune-project
@@ -6,8 +6,6 @@
(generate_opam_files true)
-(formatting)
-
(source
(uri git+https://github.com/AeneasVerif/aeneas.git))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 01:15:38 +0000