diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Contexts.ml | 43 | ||||
| -rw-r--r-- | src/Identifiers.ml | 36 | ||||
| -rw-r--r-- | src/Interpreter.ml | 61 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 132 | ||||
| -rw-r--r-- | src/InterpreterExpressions.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 6 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 8 | ||||
| -rw-r--r-- | src/Invariants.ml | 11 | ||||
| -rw-r--r-- | src/Modules.ml | 44 | ||||
| -rw-r--r-- | src/Print.ml | 18 | ||||
| -rw-r--r-- | src/main.ml | 12 |
11 files changed, 313 insertions, 62 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 6eafd9ef..8a9c4857 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -3,6 +3,7 @@ open Values open CfimAst module V = Values open ValuesUtils +module M = Modules (** Some global counters. * @@ -104,10 +105,42 @@ type env = env_elem list type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show] -type config = { mode : interpreter_mode; check_invariants : bool } +type config = { + mode : interpreter_mode; + (** Concrete mode (interpreter) or symbolic mode (for synthesis) **) + check_invariants : bool; + (** Check that invariants are maintained whenever we execute a statement *) + greedy_expand_symbolics_with_borrows : bool; + (** Expand all symbolic values containing borrows upon introduction - allows + to use restrict ourselves to a simpler model for the projectors over + symbolic values. + The interpreter fails if doing this requires to do a branching (because + we need to expand an enumeration with strictly more than one variant) + or if we need to expand a recursive type (because this leads to looping). + *) +} [@@deriving show] -type type_context = { type_defs : type_def list } [@@deriving show] +type partial_config = { + check_invariants : bool; + greedy_expand_symbolics_with_borrows : bool; +} +(** See [config] *) + +let config_of_partial (mode : interpreter_mode) (config : partial_config) : + config = + { + mode; + check_invariants = config.check_invariants; + greedy_expand_symbolics_with_borrows = + config.greedy_expand_symbolics_with_borrows; + } + +type type_context = { + type_defs_groups : M.types_decl_group TypeDefId.map_t; + type_defs : type_def list; +} +[@@deriving show] type eval_ctx = { type_context : type_context; @@ -137,9 +170,11 @@ let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder = in lookup ctx.env +(** TODO: make this more efficient with maps *) let ctx_lookup_type_def (ctx : eval_ctx) (tid : TypeDefId.id) : type_def = TypeDefId.nth ctx.type_context.type_defs tid +(** TODO: make this more efficient with maps *) let ctx_lookup_fun_def (ctx : eval_ctx) (fid : FunDefId.id) : fun_def = FunDefId.nth ctx.fun_context fid @@ -269,6 +304,10 @@ let env_lookup_abs (env : env) (abs_id : V.AbstractionId.id) : V.abs = let ctx_lookup_abs (ctx : eval_ctx) (abs_id : V.AbstractionId.id) : V.abs = env_lookup_abs ctx.env abs_id +let ctx_type_def_is_rec (ctx : eval_ctx) (id : TypeDefId.id) : bool = + let decl_group = TypeDefId.Map.find id ctx.type_context.type_defs_groups in + match decl_group with M.Rec _ -> true | M.NonRec _ -> false + (** Visitor to iterate over the values in the *current* frame *) class ['self] iter_frame = object (self : 'self) diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 18b8edee..c6d7ea10 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -12,6 +12,8 @@ module type Id = sig type set_t + type +!'a map_t + val zero : id val generator_zero : generator @@ -55,13 +57,18 @@ module type Id = sig val show_set_t : set_t -> string + val pp_map_t : + (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a map_t -> unit + + val show_map_t : ('a -> string) -> 'a map_t -> string + module Ord : Map.OrderedType with type t = id module Set : Set.S with type elt = id with type t = set_t val set_to_string : Set.t -> string - module Map : Map.S with type key = id + module Map : Map.S with type key = id with type 'a t = 'a map_t (* TODO: map_to_string *) @@ -134,12 +141,37 @@ module IdGen () : Id = struct type set_t = Set.t + type +!'a map_t = 'a Map.t + let show_set_t s = let ids = Set.fold (fun id s -> to_string id :: s) s [] in let ids = List.rev ids in "{" ^ String.concat "," ids ^ "}" - let pp_set_t fmt s = Format.pp_print_string fmt (show_set_t s) + let pp_set_t fmt s = + let pp_string = Format.pp_print_string fmt in + pp_string "{"; + Set.iter (fun id -> pp_string (to_string id ^ ",")) s; + pp_string "}" + + let show_map_t show_a s = + let ids = + Map.fold (fun id x s -> (to_string id ^ " -> " ^ show_a x) :: s) s [] + in + let ids = List.rev ids in + "{" ^ String.concat "," ids ^ "}" + + let pp_map_t (pp_a : Format.formatter -> 'a -> unit) (fmt : Format.formatter) + (m : 'a map_t) : unit = + let pp_string = Format.pp_print_string fmt in + pp_string "{"; + Map.iter + (fun id x -> + pp_string (to_string id ^ " -> "); + pp_a fmt x; + pp_string ",") + m; + pp_string "}" let set_to_string ids = let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ae5376f9..c998214b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1,6 +1,7 @@ module L = Logging module T = Types module A = CfimAst +module M = Modules open Utils open InterpreterUtils open InterpreterExpressions @@ -25,12 +26,16 @@ open InterpreterStatements let log = L.interpreter_log module Test = struct - let initialize_context (type_context : C.type_context) - (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx = + let initialize_context (m : M.cfim_module) (type_vars : T.type_var list) : + C.eval_ctx = + let type_defs_groups, _funs_defs_groups = + M.split_declarations_to_group_maps m.declarations + in + let type_context = { C.type_defs_groups; type_defs = m.types } in C.reset_global_counters (); { C.type_context; - C.fun_context = fun_defs; + C.fun_context = m.functions; C.type_vars; C.env = []; C.ended_regions = T.RegionId.Set.empty; @@ -44,8 +49,8 @@ module Test = struct "Dummy" abstractions are introduced for the regions present in the function signature. *) - let initialize_symbolic_context_for_fun (type_context : C.type_context) - (fun_defs : A.fun_def list) (fdef : A.fun_def) : C.eval_ctx = + let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) + : C.eval_ctx = (* The abstractions are not initialized the same way as for function * calls: they contain *loan* projectors, because they "provide" us * with the input values (which behave as if they had been returned @@ -59,7 +64,7 @@ module Test = struct * *) let sg = fdef.signature in (* Create the context *) - let ctx = initialize_context type_context fun_defs sg.type_params in + let ctx = initialize_context m sg.type_params in (* Instantiate the signature *) let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params @@ -108,14 +113,14 @@ module Test = struct (** Test a unit function (taking no arguments) by evaluating it in an empty environment. *) - let test_unit_function (type_context : C.type_context) - (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result = + let test_unit_function (config : C.partial_config) (m : M.cfim_module) + (fid : A.FunDefId.id) : unit eval_result = (* Retrieve the function declaration *) - let fdef = A.FunDefId.nth fun_defs fid in + let fdef = A.FunDefId.nth m.functions fid in (* Debug *) log#ldebug - (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name)); + (lazy ("test_unit_function: " ^ Print.name_to_string fdef.A.name)); (* Sanity check - *) assert (List.length fdef.A.signature.region_params = 0); @@ -123,13 +128,13 @@ module Test = struct assert (fdef.A.arg_count = 0); (* Create the evaluation context *) - let ctx = initialize_context type_context fun_defs [] in + let ctx = initialize_context m [] in (* Insert the (uninitialized) local variables *) let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in (* Evaluate the function *) - let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in + let config = C.config_of_partial C.ConcreteMode config in match eval_function_body config ctx fdef.A.body with | [ Ok _ ] -> Ok () | [ Error err ] -> Error err @@ -146,34 +151,31 @@ module Test = struct && List.length def.A.signature.inputs = 0 (** Test all the unit functions in a list of function definitions *) - let test_unit_functions (type_defs : T.type_def list) - (fun_defs : A.fun_def list) : unit = - let unit_funs = List.filter fun_def_is_unit fun_defs in + let test_unit_functions (config : C.partial_config) (m : M.cfim_module) : unit + = + let unit_funs = List.filter fun_def_is_unit m.functions in let test_unit_fun (def : A.fun_def) : unit = - let type_ctx = { C.type_defs } in - match test_unit_function type_ctx fun_defs def.A.def_id with + match test_unit_function config m def.A.def_id with | Error _ -> failwith "Unit test failed (concrete execution)" | Ok _ -> () in List.iter test_unit_fun unit_funs (** Execute the symbolic interpreter on a function. *) - let test_function_symbolic (type_context : C.type_context) - (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : - C.eval_ctx eval_result list = + let test_function_symbolic (config : C.partial_config) (m : M.cfim_module) + (fid : A.FunDefId.id) : C.eval_ctx eval_result list = (* Retrieve the function declaration *) - let fdef = A.FunDefId.nth fun_defs fid in + let fdef = A.FunDefId.nth m.functions fid in (* Debug *) log#ldebug - (lazy - ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name)); + (lazy ("test_function_symbolic: " ^ Print.name_to_string fdef.A.name)); (* Create the evaluation context *) - let ctx = initialize_symbolic_context_for_fun type_context fun_defs fdef in + let ctx = initialize_symbolic_context_for_fun m fdef in (* Evaluate the function *) - let config = { C.mode = C.SymbolicMode; C.check_invariants = true } in + let config = C.config_of_partial C.SymbolicMode config in eval_function_body config ctx fdef.A.body (** Execute the symbolic interpreter on a list of functions. @@ -181,17 +183,16 @@ module Test = struct TODO: for now we ignore the functions which contain loops, because they are not supported by the symbolic interpreter. *) - let test_functions_symbolic (type_defs : T.type_def list) - (fun_defs : A.fun_def list) : unit = + let test_functions_symbolic (config : C.partial_config) (m : M.cfim_module) : + unit = let no_loop_funs = - List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) fun_defs + List.filter (fun f -> not (CfimAstUtils.fun_def_has_loops f)) m.functions in let test_fun (def : A.fun_def) : unit = - let type_ctx = { C.type_defs } in (* Execute the function - note that as the symbolic interpreter explores * all the path, some executions are expected to "panic": we thus don't * check the return value *) - let _ = test_function_symbolic type_ctx fun_defs def.A.def_id in + let _ = test_function_symbolic config m def.A.def_id in () in List.iter test_fun no_loop_funs diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 3903ca14..4f0ac11c 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -406,12 +406,9 @@ let expand_symbolic_value_borrow (config : C.config) (** Expand a symbolic value which is not an enumeration with several variants (i.e., in a situation where it doesn't lead to branching). - - This function is used when exploring paths. *) let expand_symbolic_value_no_branching (config : C.config) - (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) : - C.eval_ctx = + (sp : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = (* Remember the initial context for printing purposes *) let ctx0 = ctx in (* Compute the expanded value - note that when doing so, we may introduce @@ -419,11 +416,9 @@ let expand_symbolic_value_no_branching (config : C.config) let original_sv = sp in let rty = original_sv.V.sv_ty in let ctx = - match (pe, rty) with + match rty with (* "Regular" ADTs *) - | ( Field (ProjAdt (def_id, _opt_variant_id), _), - T.Adt (T.AdtId def_id', regions, types) ) -> ( - assert (def_id = def_id'); + | T.Adt (T.AdtId def_id, regions, types) -> ( (* Compute the expanded value - there should be exactly one because we * don't allow to expand enumerations with strictly more than one variant *) let expand_enumerations = false in @@ -440,10 +435,12 @@ let expand_symbolic_value_no_branching (config : C.config) S.synthesize_symbolic_expansion_no_branching original_sv see; (* Return *) ctx - | _ -> failwith "Unexpected") + | _ -> + failwith + "expand_symbolic_value_no_branching: the expansion lead to \ + branching") (* Tuples *) - | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> - assert (arity = List.length tys); + | T.Adt (T.Tuple, [], tys) -> (* Generate the field values *) let see = compute_expanded_symbolic_tuple_value tys in (* Apply in the context *) @@ -455,7 +452,7 @@ let expand_symbolic_value_no_branching (config : C.config) (* Return *) ctx (* Boxes *) - | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> + | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) -> let see = compute_expanded_symbolic_box_value boxed_ty in (* Apply in the context *) let ctx = @@ -466,11 +463,11 @@ let expand_symbolic_value_no_branching (config : C.config) (* Return *) ctx (* Borrows *) - | Deref, T.Ref (region, ref_ty, rkind) -> + | T.Ref (region, ref_ty, rkind) -> expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx | _ -> failwith - ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) + ("expand_symbolic_value_no_branching: unreachable: " ^ T.show_rty rty) in (* Debugging *) (* Debug *) @@ -485,6 +482,36 @@ let expand_symbolic_value_no_branching (config : C.config) (* Return *) ctx +(** Expand a symbolic value which is not an enumeration with several variants + (i.e., in a situation where it doesn't lead to branching). + + This function is used when exploring paths. It simply performs a few + sanity checks before calling [expand_symbolic_value_no_branching]. + *) +let expand_symbolic_value_no_branching_from_projection_elem (config : C.config) + (pe : E.projection_elem) (sp : V.symbolic_value) (ctx : C.eval_ctx) : + C.eval_ctx = + (* Sanity checks *) + let rty = sp.V.sv_ty in + let _ = + match (pe, rty) with + (* "Regular" ADTs *) + | Field (ProjAdt (def_id, _), _), T.Adt (T.AdtId def_id', _, _) -> + assert (def_id = def_id') + (* Tuples *) + | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) -> + assert (arity = List.length tys) + (* Boxes *) + | DerefBox, T.Adt (T.Assumed T.Box, [], [ _ ]) -> () + (* Borrows *) + | Deref, T.Ref (_, _, _) -> () + | _ -> + failwith + ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty) + in + (* Perform the expansion *) + expand_symbolic_value_no_branching config sp ctx + (** Expand a symbolic enumeration value. This might lead to branching. @@ -519,3 +546,80 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value) in List.map apply seel | _ -> failwith "Unexpected" + +(** Expand all the symbolic values which contain borrows. + Allows us to restrict ourselves to a simpler model for the projectors over + symbolic values. + + Fails if doing this requires to do a branching (because we need to expand + an enumeration with strictly more than one variant, a slice, etc.) or if + we need to expand a recursive type (because this leads to looping). + *) +let greedy_expand_symbolics_with_borrows (config : C.config) (ctx : C.eval_ctx) + : C.eval_ctx = + (* The visitor object, to look for symbolic values in the concrete environment *) + let obj = + object + inherit [_] C.iter_eval_ctx + + method! visit_Symbolic _ sv = + if ty_has_regions (Subst.erase_regions sv.V.sv_ty) then + raise (FoundSymbolicValue sv) + else () + + method! visit_abs _ _ = () + (** Don't enter abstractions *) + end + in + + let rec expand (ctx : C.eval_ctx) : C.eval_ctx = + try + obj#visit_eval_ctx () ctx; + ctx + with FoundSymbolicValue sv -> + (* Expand and recheck the environment *) + let ctx = + match sv.V.sv_ty with + | T.Adt (AdtId def_id, _, _) -> + (* [expand_symbolic_value_no_branching] checks if there are branchings, + * but we prefer to also check it here - this leads to cleaner messages + * and debugging *) + let def = C.ctx_lookup_type_def ctx def_id in + (match def.kind with + | T.Struct _ | T.Enum ([] | [ _ ]) -> () + | T.Enum (_ :: _) -> + failwith + ("Attempted to greedily expand a symbolic enumeration with > \ + 1 variants (option [greedy_expand_symbolics_with_borrows] \ + of [config]): " + ^ Print.name_to_string def.name)); + (* Also, we need to check if the definition is recursive *) + if C.ctx_type_def_is_rec ctx def_id then + failwith + ("Attempted to greedily expand a recursive definition (option \ + [greedy_expand_symbolics_with_borrows] of [config]): " + ^ Print.name_to_string def.name) + else expand_symbolic_value_no_branching config sv ctx + | T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) -> + (* Ok *) + expand_symbolic_value_no_branching config sv ctx + | T.Array _ -> raise Errors.Unimplemented + | T.Slice _ -> failwith "Can't expand symbolic slices" + | T.TypeVar _ | Bool | Char | Never | Integer _ | Str -> + failwith "Unreachable" + in + expand ctx + in + expand ctx + +(** If this mode is activated through the [config], greedily expand the symbolic + values which need to be expanded. See [config] for more information. + *) +let greedy_expand_symbolic_values (config : C.config) (ctx : C.eval_ctx) : + C.eval_ctx = + let ctx = + if config.greedy_expand_symbolics_with_borrows then + greedy_expand_symbolics_with_borrows config ctx + else ctx + in + ctx diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index f3b07cc2..93ec8640 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -114,6 +114,8 @@ let eval_operand_prepare (config : C.config) (ctx : C.eval_ctx) (op : E.operand) | Expressions.Copy p -> (* Access the value *) let access = Read in + (* TODO: expand the value if it is a symbolic value *) + raise Unimplemented; prepare_rplace config access p ctx | Expressions.Move p -> (* Access the value *) @@ -139,6 +141,8 @@ let eval_operand (config : C.config) (ctx : C.eval_ctx) (op : E.operand) : | Expressions.Copy p -> (* Access the value *) let access = Read in + (* TODO: expand the value if it is a symbolic value *) + raise Unimplemented; let ctx, v = prepare_rplace config access p ctx in (* Copy the value *) assert (not (bottom_in_value ctx.ended_regions v)); diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index e1c80d89..6bc22af4 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -469,7 +469,8 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind) activate_inactivated_mut_borrow config bid ctx | FailSymbolic (pe, sp) -> (* Expand the symbolic value *) - expand_symbolic_value_no_branching config pe sp ctx + expand_symbolic_value_no_branching_from_projection_elem config pe sp + ctx | FailBottom (_, _, _) -> (* We can't expand [Bottom] values while reading them *) failwith "Found [Bottom] while reading a place" @@ -496,7 +497,8 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind) activate_inactivated_mut_borrow config bid ctx | FailSymbolic (pe, sp) -> (* Expand the symbolic value *) - expand_symbolic_value_no_branching config pe sp ctx + expand_symbolic_value_no_branching_from_projection_elem config pe sp + ctx | FailBottom (remaining_pes, pe, ty) -> (* Expand the [Bottom] value *) expand_bottom_value_from_projection config access p remaining_pes pe diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index d13dc515..e6fadbdd 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -598,6 +598,9 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) ("\n**About to evaluate statement**: [\n" ^ statement_to_string_with_tab ctx st ^ "\n]\n\n**Context**:\n" ^ eval_ctx_to_string ctx ^ "\n\n")); + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let ctx = greedy_expand_symbolic_values config ctx in (* Sanity check *) if config.C.check_invariants then Inv.check_invariants ctx; (* Evaluate *) @@ -888,6 +891,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) in (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in + (* TODO: expand the primitively copyable symbolic values *) + raise Errors.Unimplemented; let args_with_rtypes = List.combine args inst_sg.A.inputs in (* Check the type of the input arguments *) assert ( @@ -1021,6 +1026,9 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx) match res with | Error err -> Error err | Ok (ctx, res) -> ( + (* Expand the symbolic values if necessary - we need to do that before + * checking the invariants *) + let ctx = greedy_expand_symbolic_values config ctx in (* Sanity check *) if config.C.check_invariants then Inv.check_invariants ctx; match res with diff --git a/src/Invariants.ml b/src/Invariants.ml index 7664f70e..5009410e 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -621,7 +621,16 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = in visitor#visit_eval_ctx (None : V.abs option) ctx +(** TODO: + + - a symbolic value can't be both in proj_borrows and in the concrete env + (this is why we preemptively expand copyable symbolic values) + + *) +let check_symbolic_values (ctx : C.eval_ctx) : unit = raise Errors.Unimplemented + let check_invariants (ctx : C.eval_ctx) : unit = check_loans_borrows_relation_invariant ctx; check_borrowed_values_invariant ctx; - check_typing_invariant ctx + check_typing_invariant ctx; + check_symbolic_values ctx diff --git a/src/Modules.ml b/src/Modules.ml index bf5e9835..e4cb06c1 100644 --- a/src/Modules.ml +++ b/src/Modules.ml @@ -14,3 +14,47 @@ type cfim_module = { functions : fun_def list; } (** CFIM module *) + +type 'id decl_group = NonRec of 'id | Rec of 'id list [@@deriving show] + +type types_decl_group = TypeDefId.id decl_group [@@deriving show] + +type funs_decl_group = FunDefId.id decl_group [@@deriving show] + +(** Split a module's declarations between types and functions *) +let split_declarations (decls : declaration list) : + types_decl_group list * funs_decl_group list = + let rec split decls = + match decls with + | [] -> ([], []) + | d :: decls' -> ( + let types, funs = split decls' in + match d with + | Type id -> (NonRec id :: types, funs) + | Fun id -> (types, NonRec id :: funs) + | RecTypes ids -> (Rec ids :: types, funs) + | RecFuns ids -> (types, Rec ids :: funs)) + in + split decls + +(** Split a module's declarations into two maps from type/fun ids to + declaration groups. + *) +let split_declarations_to_group_maps (decls : declaration list) : + types_decl_group TypeDefId.Map.t * funs_decl_group FunDefId.Map.t = + let module G (M : Map.S) = struct + let add_group (map : M.key decl_group M.t) (group : M.key decl_group) : + M.key decl_group M.t = + match group with + | NonRec id -> M.add id group map + | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids + + let create_map (groups : M.key decl_group list) : M.key decl_group M.t = + List.fold_left add_group M.empty groups + end in + let types, funs = split_declarations decls in + let module TG = G (TypeDefId.Map) in + let types = TG.create_map types in + let module FG = G (FunDefId.Map) in + let funs = FG.create_map funs in + (types, funs) diff --git a/src/Print.ml b/src/Print.ml index d4f051f9..1eab6714 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -10,6 +10,8 @@ module M = Modules let option_to_string (to_string : 'a -> string) (x : 'a option) : string = match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None" +let name_to_string (name : name) : string = String.concat "::" name + (** Pretty-printing for types *) module Types = struct let type_var_to_string (tv : T.type_var) : string = tv.name @@ -115,8 +117,6 @@ module Types = struct ^ String.concat ", " (List.map (field_to_string fmt) v.fields) ^ ")" - let name_to_string (name : name) : string = String.concat "::" name - let type_def_to_string (type_def_id_to_string : T.TypeDefId.id -> string) (def : T.type_def) : string = let regions = def.region_params in @@ -492,7 +492,7 @@ module Contexts = struct | Struct _ -> failwith "Unreachable" | Enum variants -> let variant = T.VariantId.nth variants variant_id in - PT.name_to_string def.name ^ "::" ^ variant.variant_name + name_to_string def.name ^ "::" ^ variant.variant_name let type_ctx_to_adt_field_names_fun (ctx : T.type_def list) : T.TypeDefId.id -> T.VariantId.id option -> string list option = @@ -514,7 +514,7 @@ module Contexts = struct in let type_def_id_to_string def_id = let def = T.TypeDefId.nth ctx.type_context.type_defs def_id in - PT.name_to_string def.name + name_to_string def.name in let adt_variant_to_string = type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs @@ -633,7 +633,7 @@ module CfimAst = struct in let fun_def_id_to_string def_id = let def = A.FunDefId.nth ctx.fun_context def_id in - PT.name_to_string def.name + name_to_string def.name in { rvar_to_string = ctx_fmt.PV.rvar_to_string; @@ -851,7 +851,7 @@ module CfimAst = struct let sg = def.signature in (* Function name *) - let name = PT.name_to_string def.A.name in + let name = name_to_string def.A.name in (* Region/type parameters *) let regions = sg.region_params in @@ -911,7 +911,7 @@ module Module = struct string = let type_def_id_to_string (id : T.TypeDefId.id) : string = let def = T.TypeDefId.nth type_context id in - PT.name_to_string def.name + name_to_string def.name in PT.type_def_to_string type_def_id_to_string def @@ -933,11 +933,11 @@ module Module = struct in let type_def_id_to_string def_id = let def = T.TypeDefId.nth type_context def_id in - PT.name_to_string def.name + name_to_string def.name in let fun_def_id_to_string def_id = let def = A.FunDefId.nth fun_context def_id in - PT.name_to_string def.name + name_to_string def.name in let var_id_to_string vid = let var = V.VarId.nth def.locals vid in diff --git a/src/main.ml b/src/main.ml index c6545fcb..e8f46b99 100644 --- a/src/main.ml +++ b/src/main.ml @@ -59,8 +59,16 @@ let () = (* Print the module *) main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); + (* Some options for the execution *) + let config = + { + C.check_invariants = true; + greedy_expand_symbolics_with_borrows = false; + } + in + (* Test the unit functions with the concrete interpreter *) - I.Test.test_unit_functions m.types m.functions; + I.Test.test_unit_functions config m; (* Evaluate the symbolic interpreter on the functions *) - I.Test.test_functions_symbolic m.types m.functions + I.Test.test_functions_symbolic config m |