summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-14 16:32:18 +0100
committerSon Ho2022-01-14 16:32:18 +0100
commit38a877a0db9980d234cfe89a5528bef99620cab1 (patch)
tree20ca33341782d0bcc6632d423f8d1e4a538c0e96
parent20279216a270c1f8f8c76cc060ca44ad23186430 (diff)
Start working on greedy symbolic value expansion and expansion before
assignment
-rw-r--r--TODO.md10
-rw-r--r--src/Contexts.ml43
-rw-r--r--src/Identifiers.ml36
-rw-r--r--src/Interpreter.ml61
-rw-r--r--src/InterpreterExpansion.ml132
-rw-r--r--src/InterpreterExpressions.ml4
-rw-r--r--src/InterpreterPaths.ml6
-rw-r--r--src/InterpreterStatements.ml8
-rw-r--r--src/Invariants.ml11
-rw-r--r--src/Modules.ml44
-rw-r--r--src/Print.ml18
-rw-r--r--src/main.ml12
12 files changed, 318 insertions, 67 deletions
diff --git a/TODO.md b/TODO.md
index fdebe51f..c56c91a9 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,13 +1,13 @@
# TODO
-1. add a switch to allow general symbolic values (containing references, etc.)
- or not.
-
-2. expand symbolic values which are primitively copyable upon using them as
+1. expand symbolic values which are primitively copyable upon using them as
function arguments or putting them in the return value, in order to deduplicate
those values.
-4. add a check in function inputs: ok to take as parameters symbolic values with
+2. add a switch to allow general symbolic values (containing references, etc.)
+ or not.
+
+3. add a check in function inputs: ok to take as parameters symbolic values with
borrow parameters *if* they come from the "input abstractions".
In order to do this, add a symbolic value kind (would make things easier than
adding ad-hoc lookups...): `FunRet`, `FunGivenBack`, `SynthInput`, `SynthGivenBack`
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