diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CfimAst.ml | 7 | ||||
| -rw-r--r-- | src/Contexts.ml | 6 | ||||
| -rw-r--r-- | src/Interpreter.ml | 21 | ||||
| -rw-r--r-- | src/Invariants.ml | 4 | ||||
| -rw-r--r-- | src/Print.ml | 10 | ||||
| -rw-r--r-- | src/main.ml | 40 |
6 files changed, 53 insertions, 35 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 192638cf..6c9b596e 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -86,3 +86,10 @@ type fun_def = { body : statement; } [@@deriving show] +(** TODO: the type and function definitions contain information like `divergent` + * or `copyable`. I wonder if this information should be stored directly inside + * the definitions or inside separate maps/sets. + * Of course, if everything is stored in separate maps/sets, nothing + * prevents us from computing this info in Charon (and thus exporting directly + * it with the type/function defs), in which case we just have to implement special + * treatment when deserializing, to move the info to a separate map. *) diff --git a/src/Contexts.ml b/src/Contexts.ml index 5e8ae3d0..521ea0ed 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -60,8 +60,10 @@ type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] type config = { mode : interpreter_mode; check_invariants : bool } [@@deriving show] +type type_context = { type_defs : type_def list } [@@deriving show] + type eval_ctx = { - type_context : type_def list; + type_context : type_context; fun_context : fun_def list; type_vars : type_var list; env : env; @@ -94,7 +96,7 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder = lookup ctx.env let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def = - TypeDefId.nth ctx.type_context tid + TypeDefId.nth ctx.type_context.type_defs tid let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def = FunDefId.nth ctx.fun_context fid diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 1107ee20..a335a0d5 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2361,8 +2361,8 @@ let expand_bottom_value_from_projection (config : C.config) | ( Field (ProjAdt (def_id, opt_variant_id), _), T.Adt (T.AdtId def_id', regions, types) ) -> assert (def_id = def_id'); - compute_expanded_bottom_adt_value ctx.type_context def_id opt_variant_id - regions types + compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id + opt_variant_id regions types (* Tuples *) | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> assert (arity = List.length tys); @@ -2391,7 +2391,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool) (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list = (* Lookup the definition and check if it is an enumeration with several * variants *) - let def = T.TypeDefId.nth ctx.type_context def_id in + let def = C.ctx_lookup_type_def ctx def_id in assert (List.length regions = List.length def.T.region_params); (* Retrieve, for every variant, the list of its instantiated field types *) let variants_fields_types = @@ -2976,7 +2976,7 @@ let constant_value_to_typed_value (ctx : C.eval_ctx) (ty : T.ety) assert (def_id = def_id'); (* Check that the adt definition only has one variant with no fields, compute the variant id at the same time. *) - let def = T.TypeDefId.nth ctx.type_context def_id in + let def = C.ctx_lookup_type_def ctx def_id in assert (List.length def.region_params = 0); assert (List.length def.type_params = 0); let variant_id = @@ -3382,14 +3382,14 @@ let set_discriminant (config : C.config) (ctx : C.eval_ctx) (p : E.place) else (* Replace the value *) let bottom_v = - compute_expanded_bottom_adt_value ctx.type_context def_id - (Some variant_id) regions types + compute_expanded_bottom_adt_value ctx.type_context.type_defs + def_id (Some variant_id) regions types in let ctx = write_place_unwrap config access p bottom_v ctx in Ok (ctx, Unit)) | T.Adt (T.AdtId def_id, regions, types), V.Bottom -> let bottom_v = - compute_expanded_bottom_adt_value ctx.type_context def_id + compute_expanded_bottom_adt_value ctx.type_context.type_defs def_id (Some variant_id) regions types in let ctx = write_place_unwrap config access p bottom_v ctx in @@ -3894,7 +3894,7 @@ module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment *) - let test_unit_function (type_defs : T.type_def list) + let test_unit_function (type_context : C.type_context) (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result = (* Retrieve the function declaration *) let fdef = A.FunDefId.nth fun_defs fid in @@ -3911,7 +3911,7 @@ module Test = struct (* Create the evaluation context *) let ctx = { - C.type_context = type_defs; + C.type_context; C.fun_context = fun_defs; C.type_vars = []; C.env = []; @@ -3942,7 +3942,8 @@ module Test = struct (fun_defs : A.fun_def list) : unit = let test_fun (def : A.fun_def) : unit = if fun_def_is_unit def then - match test_unit_function type_defs fun_defs def.A.def_id with + let type_ctx = { C.type_defs } in + match test_unit_function type_ctx fun_defs def.A.def_id with | Error _ -> failwith "Unit test failed" | Ok _ -> () else () diff --git a/src/Invariants.ml b/src/Invariants.ml index fec6b2ed..364c14d0 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -352,7 +352,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.Adt av, T.Adt (T.AdtId def_id, regions, tys) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) - let def = T.TypeDefId.nth ctx.type_context def_id in + let def = C.ctx_lookup_type_def ctx def_id in (* Check the number of parameters *) assert (List.length regions = List.length def.region_params); assert (List.length tys = List.length def.type_params); @@ -435,7 +435,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = | V.AAdt av, T.Adt (T.AdtId def_id, regions, tys) -> (* Retrieve the definition to check the variant id, the number of * parameters, etc. *) - let def = T.TypeDefId.nth ctx.type_context def_id in + let def = C.ctx_lookup_type_def ctx def_id in (* Check the number of parameters *) assert (List.length regions = List.length def.region_params); assert (List.length tys = List.length def.type_params); diff --git a/src/Print.ml b/src/Print.ml index 2fd7e336..90f3946b 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -492,17 +492,19 @@ module Contexts = struct v.name in let type_def_id_to_string def_id = - let def = T.TypeDefId.nth ctx.type_context def_id in + let def = T.TypeDefId.nth ctx.type_context.type_defs def_id in PT.name_to_string def.name in let adt_variant_to_string = - type_ctx_to_adt_variant_to_string_fun ctx.type_context + type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs in let var_id_to_string vid = let bv = C.ctx_lookup_binder ctx vid in binder_to_string bv in - let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in + let adt_field_names = + type_ctx_to_adt_field_names_fun ctx.type_context.type_defs + in { rvar_to_string; r_to_string; @@ -604,7 +606,7 @@ module CfimAst = struct let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter = let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in let adt_field_to_string = - type_ctx_to_adt_field_to_string_fun ctx.type_context + type_ctx_to_adt_field_to_string_fun ctx.type_context.type_defs in let fun_def_id_to_string def_id = let def = A.FunDefId.nth ctx.fun_context def_id in diff --git a/src/main.ml b/src/main.ml index 4616aadf..f2e6eb06 100644 --- a/src/main.ml +++ b/src/main.ml @@ -1,9 +1,11 @@ open CfimOfJson open Logging open Print +open Contexts module T = Types module A = CfimAst module I = Interpreter +module C = Contexts type test = Test [@@deriving show] @@ -13,31 +15,35 @@ let _ = show_test Test * reason, the -g option doesn't work *) let () = Printexc.record_backtrace true -let usage = Printf.sprintf {|Aenaes: verification of Rust programs by translation +let usage = + Printf.sprintf + {|Aenaes: verification of Rust programs by translation Usage: %s [OPTIONS] FILE -|} Sys.argv.(0);; +|} + Sys.argv.(0) let () = - let spec = [ - ] in + let spec = [] in let spec = Arg.align spec in let filename = ref "" in - let fail () = print_string usage; exit 1 in - Arg.parse spec (fun f -> - if not (Filename.check_suffix f ".cfim") then begin - print_string "Unrecognized file extension"; - fail () - end else if not (Sys.file_exists f) then begin - print_string "File not found"; - fail () - end else - filename := f - ) usage; - if !filename = "" then begin + let fail () = print_string usage; exit 1 - end; + in + Arg.parse spec + (fun f -> + if not (Filename.check_suffix f ".cfim") then ( + print_string "Unrecognized file extension"; + fail ()) + else if not (Sys.file_exists f) then ( + print_string "File not found"; + fail ()) + else filename := f) + usage; + if !filename = "" then ( + print_string usage; + exit 1); let json = Yojson.Basic.from_file !filename in match cfim_module_of_json json with | Error s -> log#error "error: %s\n" s |