diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Contexts.ml | 12 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 8 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 6 | ||||
| -rw-r--r-- | compiler/Print.ml | 22 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 37 |
5 files changed, 38 insertions, 47 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml index 9d22a643..df77959e 100644 --- a/compiler/Contexts.ml +++ b/compiler/Contexts.ml @@ -333,9 +333,21 @@ type eval_ctx = { } [@@deriving show] +let lookup_type_var_opt (ctx : eval_ctx) (vid : TypeVarId.id) : type_var option + = + if TypeVarId.to_int vid < List.length ctx.type_vars then + Some (TypeVarId.nth ctx.type_vars vid) + else None + let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = TypeVarId.nth ctx.type_vars vid +let lookup_const_generic_var_opt (ctx : eval_ctx) (vid : ConstGenericVarId.id) : + const_generic_var option = + if ConstGenericVarId.to_int vid < List.length ctx.const_generic_vars then + Some (ConstGenericVarId.nth ctx.const_generic_vars vid) + else None + let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) : const_generic_var = ConstGenericVarId.nth ctx.const_generic_vars vid diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 1ea16e58..97fb80f4 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -1198,7 +1198,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) log#ldebug (lazy ("trait method call:\n- call: " ^ call_to_string ctx call - ^ "\n- method name: " ^ method_name ^ "\n- generics:\n" + ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ egeneric_args_to_string ctx call.generics ^ "\n- trait and method generics:\n" ^ egeneric_args_to_string ctx @@ -1273,7 +1273,10 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (lazy ("provided method call:" ^ "\n- method name: " ^ method_name ^ "\n- generics:\n" - ^ egeneric_args_to_string ctx generics)); + ^ egeneric_args_to_string ctx generics + ^ "\n- parent params info: " + ^ Print.option_to_string A.show_params_info + method_def.signature.parent_params_info)); let tr_self = T.TraitRef (etrait_ref_no_regions_to_gr_trait_ref trait_ref) in @@ -1303,6 +1306,7 @@ and eval_transparent_function_call_symbolic (config : C.config) (call : A.call) (List.append trait_decl.required_methods provided) in let method_def = C.ctx_lookup_fun_decl ctx method_id in + log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) let tr_self = T.TraitRef trait_ref in let tr_self = diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 8a7e8c52..8525be29 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -39,8 +39,12 @@ let typed_avalue_to_string = PA.typed_avalue_to_string let place_to_string = PA.place_to_string let operand_to_string = PA.operand_to_string let egeneric_args_to_string = PA.egeneric_args_to_string +let fun_decl_to_string = PA.fun_decl_to_string let call_to_string = PA.call_to_string -let trait_impl_to_string = PA.trait_impl_to_string + +let trait_impl_to_string ctx = + PA.trait_impl_to_string { ctx with type_vars = []; const_generic_vars = [] } + let statement_to_string ctx = PA.statement_to_string ctx "" " " let statement_to_string_with_tab ctx = PA.statement_to_string ctx " " " " let env_elem_to_string ctx = PA.env_elem_to_string ctx "" " " diff --git a/compiler/Print.ml b/compiler/Print.ml index 55aa0c53..92743bc1 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -479,19 +479,23 @@ module Contexts = struct PV.value_to_rtype_formatter fmt let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter = - (* We shouldn't use rvar_to_string *) - let rvar_to_string _r = - raise (Failure "Unexpected use of rvar_to_string") + let rvar_to_string r = + (* In theory we shouldn't use rvar_to_string, but it can happen + when printing definitions for instance... *) + T.RegionVarId.to_string r in let r_to_string r = PT.region_id_to_string r in let type_var_id_to_string vid = - let v = C.lookup_type_var ctx vid in - v.name + (* The context may be invalid *) + match C.lookup_type_var_opt ctx vid with + | None -> T.TypeVarId.to_string vid + | Some v -> v.name in let const_generic_var_id_to_string vid = - let v = C.lookup_const_generic_var ctx vid in - v.name + match C.lookup_const_generic_var_opt ctx vid with + | None -> T.ConstGenericVarId.to_string vid + | Some v -> v.name in let type_decl_id_to_string def_id = let def = C.ctx_lookup_type_decl ctx def_id in @@ -702,6 +706,10 @@ module EvalCtxLlbcAst = struct let fmt = PC.eval_ctx_to_ast_formatter ctx in PA.call_to_string fmt "" call + let fun_decl_to_string (ctx : C.eval_ctx) (f : A.fun_decl) : string = + let fmt = PC.eval_ctx_to_ast_formatter ctx in + PA.fun_decl_to_string fmt "" " " f + let statement_to_string (ctx : C.eval_ctx) (indent : string) (indent_incr : string) (e : A.statement) : string = let fmt = PC.eval_ctx_to_ast_formatter ctx in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 1da0521d..4c5b99c3 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -346,43 +346,6 @@ let bs_ctx_lookup_local_function_sig (def_id : A.FunDeclId.id) let id = (A.Regular def_id, back_id) in (RegularFunIdNotLoopMap.find id ctx.fun_context.fun_sigs).sg -let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call) - (args : texpression list) (ctx : bs_ctx) : bs_ctx = - let calls = ctx.calls in - assert (not (V.FunCallId.Map.mem call_id calls)); - let info = - { forward; forward_inputs = args; backwards = T.RegionGroupId.Map.empty } - in - let calls = V.FunCallId.Map.add call_id info calls in - { ctx with calls } - -(** [back_args]: the *additional* list of inputs received by the backward function *) -let bs_ctx_register_backward_call (abs : V.abs) (call_id : V.FunCallId.id) - (back_id : T.RegionGroupId.id) (back_args : texpression list) (ctx : bs_ctx) - : bs_ctx * fun_or_op_id = - (* Insert the abstraction in the call informations *) - let info = V.FunCallId.Map.find call_id ctx.calls in - assert (not (T.RegionGroupId.Map.mem back_id info.backwards)); - let backwards = - T.RegionGroupId.Map.add back_id (abs, back_args) info.backwards - in - let info = { info with backwards } in - let calls = V.FunCallId.Map.add call_id info ctx.calls in - (* Insert the abstraction in the abstractions map *) - let abstractions = ctx.abstractions in - assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions)); - let abstractions = - V.AbstractionId.Map.add abs.abs_id (abs, back_args) abstractions - in - (* Retrieve the fun_id *) - let fun_id = - match info.forward.call_id with - | S.Fun (fid, _) -> Fun (FromLlbc (fid, None, Some back_id)) - | S.Unop _ | S.Binop _ -> raise (Failure "Unreachable") - in - (* Update the context and return *) - ({ ctx with calls; abstractions }, fun_id) - (* Some generic translation functions (we need to translate different "flavours" of types: sty, forward types, backward types, etc.) *) let rec translate_generic_args (translate_ty : 'r T.ty -> ty) |