diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimOfJson.ml | 2 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 10 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 18 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | src/Print.ml | 5 | ||||
| -rw-r--r-- | src/PrintPure.ml | 3 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 170 | ||||
| -rw-r--r-- | src/main.ml | 2 |
8 files changed, 124 insertions, 88 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index a1d5faaa..c7bc4ce8 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -366,7 +366,7 @@ let rec operand_constant_value_of_json (js : json) : (E.operand_constant_value, string) result = combine_error_msgs js "operand_constant_value_of_json" (match js with - | `Assoc [ ("ConstantValue", cv) ] -> + | `Assoc [ ("ConstantValue", `List [ cv ]) ] -> let* cv = constant_value_of_json cv in Ok (E.ConstantValue cv) | `Assoc [ ("ConstantAdt", `List [ variant_id; field_values ]) ] -> diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index db09b316..aecd6c68 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -95,7 +95,7 @@ let fstar_keywords = List.concat [ named_unops; named_binops; misc ] let fstar_assumed_adts : (assumed_ty * string) list = - [ (Result, "result"); (Option, "option") ] + [ (Result, "result"); (Option, "option"); (Vec, "vec") ] let fstar_assumed_structs : (assumed_ty * string) list = [] @@ -397,7 +397,13 @@ let extract_type_def_register_names (ctx : extraction_ctx) (def : type_def) : let ctx = match def.kind with | Struct fields -> - fst (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx) + (* Add the fields *) + let ctx = + fst + (ctx_add_fields def (FieldId.mapi (fun id f -> (id, f)) fields) ctx) + in + (* Add the constructor name *) + fst (ctx_add_struct def ctx) | Enum variants -> fst (ctx_add_variants def diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 17e74ad3..9e4466b8 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -75,16 +75,26 @@ let rec operand_constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) (cv : E.operand_constant_value) : V.typed_value = (* Check the type while converting - we actually need some information * contained in the type *) + log#ldebug + (lazy + ("operand_constant_value_to_typed_value:" ^ "\n- ty: " + ^ ety_to_string ctx ty ^ "\n- cv: " + ^ operand_constant_value_to_string ctx cv)); match (ty, cv) with (* Adt *) - | ( T.Adt (T.AdtId def_id, region_params, type_params), + | ( T.Adt (adt_id, region_params, type_params), ConstantAdt (variant_id, field_values) ) -> assert (region_params = []); (* Compute the types of the fields *) - let def = C.ctx_lookup_type_def ctx def_id in - assert (def.region_params = []); let field_tys = - Subst.type_def_get_instantiated_field_etypes def variant_id type_params + match adt_id with + | T.AdtId def_id -> + let def = C.ctx_lookup_type_def ctx def_id in + assert (def.region_params = []); + Subst.type_def_get_instantiated_field_etypes def variant_id + type_params + | T.Tuple -> type_params + | T.Assumed _ -> failwith "Unreachable" in (* Compute the field values *) let field_values = diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 20657945..bbdd038f 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -33,6 +33,8 @@ let typed_value_to_string = PA.typed_value_to_string let typed_avalue_to_string = PA.typed_avalue_to_string +let operand_constant_value_to_string = PA.operand_constant_value_to_string + let place_to_string = PA.place_to_string let operand_to_string = PA.operand_to_string diff --git a/src/Print.ml b/src/Print.ml index b31be6ae..2db92d41 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -1142,6 +1142,11 @@ module EvalCtxCfimAst = struct let fmt = PC.eval_ctx_to_ctx_formatter ctx in PV.typed_avalue_to_string fmt v + let operand_constant_value_to_string (ctx : C.eval_ctx) + (cv : E.operand_constant_value) : string = + let fmt = PA.eval_ctx_to_ast_formatter ctx in + PA.operand_constant_value_to_string fmt cv + let place_to_string (ctx : C.eval_ctx) (op : E.place) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.place_to_string fmt op diff --git a/src/PrintPure.ml b/src/PrintPure.ml index f0e5df77..cf865a54 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -129,7 +129,8 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string = match id with | AdtId id -> fmt.type_def_id_to_string id | Tuple -> "" - | Assumed aty -> ( match aty with Result -> "Result") + | Assumed aty -> ( + match aty with Result -> "Result" | Option -> "Option" | Vec -> "Vec") let rec ty_to_string (fmt : type_formatter) (ty : ty) : string = match ty with diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 518e0a7d..04d65423 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -287,92 +287,98 @@ type extraction_ctx = { functions, etc. *) +(** Debugging function *) +let id_to_string (id : id) (ctx : extraction_ctx) : string = + let fun_defs = ctx.trans_ctx.fun_context.fun_defs in + let type_defs = ctx.trans_ctx.type_context.type_defs in + (* TODO: factorize the pretty-printing with what is in PrintPure *) + let get_type_name (id : type_id) : string = + match id with + | AdtId id -> + let def = TypeDefId.Map.find id type_defs in + Print.name_to_string def.name + | Assumed aty -> show_assumed_ty aty + | Tuple -> failwith "Unreachable" + in + match id with + | FunId (fid, rg_id) -> + let fun_name = + match fid with + | A.Local fid -> + Print.name_to_string (FunDefId.Map.find fid fun_defs).name + | A.Assumed aid -> A.show_assumed_fun_id aid + in + let fun_kind = + match rg_id with + | None -> "forward" + | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id + in + "fun name (" ^ fun_kind ^ "): " ^ fun_name + | TypeId id -> "type name: " ^ get_type_name id + | StructId id -> "struct constructor of: " ^ get_type_name id + | VariantId (id, variant_id) -> + let variant_name = + match id with + | Tuple -> failwith "Unreachable" + | Assumed Result -> + if variant_id = result_return_id then "@result::Return" + else if variant_id = result_fail_id then "@result::Fail" + else failwith "Unreachable" + | Assumed Option -> + if variant_id = option_some_id then "@option::Some" + else if variant_id = option_none_id then "@option::None" + else failwith "Unreachable" + | Assumed Vec -> failwith "Unreachable" + | AdtId id -> ( + let def = TypeDefId.Map.find id type_defs in + match def.kind with + | Struct _ -> failwith "Unreachable" + | Enum variants -> + let variant = VariantId.nth variants variant_id in + Print.name_to_string def.name ^ "::" ^ variant.variant_name) + in + "variant name: " ^ variant_name + | FieldId (id, field_id) -> + let field_name = + match id with + | Tuple -> failwith "Unreachable" + | Assumed (Result | Option) -> failwith "Unreachable" + | Assumed Vec -> + (* We can't directly have access to the fields of a vector *) + failwith "Unreachable" + | AdtId id -> ( + let def = TypeDefId.Map.find id type_defs in + match def.kind with + | Enum _ -> failwith "Unreachable" + | Struct fields -> + let field = FieldId.nth fields field_id in + let field_name = + match field.field_name with + | None -> FieldId.to_string field_id + | Some name -> name + in + Print.name_to_string def.name ^ "." ^ field_name) + in + "field name: " ^ field_name + | UnknownId -> "keyword" + | TypeVarId _ | VarId _ -> + (* We should never get there: we add indices to make sure variable + * names are unique *) + failwith "Unreachable" + let ctx_add (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = (* The id_to_string function to print nice debugging messages if there are * collisions *) - let id_to_string (id : id) : string = - let fun_defs = ctx.trans_ctx.fun_context.fun_defs in - let type_defs = ctx.trans_ctx.type_context.type_defs in - (* TODO: factorize the pretty-printing with what is in PrintPure *) - let get_type_name (id : type_id) : string = - match id with - | AdtId id -> - let def = TypeDefId.Map.find id type_defs in - Print.name_to_string def.name - | Assumed aty -> show_assumed_ty aty - | Tuple -> failwith "Unreachable" - in - match id with - | FunId (fid, rg_id) -> - let fun_name = - match fid with - | A.Local fid -> - Print.name_to_string (FunDefId.Map.find fid fun_defs).name - | A.Assumed aid -> A.show_assumed_fun_id aid - in - let fun_kind = - match rg_id with - | None -> "forward" - | Some rg_id -> "backward " ^ RegionGroupId.to_string rg_id - in - "fun name (" ^ fun_kind ^ "): " ^ fun_name - | TypeId id -> "type name: " ^ get_type_name id - | StructId id -> "struct constructor of: " ^ get_type_name id - | VariantId (id, variant_id) -> - let variant_name = - match id with - | Tuple -> failwith "Unreachable" - | Assumed Result -> - if variant_id = result_return_id then "@result::Return" - else if variant_id = result_fail_id then "@result::Fail" - else failwith "Unreachable" - | Assumed Option -> - if variant_id = option_some_id then "@option::Some" - else if variant_id = option_none_id then "@option::None" - else failwith "Unreachable" - | Assumed Vec -> failwith "Unreachable" - | AdtId id -> ( - let def = TypeDefId.Map.find id type_defs in - match def.kind with - | Struct _ -> failwith "Unreachable" - | Enum variants -> - let variant = VariantId.nth variants variant_id in - Print.name_to_string def.name ^ "::" ^ variant.variant_name) - in - "variant name: " ^ variant_name - | FieldId (id, field_id) -> - let field_name = - match id with - | Tuple -> failwith "Unreachable" - | Assumed (Result | Option) -> failwith "Unreachable" - | Assumed Vec -> - (* We can't directly have access to the fields of a vector *) - failwith "Unreachable" - | AdtId id -> ( - let def = TypeDefId.Map.find id type_defs in - match def.kind with - | Enum _ -> failwith "Unreachable" - | Struct fields -> - let field = FieldId.nth fields field_id in - let field_name = - match field.field_name with - | None -> FieldId.to_string field_id - | Some name -> name - in - Print.name_to_string def.name ^ "." ^ field_name) - in - "field name: " ^ field_name - | UnknownId -> "keyword" - | TypeVarId _ | VarId _ -> - (* We should never get there: we add indices to make sure variable - * names are unique *) - failwith "Unreachable" - in + let id_to_string (id : id) : string = id_to_string id ctx in let names_map = names_map_add id_to_string id name ctx.names_map in { ctx with names_map } let ctx_get (id : id) (ctx : extraction_ctx) : string = - IdMap.find id ctx.names_map.id_to_name + match IdMap.find_opt id ctx.names_map.id_to_name with + | Some s -> s + | None -> + log#serror ("Could not find: " ^ id_to_string id ctx); + raise Not_found let ctx_get_function (id : A.fun_id) (rg : RegionGroupId.id option) (ctx : extraction_ctx) : string = @@ -485,6 +491,12 @@ let ctx_add_variants (def : type_def) (variants : (VariantId.id * variant) list) (fun ctx (vid, v) -> ctx_add_variant def vid v ctx) ctx variants +let ctx_add_struct (def : type_def) (ctx : extraction_ctx) : + extraction_ctx * string = + let name = ctx.fmt.struct_constructor def.name in + let ctx = ctx_add (StructId (AdtId def.def_id)) name ctx in + (ctx, name) + let ctx_add_fun_def (def : fun_def) (ctx : extraction_ctx) : extraction_ctx = (* Lookup the CFIM def to compute the region group information *) let def_id = def.def_id in diff --git a/src/main.ml b/src/main.ml index b8673023..c30c43f2 100644 --- a/src/main.ml +++ b/src/main.ml @@ -95,7 +95,7 @@ let () = interpreter_log#set_level EL.Debug; statements_log#set_level EL.Debug; paths_log#set_level EL.Warning; - expressions_log#set_level EL.Warning; + expressions_log#set_level EL.Debug; expansion_log#set_level EL.Warning; borrows_log#set_level EL.Warning; invariants_log#set_level EL.Warning; |