Skip to content

Commit

Permalink
Update Charon (#364)
Browse files Browse the repository at this point in the history 
* Make minor modifications

* Update the Charon pin

* Update the Charon pin

* Update the Charon pin
  • Loading branch information
@sonmarcho
sonmarcho authored Nov 21, 2024
1 parent ee2f13b commit a8b8b2c
Show file tree
Hide file tree
Showing 8 changed files with 284 additions and 237 deletions.
2 changes: 1 addition & 1 deletion charon-pin
View file
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
# This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
c641098d7443a243c4e5b4d5150421e87f85caac
bab27dafb31080ef97d48e5589a33c0e95f2eb05
12 changes: 6 additions & 6 deletions flake.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions src/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
Config
ConstStrings
Contexts
ContextsBase
Cps
Errors
Expressions
Expand Down
39 changes: 17 additions & 22 deletions src/llbc/AssociatedTypes.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,16 @@ open TypesUtils
open Values
open LlbcAst
open Contexts
open Substitute
open Errors
module Subst = Substitute

(** The local logger *)
let log = Logging.associated_types_log

let trait_type_ref_substitute (subst : Subst.subst) (r : trait_type_ref) :
let trait_type_ref_substitute (subst : subst) (r : trait_type_ref) :
trait_type_ref =
let { trait_ref; type_name } = r in
let trait_ref = Subst.trait_ref_substitute subst trait_ref in
let trait_ref = trait_ref_substitute subst trait_ref in
{ trait_ref; type_name }

module TyOrd = struct
Expand Down Expand Up @@ -173,14 +173,12 @@ let generic_params_to_string (ctx : norm_ctx) (x : generic_params) : string =

(** Small utility to lookup trait impls, together with a substitution. *)
let norm_ctx_lookup_trait_impl (ctx : norm_ctx) (impl_id : TraitImplId.id)
(generics : generic_args) : trait_impl * Subst.subst =
(generics : generic_args) : trait_impl * subst =
(* Lookup the implementation *)
let trait_impl = TraitImplId.Map.find impl_id ctx.trait_impls in
(* The substitution *)
let tr_self = UnknownTrait __FUNCTION__ in
let subst =
Subst.make_subst_from_generics trait_impl.generics generics tr_self
in
let subst = make_subst_from_generics trait_impl.generics generics tr_self in
(* Return *)
(trait_impl, subst)

Expand All @@ -191,7 +189,7 @@ let norm_ctx_lookup_trait_impl_ty (ctx : norm_ctx) (impl_id : TraitImplId.id)
(* Lookup the type *)
let ty = List.assoc type_name trait_impl.types in
(* Substitute *)
Subst.ty_substitute subst ty
ty_substitute subst ty

let norm_ctx_lookup_trait_impl_parent_clause (ctx : norm_ctx)
(impl_id : TraitImplId.id) (generics : generic_args)
Expand All @@ -203,7 +201,7 @@ let norm_ctx_lookup_trait_impl_parent_clause (ctx : norm_ctx)
(* Sanity check: the clause necessarily refers to an impl *)
let _ = TypesUtils.trait_instance_id_as_trait_impl clause.trait_id in
(* Substitute *)
Subst.trait_ref_substitute subst clause
trait_ref_substitute subst clause

(** Normalize a type by simplifying the references to trait associated types
and choosing a representative when there are equalities between types
Expand Down Expand Up @@ -453,7 +451,7 @@ let ctx_normalize_ty (span : Meta.span option) (ctx : eval_ctx) (ty : ty) : ty =
(** Normalize a type and erase the regions at the same time *)
let ctx_normalize_erase_ty (span : Meta.span) (ctx : eval_ctx) (ty : ty) : ty =
let ty = ctx_normalize_ty (Some span) ctx ty in
Subst.erase_regions ty
erase_regions ty

let ctx_normalize_trait_type_constraint_region_binder (span : Meta.span)
(ctx : eval_ctx) (ttc : trait_type_constraint region_binder) :
Expand All @@ -466,9 +464,7 @@ let ctx_normalize_trait_type_constraint_region_binder (span : Meta.span)
let type_decl_get_inst_norm_variants_fields_rtypes (span : Meta.span)
(ctx : eval_ctx) (def : type_decl) (generics : generic_args) :
(VariantId.id option * ty list) list =
let res =
Subst.type_decl_get_instantiated_variants_fields_types def generics
in
let res = type_decl_get_instantiated_variants_fields_types def generics in
List.map
(fun (variant_id, types) ->
(variant_id, List.map (ctx_normalize_ty (Some span) ctx) types))
Expand All @@ -479,15 +475,15 @@ let type_decl_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
(def : type_decl) (opt_variant_id : VariantId.id option)
(generics : generic_args) : ty list =
let types =
Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
type_decl_get_instantiated_field_types def opt_variant_id generics
in
List.map (ctx_normalize_ty (Some span) ctx) types

(** Same as [ctx_adt_value_get_instantiated_field_rtypes] but normalizes the types *)
let ctx_adt_value_get_inst_norm_field_rtypes (span : Meta.span) (ctx : eval_ctx)
(adt : adt_value) (id : type_id) (generics : generic_args) : ty list =
let types =
Subst.ctx_adt_value_get_instantiated_field_types span ctx adt id generics
ctx_adt_value_get_instantiated_field_types span ctx adt id generics
in
List.map (ctx_normalize_ty (Some span) ctx) types

Expand All @@ -497,22 +493,21 @@ let type_decl_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
(def : type_decl) (opt_variant_id : VariantId.id option)
(generics : generic_args) : ty list =
let types =
Subst.type_decl_get_instantiated_field_types def opt_variant_id generics
type_decl_get_instantiated_field_types def opt_variant_id generics
in
let types = List.map (ctx_normalize_ty (Some span) ctx) types in
List.map Subst.erase_regions types
List.map erase_regions types

(** Same as [ctx_adt_get_instantiated_field_types] but normalizes the types and
erases the regions. *)
let ctx_adt_get_inst_norm_field_etypes (span : Meta.span) (ctx : eval_ctx)
(def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option)
(generics : generic_args) : ty list =
let types =
Subst.ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id
generics
ctx_adt_get_instantiated_field_types ctx def_id opt_variant_id generics
in
let types = List.map (ctx_normalize_ty (Some span) ctx) types in
List.map Subst.erase_regions types
List.map erase_regions types

(** Same as [substitute_signature] but normalizes the types *)
let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
Expand All @@ -523,8 +518,8 @@ let ctx_subst_norm_signature (span : Meta.span) (ctx : eval_ctx)
(tr_self : trait_instance_id) (sg : fun_sig)
(regions_hierarchy : region_var_groups) : inst_fun_sig =
let sg =
Subst.substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self
sg regions_hierarchy
substitute_signature asubst r_subst ty_subst cg_subst tr_subst tr_self sg
regions_hierarchy
in
let { regions_hierarchy; inputs; output; trait_type_constraints } = sg in
let inputs = List.map (ctx_normalize_ty (Some span) ctx) inputs in
Expand Down
209 changes: 42 additions & 167 deletions src/llbc/Contexts.ml
View file
Original file line number Diff line number Diff line change
@@ -1,178 +1,13 @@
open Types
open TypesUtils
open Expressions
open Values
open LlbcAst
open LlbcAstUtils
open ValuesUtils
open Identifiers
open Errors
module L = Logging

(** The [Id] module for dummy variables.
Dummy variables are used to store values that we don't want to forget
in the environment, because they contain borrows for instance, typically
because they might be overwritten during an assignment.
*)
module DummyVarId =
IdGen ()

type dummy_var_id = DummyVarId.id [@@deriving show, ord]

(** The local logger *)
let log = L.contexts_log

(** Some global counters.
Note that those counters were initially stored in {!eval_ctx} values,
but it proved better to make them global and stateful:
- when branching (and thus executing on several paths with different
contexts) it is better to really have unique ids everywhere (and
not have fresh ids shared by several contexts even though introduced
after the branching) because at some point we might need to merge the
different contexts
- also, it is a lot more convenient to not store those counters in contexts
objects
=============
**WARNING**:
=============
Pay attention when playing with closures, as you may not always generate
fresh identifiers without noticing it, especially when using type abbreviations.
For instance, consider the following:
{[
type fun_type = unit -> ...
fn f x : fun_type =
let id = fresh_id () in
...
fun () -> ...
let g = f x in // <-- the fresh identifier gets generated here
let x1 = g () in // <-- no fresh generation here
let x2 = g () in
...
]}
This is why, in such cases, we often introduce all the inputs, even
when they are not used (which happens!).
{[
fn f x : fun_type =
fun .. ->
let id = fresh_id () in
...
]}
Note that in practice, we never reuse closures, except when evaluating
a branching in the execution (which is fine, because the branches evaluate
independentely of each other). Still, it is always a good idea to be
defensive.
However, the same problem arises with logging.
Also, a more defensive way would be to not use global references, and
store the counters in the evaluation context. This is actually what was
originally done, before we updated the code to use global counters because
it proved more convenient (and even before updating the code of the
interpreter to use CPS).
*)

let symbolic_value_id_counter, fresh_symbolic_value_id =
SymbolicValueId.fresh_stateful_generator ()

let borrow_id_counter, fresh_borrow_id = BorrowId.fresh_stateful_generator ()
let region_id_counter, fresh_region_id = RegionId.fresh_stateful_generator ()

let abstraction_id_counter, fresh_abstraction_id =
AbstractionId.fresh_stateful_generator ()

let loop_id_counter, fresh_loop_id = LoopId.fresh_stateful_generator ()

let fun_call_id_counter, fresh_fun_call_id =
FunCallId.fresh_stateful_generator ()

let dummy_var_id_counter, fresh_dummy_var_id =
DummyVarId.fresh_stateful_generator ()

(** We shouldn't need to reset the global counters, but it might be good to
do it from time to time, for instance every time we start evaluating/
synthesizing a function.
The reasons are manifold:
- it might prevent the counters from overflowing (although this seems
extremely unlikely - as a side node: we have overflow checks to make
sure the synthesis doesn't get impacted by potential overflows)
- most importantly, it allows to always manipulate low values, which
is always a lot more readable when debugging
*)
let reset_global_counters () =
symbolic_value_id_counter := SymbolicValueId.generator_zero;
borrow_id_counter := BorrowId.generator_zero;
region_id_counter := RegionId.generator_zero;
abstraction_id_counter := AbstractionId.generator_zero;
loop_id_counter := LoopId.generator_zero;
(* We want the loop id to start at 1 *)
let _ = fresh_loop_id () in
fun_call_id_counter := FunCallId.generator_zero;
dummy_var_id_counter := DummyVarId.generator_zero

(** Ancestor for {!type:env} iter visitor *)
class ['self] iter_env_base =
object (_self : 'self)
inherit [_] iter_abs
method visit_var_id : 'env -> var_id -> unit = fun _ _ -> ()
method visit_dummy_var_id : 'env -> dummy_var_id -> unit = fun _ _ -> ()
end

(** Ancestor for {!type:env} map visitor *)
class ['self] map_env_base =
object (_self : 'self)
inherit [_] map_abs
method visit_var_id : 'env -> var_id -> var_id = fun _ x -> x

method visit_dummy_var_id : 'env -> dummy_var_id -> dummy_var_id =
fun _ x -> x
end

(** A binder used in an environment, to map a variable to a value *)
type var_binder = {
index : var_id; (** Unique variable identifier *)
name : string option; (** Possible name *)
}

(** A binder, for a "real" variable or a dummy variable *)
and binder = BVar of var_binder | BDummy of dummy_var_id

(** Environment value: mapping from variable to value, abstraction (only
used in symbolic mode) or stack frame delimiter.
*)
and env_elem =
| EBinding of binder * typed_value
(** Variable binding - the binder is None if the variable is a dummy variable
(we use dummy variables to store temporaries while doing bookkeeping such
as ending borrows for instance). *)
| EAbs of abs
| EFrame

and env = env_elem list
[@@deriving
show,
ord,
visitors
{
name = "iter_env";
variety = "iter";
ancestors = [ "iter_env_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
concrete = true;
},
visitors
{
name = "map_env";
variety = "map";
ancestors = [ "map_env_base" ];
nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
concrete = true;
}]
include ContextsBase

module OrderedBinder : Collections.OrderedType with type t = binder = struct
type t = binder
Expand Down Expand Up @@ -648,3 +483,43 @@ let env_filter_abs (f : abs -> bool) (env : env) : env =
| EBinding _ | EFrame -> true
| EAbs abs -> f abs)
env

(** Return the types of the properly instantiated ADT's variant, provided a
context.
**IMPORTANT**: this function doesn't normalize the types, you may want to
use the [AssociatedTypes] equivalent instead.
*)
let ctx_adt_get_instantiated_field_types (ctx : eval_ctx)
(def_id : TypeDeclId.id) (opt_variant_id : VariantId.id option)
(generics : generic_args) : ty list =
let def = ctx_lookup_type_decl ctx def_id in
Substitute.type_decl_get_instantiated_field_types def opt_variant_id generics

(** Return the types of the properly instantiated ADT value (note that
here, ADT is understood in its broad meaning: ADT, builtin value or tuple).
**IMPORTANT**: this function doesn't normalize the types, you may want to
use the [AssociatedTypes] equivalent instead.
*)
let ctx_adt_value_get_instantiated_field_types (span : Meta.span)
(ctx : eval_ctx) (adt : adt_value) (id : type_id) (generics : generic_args)
: ty list =
match id with
| TAdtId id ->
(* Retrieve the types of the fields *)
ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics
| TTuple ->
cassert __FILE__ __LINE__ (generics.regions = []) span
"Tuples don't have region parameters";
generics.types
| TBuiltin aty -> (
match aty with
| TBox ->
sanity_check __FILE__ __LINE__ (generics.regions = []) span;
sanity_check __FILE__ __LINE__ (List.length generics.types = 1) span;
sanity_check __FILE__ __LINE__ (generics.const_generics = []) span;
generics.types
| TArray | TSlice | TStr ->
(* Those types don't have fields *)
craise __FILE__ __LINE__ span "Unreachable")
Loading

0 comments on commit a8b8b2c

Please sign in to comment.