From 71834958a958523a4881d822e729af1ddd78c9df Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 23 May 2024 10:56:28 +0200 Subject: Add printing of projectors for recursive structs in Lean backend --- compiler/ExtractTypes.ml | 133 +++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 130 insertions(+), 3 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 6a6067de..4272e7a9 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1662,6 +1662,127 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 +(** Auxiliary function. + + Generate field projectors in Lean. + + Recursive structs are defined as inductives in Lean. + Field projectors allow to retrieve the facilities provided by + Lean structures. + *) +let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) + (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = + sanity_check __FILE__ __LINE__ (!backend = Lean) decl.meta; + match decl.kind with + | Opaque | Enum _ -> () + | Struct fields -> + (* Records are extracted as inductives only if they are recursive *) + let is_rec = decl_is_from_rec_group kind in + if is_rec then + (* Add the type params *) + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params decl.meta decl.llbc_name decl.llbc_generics + decl.generics ctx + in + (* Record_var will be the ADT argument to the projector *) + let ctx, record_var = ctx_add_var decl.meta "x" (VarId.of_int 0) ctx in + (* Field_var will be the variable in the constructor that is returned by the projector *) + let ctx, field_var = ctx_add_var decl.meta "x" (VarId.of_int 1) ctx in + (* Name of the ADT *) + let def_name = ctx_get_local_type decl.meta decl.def_id ctx in + (* Name of the ADT constructor. As we are in the struct case, we only have + one constructor *) + let cons_name = ctx_get_struct decl.meta (TAdtId decl.def_id) ctx in + + let extract_field_proj (field_id : FieldId.id) (_ : field) : unit = + F.pp_print_space fmt (); + (* Box for the projector definition *) + F.pp_open_hvbox fmt 0; + (* Box for the [def ADT.proj ... :=] *) + F.pp_open_hovbox fmt ctx.indent_incr; + F.pp_print_string fmt "def"; + F.pp_print_space fmt (); + + (* Print the function name. In Lean, the syntax ADT.proj will + allow us to call x.proj for any x of type ADT *) + let field_name = + ctx_get_field decl.meta (TAdtId decl.def_id) field_id ctx + in + F.pp_print_string fmt def_name; + F.pp_print_string fmt "."; + F.pp_print_string fmt field_name; + + (* Print the generics *) + let as_implicits = true in + extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty + ~as_implicits decl.generics type_params cg_params trait_clauses; + + (* Print the record parameter as "(x : ADT)" *) + F.pp_print_space fmt (); + F.pp_print_string fmt "("; + F.pp_print_string fmt record_var; + F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + F.pp_print_string fmt def_name; + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + type_params; + F.pp_print_string fmt ")"; + + F.pp_print_space fmt (); + F.pp_print_string fmt ":="; + + (* Close the box for the [def ADT.proj ... :=] *) + F.pp_close_box fmt (); + F.pp_print_space fmt (); + + (* Open a box for the whole match *) + F.pp_open_hvbox fmt 0; + + (* Open a box for the [match ... with] *) + F.pp_open_hovbox fmt ctx.indent_incr; + F.pp_print_string fmt "match"; + F.pp_print_space fmt (); + F.pp_print_string fmt record_var; + F.pp_print_space fmt (); + F.pp_print_string fmt "with"; + (* Close the box for the [match ... with] *) + F.pp_close_box fmt (); + + (* Open a box for the branch *) + F.pp_open_hovbox fmt ctx.indent_incr; + (* Print the match branch *) + F.pp_print_space fmt (); + F.pp_print_string fmt "|"; + F.pp_print_space fmt (); + F.pp_print_string fmt cons_name; + FieldId.iteri + (fun id _ -> + F.pp_print_space fmt (); + if field_id = id then F.pp_print_string fmt field_var + else F.pp_print_string fmt "_") + fields; + F.pp_print_space fmt (); + F.pp_print_string fmt "=>"; + F.pp_print_space fmt (); + F.pp_print_string fmt field_var; + (* Close the box for the branch *) + F.pp_close_box fmt (); + + (* Close the box for the whole match *) + F.pp_close_box fmt (); + + (* Close the box for projector definition *) + F.pp_close_box fmt (); + (* Add breaks to insert new lines between definitions *) + F.pp_print_break fmt 0 0 + in + + FieldId.iteri extract_field_proj fields + (** Auxiliary function. Generate field projectors in Coq. @@ -1669,7 +1790,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) Sometimes we extract records as inductives in Coq: when this happens we have to define the field projectors afterwards. *) -let extract_type_decl_record_field_projectors (ctx : extraction_ctx) +let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = sanity_check __FILE__ __LINE__ (!backend = Coq) decl.meta; match decl.kind with @@ -1826,7 +1947,13 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx) let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = match !backend with - | FStar | Lean | HOL4 -> () + | FStar | HOL4 -> () + | Lean -> + if + not + (TypesUtils.type_decl_from_decl_id_is_tuple_struct + ctx.trans_ctx.type_ctx.type_infos decl.def_id) + then extract_type_decl_lean_record_field_projectors ctx fmt kind decl | Coq -> if not @@ -1834,7 +1961,7 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) ctx.trans_ctx.type_ctx.type_infos decl.def_id) then ( extract_type_decl_coq_arguments ctx fmt kind decl; - extract_type_decl_record_field_projectors ctx fmt kind decl) + extract_type_decl_coq_record_field_projectors ctx fmt kind decl) (** Extract the state type declaration. *) let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) -- cgit v1.2.3 From e660a4d575ba55bd23c64b5bd7b4e435be82d7ed Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 23 May 2024 10:58:47 +0200 Subject: Improve formatting of Lean struct projectors --- compiler/ExtractTypes.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 4272e7a9..8520b0fb 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1696,8 +1696,11 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) let extract_field_proj (field_id : FieldId.id) (_ : field) : unit = F.pp_print_space fmt (); - (* Box for the projector definition *) + (* Outer box for the projector definition *) F.pp_open_hvbox fmt 0; + (* Inner box for the projector definition *) + F.pp_open_hvbox fmt ctx.indent_incr; + (* Box for the [def ADT.proj ... :=] *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "def"; @@ -1775,7 +1778,8 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) (* Close the box for the whole match *) F.pp_close_box fmt (); - (* Close the box for projector definition *) + F.pp_close_box fmt (); + (* Close the outer box for projector definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 -- cgit v1.2.3 From 7238177f5c7cff15f924e13c01d5b3b4802daf77 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 23 May 2024 11:33:46 +0200 Subject: Do not expand field projector for recursive structs to a let binding in Lean --- compiler/SymbolicToPure.ml | 5 ----- 1 file changed, 5 deletions(-) (limited to 'compiler') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 6c925bcd..351f5cf2 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2902,14 +2902,9 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) - if the ADT is an enumeration (which must have exactly one branch) - if we forbid using field projectors. *) - let is_rec_def = - T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls - in let use_let_with_cons = is_enum || !Config.dont_use_field_projectors - (* TODO: for now, we don't have field projectors over recursive ADTs in Lean. *) - || (!Config.backend = Lean && is_rec_def) (* Also, there is a special case when the ADT is to be extracted as a tuple, because it is a structure with unnamed fields. Some backends like Lean have projectors for tuples (like so: `x.3`), but others -- cgit v1.2.3 From e76ef95ddda11d4220e1f0fd863b0df568de95bc Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Thu, 23 May 2024 16:41:54 +0200 Subject: Add simp, reducible attributes to generated Lean projectors --- compiler/ExtractTypes.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'compiler') diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 8520b0fb..70a4d000 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1701,6 +1701,16 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) (* Inner box for the projector definition *) F.pp_open_hvbox fmt ctx.indent_incr; + (* Box for the attributes *) + F.pp_open_vbox fmt 0; + (* Annotate the projectors with both simp and reducible. + The first one allows to automatically unfold when calling simp in proofs. + The second ensures that projectors will interact well with the unifier *) + F.pp_print_string fmt "@[simp, reducible]"; + F.pp_print_break fmt 0 0; + (* Close box for the attributes *) + F.pp_close_box fmt (); + (* Box for the [def ADT.proj ... :=] *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "def"; -- cgit v1.2.3 From 3b4139de5b9bcf5f43213330652ad01383e975d3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 24 May 2024 16:50:18 +0200 Subject: Factor out the code for Lean and Coq --- compiler/ExtractTypes.ml | 184 +++++++++++------------------------------------ 1 file changed, 41 insertions(+), 143 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 2fc0c117..cc0c351d 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -1666,15 +1666,15 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter) (** Auxiliary function. - Generate field projectors in Lean. + Generate field projectors for Lean and Coq. - Recursive structs are defined as inductives in Lean. + Recursive structs are defined as inductives in Lean and Coq. Field projectors allow to retrieve the facilities provided by Lean structures. *) -let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) +let extract_type_decl_record_field_projectors (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - sanity_check __FILE__ __LINE__ (!backend = Lean) decl.meta; + sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span; match decl.kind with | Opaque | Enum _ -> () | Struct fields -> @@ -1683,18 +1683,18 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) if is_rec then (* Add the type params *) let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params decl.meta decl.llbc_name decl.llbc_generics + ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics decl.generics ctx in (* Record_var will be the ADT argument to the projector *) - let ctx, record_var = ctx_add_var decl.meta "x" (VarId.of_int 0) ctx in + let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in (* Field_var will be the variable in the constructor that is returned by the projector *) - let ctx, field_var = ctx_add_var decl.meta "x" (VarId.of_int 1) ctx in + let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in (* Name of the ADT *) - let def_name = ctx_get_local_type decl.meta decl.def_id ctx in + let def_name = ctx_get_local_type decl.span decl.def_id ctx in (* Name of the ADT constructor. As we are in the struct case, we only have one constructor *) - let cons_name = ctx_get_struct decl.meta (TAdtId decl.def_id) ctx in + let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in let extract_field_proj (field_id : FieldId.id) (_ : field) : unit = F.pp_print_space fmt (); @@ -1703,33 +1703,40 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) (* Inner box for the projector definition *) F.pp_open_hvbox fmt ctx.indent_incr; - (* Box for the attributes *) - F.pp_open_vbox fmt 0; - (* Annotate the projectors with both simp and reducible. - The first one allows to automatically unfold when calling simp in proofs. - The second ensures that projectors will interact well with the unifier *) - F.pp_print_string fmt "@[simp, reducible]"; - F.pp_print_break fmt 0 0; - (* Close box for the attributes *) - F.pp_close_box fmt (); + (* For Lean: add some attributes *) + if !backend = Lean then ( + (* Box for the attributes *) + F.pp_open_vbox fmt 0; + (* Annotate the projectors with both simp and reducible. + The first one allows to automatically unfold when calling simp in proofs. + The second ensures that projectors will interact well with the unifier *) + F.pp_print_string fmt "@[simp, reducible]"; + F.pp_print_break fmt 0 0; + (* Close box for the attributes *) + F.pp_close_box fmt ()); (* Box for the [def ADT.proj ... :=] *) F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_string fmt "def"; + (match !backend with + | Lean -> F.pp_print_string fmt "def" + | Coq -> F.pp_print_string fmt "Definition" + | _ -> internal_error __FILE__ __LINE__ decl.span); F.pp_print_space fmt (); (* Print the function name. In Lean, the syntax ADT.proj will - allow us to call x.proj for any x of type ADT *) + allow us to call x.proj for any x of type ADT. In Coq, + we will have to introduce a notation for the projector. *) let field_name = - ctx_get_field decl.meta (TAdtId decl.def_id) field_id ctx + ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx in - F.pp_print_string fmt def_name; - F.pp_print_string fmt "."; + if !backend = Lean then ( + F.pp_print_string fmt def_name; + F.pp_print_string fmt "."); F.pp_print_string fmt field_name; (* Print the generics *) let as_implicits = true in - extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty + extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty ~as_implicits decl.generics type_params cg_params trait_clauses; (* Print the record parameter as "(x : ADT)" *) @@ -1787,115 +1794,11 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx) (* Close the box for the branch *) F.pp_close_box fmt (); - (* Close the box for the whole match *) - F.pp_close_box fmt (); - - F.pp_close_box fmt (); - (* Close the outer box for projector definition *) - F.pp_close_box fmt (); - (* Add breaks to insert new lines between definitions *) - F.pp_print_break fmt 0 0 - in - - FieldId.iteri extract_field_proj fields - -(** Auxiliary function. - - Generate field projectors in Coq. - - Sometimes we extract records as inductives in Coq: when this happens we - have to define the field projectors afterwards. - *) -let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx) - (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = - sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span; - match decl.kind with - | Opaque | Enum _ -> () - | Struct fields -> - (* Records are extracted as inductives only if they are recursive *) - let is_rec = decl_is_from_rec_group kind in - if is_rec then - (* Add the type params *) - let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics - decl.generics ctx - in - let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in - let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in - let def_name = ctx_get_local_type decl.span decl.def_id ctx in - let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in - let extract_field_proj (field_id : FieldId.id) (_ : field) : unit = - F.pp_print_space fmt (); - (* Outer box for the projector definition *) - F.pp_open_hvbox fmt 0; - (* Inner box for the projector definition *) - F.pp_open_hvbox fmt ctx.indent_incr; - (* Open a box for the [Definition PROJ ... :=] *) - F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_string fmt "Definition"; - F.pp_print_space fmt (); - let field_name = - ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx - in - F.pp_print_string fmt field_name; - (* Print the generics *) - let as_implicits = true in - extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty - ~as_implicits decl.generics type_params cg_params trait_clauses; - (* Print the record parameter *) - F.pp_print_space fmt (); - F.pp_print_string fmt "("; - F.pp_print_string fmt record_var; - F.pp_print_space fmt (); - F.pp_print_string fmt ":"; - F.pp_print_space fmt (); - F.pp_print_string fmt def_name; - List.iter - (fun p -> - F.pp_print_space fmt (); - F.pp_print_string fmt p) - type_params; - F.pp_print_string fmt ")"; - (* *) - F.pp_print_space fmt (); - F.pp_print_string fmt ":="; - (* Close the box for the [Definition PROJ ... :=] *) - F.pp_close_box fmt (); - F.pp_print_space fmt (); - (* Open a box for the whole match *) - F.pp_open_hvbox fmt 0; - (* Open a box for the [match ... with] *) - F.pp_open_hovbox fmt ctx.indent_incr; - F.pp_print_string fmt "match"; - F.pp_print_space fmt (); - F.pp_print_string fmt record_var; - F.pp_print_space fmt (); - F.pp_print_string fmt "with"; - (* Close the box for the [match ... with] *) - F.pp_close_box fmt (); - - (* Open a box for the branch *) - F.pp_open_hovbox fmt ctx.indent_incr; - (* Print the match branch *) - F.pp_print_space fmt (); - F.pp_print_string fmt "|"; - F.pp_print_space fmt (); - F.pp_print_string fmt cons_name; - FieldId.iteri - (fun id _ -> - F.pp_print_space fmt (); - if field_id = id then F.pp_print_string fmt field_var - else F.pp_print_string fmt "_") - fields; - F.pp_print_space fmt (); - F.pp_print_string fmt "=>"; - F.pp_print_space fmt (); - F.pp_print_string fmt field_var; - (* Close the box for the branch *) - F.pp_close_box fmt (); (* Print the [end] *) - F.pp_print_space fmt (); - F.pp_print_string fmt "end"; + if !backend = Coq then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "end"); + (* Close the box for the whole match *) F.pp_close_box fmt (); (* Close the inner box projector *) @@ -1904,12 +1807,13 @@ let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx) if !backend = Coq then ( F.pp_print_cut fmt (); F.pp_print_string fmt "."); - (* Close the outer box projector *) + (* Close the outer box for projector definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) F.pp_print_break fmt 0 0 in + (* Only for Coq: we need to define a notation for the projector *) let extract_proj_notation (field_id : FieldId.id) (_ : field) : unit = F.pp_print_space fmt (); (* Outer box for the projector definition *) @@ -1950,7 +1854,7 @@ let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx) let extract_field_proj_and_notation (field_id : FieldId.id) (field : field) : unit = extract_field_proj field_id field; - extract_proj_notation field_id field + if !backend = Coq then extract_proj_notation field_id field in FieldId.iteri extract_field_proj_and_notation fields @@ -1964,20 +1868,14 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit = match !backend with | FStar | HOL4 -> () - | Lean -> - if - not - (TypesUtils.type_decl_from_decl_id_is_tuple_struct - ctx.trans_ctx.type_ctx.type_infos decl.def_id) - then extract_type_decl_lean_record_field_projectors ctx fmt kind decl - | Coq -> + | Lean | Coq -> if not (TypesUtils.type_decl_from_decl_id_is_tuple_struct ctx.trans_ctx.type_ctx.type_infos decl.def_id) then ( - extract_type_decl_coq_arguments ctx fmt kind decl; - extract_type_decl_coq_record_field_projectors ctx fmt kind decl) + if !backend = Coq then extract_type_decl_coq_arguments ctx fmt kind decl; + extract_type_decl_record_field_projectors ctx fmt kind decl) (** Extract the state type declaration. *) let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx) -- cgit v1.2.3 From 2b5186fef6932995626790af241eaed4e7cc02ae Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 28 May 2024 18:04:38 +0200 Subject: Fix a bug in SymbolicToPure.translate_loop --- compiler/SymbolicToPure.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'compiler') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index d6d2e018..cc203040 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3529,10 +3529,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ] else output in - let output = - if effect_info.can_fail && inputs <> [] then mk_result_ty output - else output - in + let output = if effect_info.can_fail then mk_result_ty output else output in (back_info, output) in -- cgit v1.2.3 From b5eac0384818e1f51fbfd900ab580514e851b0ca Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 28 May 2024 18:48:56 +0200 Subject: Fix an issue with some names being ignored when generating unique variable names --- compiler/ExtractBase.ml | 40 +++++++++++++++++++--------------------- 1 file changed, 19 insertions(+), 21 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index ab7eb50c..815e228f 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -351,13 +351,13 @@ let unsafe_names_map_add (id : id) (name : string) (nm : unsafe_names_map) : [append]: function to append an index to a string *) -let basename_to_unique (names_set : StringSet.t) +let basename_to_unique_aux (collision : string -> bool) (append : string -> int -> string) (basename : string) : string = let rec gen (i : int) : string = let s = append basename i in - if StringSet.mem s names_set then gen (i + 1) else s + if collision s then gen (i + 1) else s in - if StringSet.mem basename names_set then gen 1 else basename + if collision basename then gen 1 else basename type names_maps = { names_map : names_map; @@ -1841,13 +1841,22 @@ let trait_self_clause_basename = "self_clause" let name_append_index (basename : string) (i : int) : string = basename ^ string_of_int i +let basename_to_unique (ctx : extraction_ctx) (name : string) = + let collision s = + (* Note that we ignore the "unsafe" names which contain in particular + field names: we want to allow using field names for variables if + the backend allows such collisions *) + StringSet.mem s ctx.names_maps.names_map.names_set + || StringSet.mem s ctx.names_maps.strict_names_map.names_set + in + + basename_to_unique_aux collision name_append_index name + (** Generate a unique type variable name and add it to the context *) let ctx_add_type_var (span : Meta.span) (basename : string) (id : TypeVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx_compute_type_var_basename ctx basename in - let name = - basename_to_unique ctx.names_maps.names_map.names_set name_append_index name - in + let name = basename_to_unique ctx name in let ctx = ctx_add span (TypeVarId id) name ctx in (ctx, name) @@ -1856,9 +1865,7 @@ let ctx_add_const_generic_var (span : Meta.span) (basename : string) (id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string = let name = ctx_compute_const_generic_var_basename ctx basename in - let name = - basename_to_unique ctx.names_maps.names_map.names_set name_append_index name - in + let name = basename_to_unique ctx name in let ctx = ctx_add span (ConstGenericVarId id) name ctx in (ctx, name) @@ -1872,10 +1879,7 @@ let ctx_add_type_vars (span : Meta.span) (vars : (string * TypeVarId.id) list) (** Generate a unique variable name and add it to the context *) let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id) (ctx : extraction_ctx) : extraction_ctx * string = - let name = - basename_to_unique ctx.names_maps.names_map.names_set name_append_index - basename - in + let name = basename_to_unique ctx basename in let ctx = ctx_add span (VarId id) name ctx in (ctx, name) @@ -1883,20 +1887,14 @@ let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id) let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) : extraction_ctx * string = let basename = trait_self_clause_basename in - let name = - basename_to_unique ctx.names_maps.names_map.names_set name_append_index - basename - in + let name = basename_to_unique ctx basename in let ctx = ctx_add span TraitSelfClauseId name ctx in (ctx, name) (** Generate a unique trait clause name and add it to the context *) let ctx_add_local_trait_clause (span : Meta.span) (basename : string) (id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string = - let name = - basename_to_unique ctx.names_maps.names_map.names_set name_append_index - basename - in + let name = basename_to_unique ctx basename in let ctx = ctx_add span (LocalTraitClauseId id) name ctx in (ctx, name) -- cgit v1.2.3 From 5330a6f728add1525854ad4cedd86b8e1d3a1fa7 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 29 May 2024 01:00:38 +0200 Subject: Factor out code in ExtractBuiltin.ml --- compiler/ExtractBuiltin.ml | 284 +++++++++++++++++++-------------------------- compiler/FunsAnalysis.ml | 3 +- 2 files changed, 124 insertions(+), 163 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index a7ab6da0..ff936d2f 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -233,7 +233,12 @@ let mk_builtin_types_map () = let builtin_types_map = mk_memoized mk_builtin_types_map -type builtin_fun_info = { extract_name : string } [@@deriving show] +type builtin_fun_info = { + extract_name : string; + can_fail : bool; + stateful : bool; +} +[@@deriving show] let int_and_smaller_list : (string * string) list = let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in @@ -257,16 +262,17 @@ let int_and_smaller_list : (string * string) list = ] @ compute_pairs uint_names @ compute_pairs int_names -(** The assumed functions. +(** The builtin functions. The optional list of booleans is filtering information for the type parameters. For instance, in the case of the `Vec` functions, there is a type parameter for the allocator to use, which we want to filter. *) -let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = +let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list = (* Small utility *) - let mk_fun (rust_name : string) (extract_name : string option) - (filter : bool list option) : + let mk_fun (rust_name : string) ?(filter : bool list option = None) + ?(can_fail = true) ?(stateful = false) + ?(extract_name : string option = None) () : pattern * bool list option * builtin_fun_info = let rust_name = try parse_pattern rust_name @@ -279,124 +285,151 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = | Some name -> split_on_separator name in let basename = flatten_name extract_name in - let f = { extract_name = basename } in + let f = { extract_name = basename; can_fail; stateful } in (rust_name, filter, f) in let mk_scalar_fun (rust_name : string -> string) - (extract_name : string -> string) : + (extract_name : string -> string) ?(can_fail = true) () : (pattern * bool list option * builtin_fun_info) list = List.map - (fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None) + (fun ty -> + mk_fun (rust_name ty) + ~extract_name:(Some (extract_name ty)) + ~can_fail ()) all_int_names in [ - mk_fun "core::mem::replace" None None; + mk_fun "core::mem::replace" ~can_fail:false (); + mk_fun "core::mem::take" ~can_fail:false (); mk_fun "core::slice::{[@T]}::len" - (Some (backend_choice "slice::len" "Slice::len")) - None; + ~extract_name:(Some (backend_choice "slice::len" "Slice::len")) + ~can_fail:false (); mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new" - (Some "alloc::vec::Vec::new") None; - mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None - (Some [ true; false ]); - mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" None - (Some [ true; false ]); - mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None - (Some [ true; false ]); + ~extract_name:(Some "alloc::vec::Vec::new") ~can_fail:false (); + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" + ~filter:(Some [ true; false ]) + (); + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" + ~filter:(Some [ true; false ]) + (); + mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" + ~filter:(Some [ true; false ]) + ~can_fail:false (); mk_fun "alloc::vec::{core::ops::index::Index, \ @I>}::index" - (Some "alloc.vec.Vec.index") - (Some [ true; true; false ]); + ~extract_name:(Some "alloc.vec.Vec.index") + ~filter:(Some [ true; true; false ]) + (); mk_fun "alloc::vec::{core::ops::index::IndexMut, \ @I>}::index_mut" - (Some "alloc.vec.Vec.index_mut") - (Some [ true; true; false ]); + ~extract_name:(Some "alloc.vec.Vec.index_mut") + ~filter:(Some [ true; true; false ]) + (); mk_fun "alloc::boxed::{core::ops::deref::Deref>}::deref" - (Some "alloc.boxed.Box.deref") - (Some [ true; false ]); + ~extract_name:(Some "alloc.boxed.Box.deref") + ~filter:(Some [ true; false ]) + (); mk_fun "alloc::boxed::{core::ops::deref::DerefMut>}::deref_mut" - (Some "alloc.boxed.Box.deref_mut") - (Some [ true; false ]); + ~extract_name:(Some "alloc.boxed.Box.deref_mut") + ~filter:(Some [ true; false ]) + (); mk_fun "core::slice::index::{core::ops::index::Index<[@T], @I>}::index" - (Some "core.slice.index.Slice.index") None; + ~extract_name:(Some "core.slice.index.Slice.index") (); mk_fun "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut" - (Some "core.slice.index.Slice.index_mut") None; + ~extract_name:(Some "core.slice.index.Slice.index_mut") (); mk_fun "core::array::{core::ops::index::Index<[@T; @N], @I>}::index" - (Some "core.array.Array.index") None; + ~extract_name:(Some "core.array.Array.index") (); mk_fun "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut" - (Some "core.array.Array.index_mut") None; + ~extract_name:(Some "core.array.Array.index_mut") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex, \ [@T]>}::get" - (Some "core::slice::index::RangeUsize::get") None; + ~extract_name:(Some "core::slice::index::RangeUsize::get") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex, \ [@T]>}::get_mut" - (Some "core::slice::index::RangeUsize::get_mut") None; + ~extract_name:(Some "core::slice::index::RangeUsize::get_mut") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex, \ [@T]>}::index" - (Some "core::slice::index::RangeUsize::index") None; + ~extract_name:(Some "core::slice::index::RangeUsize::index") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex, \ [@T]>}::index_mut" - (Some "core::slice::index::RangeUsize::index_mut") None; + ~extract_name:(Some "core::slice::index::RangeUsize::index_mut") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex, \ [@T]>}::get_unchecked" - (Some "core::slice::index::RangeUsize::get_unchecked") None; + ~extract_name:(Some "core::slice::index::RangeUsize::get_unchecked") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex, \ [@T]>}::get_unchecked_mut" - (Some "core::slice::index::RangeUsize::get_unchecked_mut") None; + ~extract_name:(Some "core::slice::index::RangeUsize::get_unchecked_mut") + (); mk_fun "core::slice::index::{core::slice::index::SliceIndex}::get" - None None; + (); mk_fun "core::slice::index::{core::slice::index::SliceIndex}::get_mut" - None None; + (); mk_fun "core::slice::index::{core::slice::index::SliceIndex}::get_unchecked" - None None; + (); mk_fun "core::slice::index::{core::slice::index::SliceIndex}::get_unchecked_mut" - None None; + (); mk_fun "core::slice::index::{core::slice::index::SliceIndex}::index" - (Some "core_slice_index_Slice_index") None; + ~extract_name:(Some "core_slice_index_Slice_index") (); mk_fun "core::slice::index::{core::slice::index::SliceIndex}::index_mut" - (Some "core_slice_index_Slice_index_mut") None; - mk_fun "alloc::slice::{[@T]}::to_vec" (Some "alloc.slice.Slice.to_vec") None; + ~extract_name:(Some "core_slice_index_Slice_index_mut") (); + mk_fun "alloc::slice::{[@T]}::to_vec" + ~extract_name:(Some "alloc.slice.Slice.to_vec") (); mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity" - (Some "alloc.vec.Vec.with_capacity") None; - mk_fun "core::slice::{[@T]}::reverse" (Some "core.slice.Slice.reverse") None; + ~extract_name:(Some "alloc.vec.Vec.with_capacity") ~can_fail:false (); + mk_fun "core::slice::{[@T]}::reverse" + ~extract_name:(Some "core.slice.Slice.reverse") ~can_fail:false (); mk_fun "alloc::vec::{core::ops::deref::Deref>}::deref" - (Some "alloc.vec.DerefVec.deref") - (Some [ true; false ]); + ~extract_name:(Some "alloc.vec.DerefVec.deref") + ~filter:(Some [ true; false ]) + ~can_fail:false (); mk_fun "alloc::vec::{core::ops::deref::DerefMut>}::deref_mut" - (Some "alloc.vec.DerefMutVec.deref_mut") - (Some [ true; false ]); + ~extract_name:(Some "alloc.vec.DerefMutVec.deref_mut") + ~filter:(Some [ true; false ]) + (); mk_fun "core::option::{core::option::Option<@T>}::unwrap" - (Some "core.option.Option.unwrap") None; + ~extract_name:(Some "core.option.Option.unwrap") (); ] + @ List.flatten + (List.map + (fun int_name -> + List.map + (fun op -> + mk_fun + ("core::num::" ^ "{" ^ int_name ^ "}::" ^ op) + ~can_fail:false ()) + [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ]) + all_int_names) @ List.flatten (List.map (fun op -> mk_scalar_fun (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op) (fun ty -> - StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)) + StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op) + ~can_fail:false ()) [ "add"; "sub"; "mul"; "div"; "rem" ]) (* From *) @ mk_scalar_fun @@ -406,44 +439,50 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = "core.convert.num.From" ^ StringUtils.capitalize_first_letter ty ^ "Bool.from") + ~can_fail:false () (* From *) @ List.map (fun (big, small) -> mk_fun ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small ^ ">}::from") - (Some - ("core.convert.num.From" - ^ StringUtils.capitalize_first_letter big - ^ StringUtils.capitalize_first_letter small - ^ ".from")) - None) + ~extract_name: + (Some + ("core.convert.num.From" + ^ StringUtils.capitalize_first_letter big + ^ StringUtils.capitalize_first_letter small + ^ ".from")) + ~can_fail:false ()) int_and_smaller_list (* Leading zeros *) @ mk_scalar_fun (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") (fun ty -> "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros") + ~can_fail:false () (* to_le_bytes *) @ mk_scalar_fun (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes") (fun ty -> "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes") + ~can_fail:false () (* to_be_bytes *) @ mk_scalar_fun (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes") (fun ty -> "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes") + ~can_fail:false () (* Clone *) @ [ mk_fun "core::clone::impls::{core::clone::Clone}::clone" - (Some "core.clone.CloneBool.clone") None; + ~extract_name:(Some "core.clone.CloneBool.clone") ~can_fail:false (); ] (* Clone *) @ mk_scalar_fun (fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone") (fun ty -> "core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone") + ~can_fail:false () (* Lean-only definitions *) @ mk_lean_only [ @@ -451,15 +490,19 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list = By construction, we cannot write down that parameter in the output in this list *) - mk_fun "core::mem::swap" None None; + mk_fun "core::mem::swap" ~can_fail:false (); mk_fun "core::option::{core::option::Option<@T>}::take" - (Some (backend_choice "" "Option::take")) - None; + ~extract_name:(Some (backend_choice "" "Option::take")) + ~can_fail:false (); mk_fun "core::option::{core::option::Option<@T>}::is_none" - (Some (backend_choice "" "Option::isNone")) - (Some [ false ]); + ~extract_name:(Some (backend_choice "" "Option::isNone")) + ~filter:(Some [ false ]) ~can_fail:false (); ] +let builtin_funs : unit -> (pattern * bool list option * builtin_fun_info) list + = + mk_memoized mk_builtin_funs + let mk_builtin_funs_map () = let m = NameMatcherMap.of_list @@ -475,106 +518,20 @@ let builtin_funs_map = mk_memoized mk_builtin_funs_map type effect_info = { can_fail : bool; stateful : bool } -let builtin_fun_effects = - let int_ops = - [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ] - in - let int_funs = - List.map - (fun int_name -> - List.map (fun op -> "core::num::" ^ "{" ^ int_name ^ "}::" ^ op) int_ops) - all_int_names - @ List.map - (fun op -> - List.map - (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op) - all_int_names) - [ "add"; "sub"; "mul"; "div"; "rem" ] - (* From *) - @ [ - List.map - (fun int_name -> - "core::convert::num::{core::convert::From<" ^ int_name - ^ ", bool>}::from") - all_int_names; - ] - (* From *) - @ [ - List.map - (fun (big, small) -> - "core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small - ^ ">}::from") - int_and_smaller_list; - ] - (* Leading zeros *) - @ [ - List.map - (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros") - all_int_names; - ] - (* to_{le,be}_bytes *) - @ List.map - (fun ty -> - let pre = "core::num::{" ^ ty ^ "}::" in - [ pre ^ "to_le_bytes"; pre ^ "to_be_bytes" ]) - all_int_names - (* clone *) - @ [ - List.map - (fun ty -> - "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone") - all_int_names; - ] +let mk_builtin_fun_effects () : (pattern * effect_info) list = + let builtin_funs : (pattern * bool list option * builtin_fun_info) list = + builtin_funs () in + List.map + (fun ((pattern, _, info) : _ * _ * builtin_fun_info) -> + let info = { can_fail = info.can_fail; stateful = info.stateful } in + (pattern, info)) + builtin_funs - let int_funs = List.concat int_funs in - let no_fail_no_state_funs = - [ - (* TODO: redundancy with the funs information above *) - "core::slice::{[@T]}::len"; - "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"; - "alloc::vec::{alloc::vec::Vec<@T, @A>}::len"; - "core::mem::replace"; - "core::mem::take"; - "core::clone::impls::{core::clone::Clone}::clone"; - "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity"; - "core::slice::{[@T]}::reverse"; - "alloc::vec::{core::ops::deref::Deref>}::deref"; - ] - @ int_funs - @ mk_lean_only - [ - "core::mem::swap"; - "core::option::{core::option::Option<@T>}::take"; - "core::option::{core::option::Option<@T>}::is_none"; - ] - in - let no_fail_no_state_funs = - List.map - (fun n -> (n, { can_fail = false; stateful = false })) - no_fail_no_state_funs - in - (* TODO: all the functions registered in the [builtin_funs] above should - be considered as not using a state. There is a lot of redundancy - right now. *) - let no_state_funs = - [ - "alloc::vec::{alloc::vec::Vec<@T, @A>}::push"; - "alloc::vec::{core::ops::index::Index, \ - @I>}::index"; - "alloc::vec::{core::ops::index::IndexMut, \ - @I>}::index_mut"; - "core::option::{core::option::Option<@T>}::unwrap"; - ] - in - let no_state_funs = - List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs - in - no_fail_no_state_funs @ no_state_funs +let mk_builtin_fun_effects_map () = + NameMatcherMap.of_list (mk_builtin_fun_effects ()) -let builtin_fun_effects_map = - NameMatcherMap.of_list - (List.map (fun (n, x) -> (parse_pattern n, x)) builtin_fun_effects) +let builtin_fun_effects_map = mk_memoized mk_builtin_fun_effects_map type builtin_trait_decl_info = { rust_name : pattern; @@ -632,13 +589,16 @@ let builtin_trait_decls_info () = if !record_fields_short_names then item_name else extract_name ^ "_" ^ item_name in - let fwd = { extract_name = basename } in + let fwd = + { extract_name = basename; can_fail = true; stateful = false } + in (item_name, fwd) in List.map mk_method methods | Some methods -> List.map - (fun (item_name, extract_name) -> (item_name, { extract_name })) + (fun (item_name, extract_name) -> + (item_name, { extract_name; can_fail = true; stateful = false })) methods in { diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index a11eab87..eadd8f8a 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -74,7 +74,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) way. *) let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option = let open ExtractBuiltin in - NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map + NameMatcherMap.find_opt name_matcher_ctx f.name + (builtin_fun_effects_map ()) in (* JP: Why not use a reduce visitor here with a tuple of the values to be -- cgit v1.2.3 From ec039b63748c2a95f89c0538a843e18d3a51cdf3 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 3 Jun 2024 16:53:09 +0200 Subject: feat: basic handling for `RValue::Len`, following AeneasVerif/charon#209 --- compiler/FunsAnalysis.ml | 4 +++- compiler/InterpreterExpressions.ml | 1 + compiler/InterpreterStatements.ml | 1 + compiler/InterpreterUtils.ml | 2 +- 4 files changed, 6 insertions(+), 2 deletions(-) (limited to 'compiler') diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index eadd8f8a..815c470f 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -103,7 +103,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) method! visit_rvalue _env rv = match rv with - | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> () + | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _ + -> + () | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail | BinaryOp (bop, _, _) -> can_fail := binop_can_fail bop || !can_fail diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 2223897c..56c0ab5f 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -816,6 +816,7 @@ let eval_rvalue_not_global (config : config) (span : Meta.span) "Unreachable: discriminant reads should have been eliminated from the \ AST" | Global _ -> craise __FILE__ __LINE__ span "Unreachable" + | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len" let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun = fun ctx -> diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index c6a65757..c60be905 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -950,6 +950,7 @@ let rec eval_statement (config : config) (st : statement) : stl_cm_fun = let cc = match rvalue with | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable" + | Len _ -> craise __FILE__ __LINE__ st.span "Unhandled Len" | Use _ | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow)) | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ -> diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 653a0e24..f3f12906 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -291,7 +291,7 @@ let rvalue_get_place (rv : rvalue) : place option = match rv with | Use (Copy p | Move p) -> Some p | Use (Constant _) -> None - | RvRef (p, _) -> Some p + | Len (p, _, _) | RvRef (p, _) -> Some p | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None (** See {!ValuesUtils.symbolic_value_has_borrows} *) -- cgit v1.2.3