From f45502c131fc6aae08aa5f0049911b85ba13529f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 27 Oct 2022 17:53:32 +0200 Subject: Move some files to the Charon project --- compiler/Assumed.ml | 6 +- compiler/Collections.ml | 379 +--------------- compiler/Contexts.ml | 1 + compiler/Crates.ml | 91 +--- compiler/Errors.ml | 3 +- compiler/Expressions.ml | 119 +---- compiler/ExpressionsUtils.ml | 11 +- compiler/Identifiers.ml | 140 +----- compiler/InterpreterStatements.ml | 18 +- compiler/InterpreterUtils.ml | 6 +- compiler/LlbcAst.ml | 190 +------- compiler/LlbcAstUtils.ml | 61 +-- compiler/LlbcOfJson.ml | 918 +------------------------------------- compiler/Logging.ml | 138 +----- compiler/Meta.ml | 45 +- compiler/Names.ml | 81 +--- compiler/OfJsonBasic.ml | 75 ---- compiler/PrimitiveValues.ml | 42 +- compiler/Print.ml | 732 +----------------------------- compiler/PrintPure.ml | 2 +- compiler/Pure.ml | 6 +- compiler/PureMicroPasses.ml | 26 +- compiler/Scalars.ml | 60 +-- compiler/Types.ml | 209 +-------- compiler/TypesUtils.ml | 164 +------ compiler/Utils.ml | 7 +- compiler/Values.ml | 2 +- compiler/dune | 9 +- compiler/dune-project | 2 - 29 files changed, 57 insertions(+), 3486 deletions(-) delete mode 100644 compiler/OfJsonBasic.ml (limited to 'compiler') 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::>::deref] *) - | BoxDerefMut - (** [core::ops::deref::DerefMut::>::deref_mut] *) - | BoxFree - | VecNew - | VecPush - | VecInsert - | VecLen - | VecIndex (** [core::ops::index::Index::index, usize>] *) - | VecIndexMut - (** [core::ops::index::IndexMut::index_mut, 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 List { - ... - } - ]} - - 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::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::index" - | A.VecIndexMut -> - "core::ops::index::IndexMut::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] 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)) -- cgit v1.2.3