summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CfimOfJson.ml2
-rw-r--r--src/ExtractToFStar.ml10
-rw-r--r--src/InterpreterExpressions.ml18
-rw-r--r--src/InterpreterUtils.ml2
-rw-r--r--src/Print.ml5
-rw-r--r--src/PrintPure.ml3
-rw-r--r--src/PureToExtract.ml170
-rw-r--r--src/main.ml2
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 00:26:54 +0000