summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-06 14:43:35 +0100
committerSon Ho2022-01-06 14:43:35 +0100
commitf2fb0dc39cfa9aef2b16963d3f8a270ec45bae5e (patch)
tree652fbd0e923a1cae5d6516f4ce9cadd9177c56db
parent3cadf01e5b67af4ec91f2de3c32e119cd90c678c (diff)
Make good progress on implementing utilities to test symbolic execution
Diffstat (limited to '')
-rw-r--r--src/CfimAst.ml17
-rw-r--r--src/CfimAstUtils.ml5
-rw-r--r--src/Interpreter.ml173
-rw-r--r--src/InterpreterPaths.ml2
-rw-r--r--src/InterpreterStatements.ml101
-rw-r--r--src/InterpreterUtils.ml28
-rw-r--r--src/Print.ml2
-rw-r--r--src/Utilities.ml16
-rw-r--r--src/Utils.ml17
-rw-r--r--src/main.ml2
10 files changed, 269 insertions, 94 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml
index a4a128c3..ac66d1a4 100644
--- a/src/CfimAst.ml
+++ b/src/CfimAst.ml
@@ -95,13 +95,19 @@ class ['self] iter_statement_base =
method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
+ method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
+
method visit_call : 'env -> call -> unit = fun _ _ -> ()
+
+ method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
+
+ method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
end
(** Ancestor for [typed_value] map visitor *)
class ['self] map_statement_base =
object (_self : 'self)
- inherit [_] VisitorsRuntime.iter
+ inherit [_] VisitorsRuntime.map
method visit_place : 'env -> place -> place = fun _ x -> x
@@ -111,7 +117,15 @@ class ['self] map_statement_base =
method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
+ method visit_operand : 'env -> operand -> operand = fun _ x -> x
+
method visit_call : 'env -> call -> call = fun _ x -> x
+
+ method visit_integer_type : 'env -> integer_type -> integer_type =
+ fun _ x -> x
+
+ method visit_scalar_value : 'env -> scalar_value -> scalar_value =
+ fun _ x -> x
end
type statement =
@@ -136,7 +150,6 @@ type statement =
| Sequence of statement * statement
| Switch of operand * switch_targets
| Loop of statement
-[@@deriving show]
and switch_targets =
| If of statement * statement (** Gives the "if" and "else" blocks *)
diff --git a/src/CfimAstUtils.ml b/src/CfimAstUtils.ml
index f811475c..96410dde 100644
--- a/src/CfimAstUtils.ml
+++ b/src/CfimAstUtils.ml
@@ -2,7 +2,7 @@ open CfimAst
open Utils
(** Check if a [statement] contains loops *)
-let rec statement_has_loops (st : statement) : bool =
+let statement_has_loops (st : statement) : bool =
let obj =
object
inherit [_] iter_statement
@@ -14,3 +14,6 @@ let rec statement_has_loops (st : statement) : bool =
obj#visit_statement () st;
false
with Found -> true
+
+(** Check if a [fun_def] contains loops *)
+let fun_def_has_loops (fd : fun_def) : bool = statement_has_loops fd.body
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index e74aa1e7..cb42abf2 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1,4 +1,9 @@
+open Errors
module L = Logging
+module T = Types
+module A = CfimAst
+open Utils
+open InterpreterUtils
open InterpreterExpressions
open InterpreterStatements
@@ -18,9 +23,94 @@ open InterpreterStatements
(* TODO: remove the config parameters when they are useless *)
module Test = struct
+ let initialize_context (type_context : C.type_context)
+ (fun_defs : A.fun_def list) : C.eval_ctx =
+ {
+ C.type_context;
+ C.fun_context = fun_defs;
+ C.type_vars = [];
+ C.env = [];
+ C.symbolic_counter = V.SymbolicValueId.generator_zero;
+ C.borrow_counter = V.BorrowId.generator_zero;
+ C.region_counter = T.RegionId.generator_zero;
+ C.abstraction_counter = V.AbstractionId.generator_zero;
+ }
+
+ (** Initialize an evaluation context to execute a function.
+
+ Introduces local variables initialized in the following manner:
+ - input arguments are initialized as symbolic values
+ - the remaining locals are initialized as ⊥
+ "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 =
+ (* 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
+ * by some function calls...).
+ * Also, note that we properly set the set of parents of every abstraction:
+ * this should not be necessary, as those abstractions should never be
+ * *automatically* ended (because ending some borrows requires to end
+ * one of them), but rather selectively ended when generating code
+ * for each of the backward functions. We do it only because we can
+ * do it, and because it gives a bit of sanity.
+ * *)
+ (* Create the context *)
+ let ctx = initialize_context type_context fun_defs in
+ (* Instantiate the signature *)
+ let sg = fdef.signature in
+ let type_params =
+ List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params
+ in
+ let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
+ (* Create fresh symbolic values for the inputs *)
+ let ctx, input_svs =
+ List.fold_left_map
+ (fun ctx ty -> mk_fresh_symbolic_value ty ctx)
+ ctx inst_sg.inputs
+ in
+ (* Create the abstractions and insert them in the context *)
+ let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
+ let abs_id = rg.A.id in
+ let parents =
+ List.fold_left
+ (fun s pid -> V.AbstractionId.Set.add pid s)
+ V.AbstractionId.Set.empty rg.A.parents
+ in
+ let regions =
+ List.fold_left
+ (fun s rid -> T.RegionId.Set.add rid s)
+ T.RegionId.Set.empty rg.A.regions
+ in
+ (* Project over the values - we use *loan* projectors, as explained above *)
+ let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
+ (* Create the abstraction *)
+ let abs = { V.abs_id; parents; regions; avalues } in
+ (* Insert the abstraction in the context *)
+ let ctx = { ctx with env = Abs abs :: ctx.env } in
+ (* Return *)
+ ctx
+ in
+ (* Split the variables between return var, inputs and remaining locals *)
+ let ret_var = List.hd fdef.locals in
+ let input_vars, local_vars =
+ list_split_at (List.tl fdef.locals) fdef.arg_count
+ in
+ (* Push the return variable (initialized with ⊥) *)
+ let ctx = C.ctx_push_uninitialized_var ctx ret_var in
+ (* Push the input variables (initialized with symbolic values) *)
+ let input_values = List.map mk_typed_value_from_symbolic_value input_svs in
+ let ctx = C.ctx_push_vars ctx (List.combine input_vars input_values) in
+ (* Push the remaining local variables (initialized with ⊥) *)
+ let ctx = C.ctx_push_uninitialized_vars ctx local_vars in
+ (* Return *)
+ ctx
+
(** Test a unit function (taking no arguments) by evaluating it in an empty
- environment
- *)
+ environment.
+ *)
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 *)
@@ -36,20 +126,9 @@ module Test = struct
assert (fdef.A.arg_count = 0);
(* Create the evaluation context *)
- let ctx =
- {
- C.type_context;
- C.fun_context = fun_defs;
- C.type_vars = [];
- C.env = [];
- C.symbolic_counter = V.SymbolicValueId.generator_zero;
- C.borrow_counter = V.BorrowId.generator_zero;
- C.region_counter = T.RegionId.generator_zero;
- C.abstraction_counter = V.AbstractionId.generator_zero;
- }
- in
+ let ctx = initialize_context type_context fun_defs in
- (* Put the (uninitialized) local variables *)
+ (* Insert the (uninitialized) local variables *)
let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in
(* Evaluate the function *)
@@ -70,15 +149,65 @@ module Test = struct
&& List.length def.A.signature.inputs = 0
(** Test all the unit functions in a list of function definitions *)
- let test_all_unit_functions (type_defs : T.type_def list)
+ 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_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
+ | 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_symbolic_function (type_context : C.type_context)
+ (fun_defs : A.fun_def list) (fid : A.FunDefId.id) : unit eval_result list
+ =
+ (* Retrieve the function declaration *)
+ let fdef = A.FunDefId.nth fun_defs fid in
+
+ (* Debug *)
+ L.log#ldebug
+ (lazy
+ ("test_symbolic_function: " ^ Print.Types.name_to_string fdef.A.name));
+
+ (* Sanity check - *)
+ assert (List.length fdef.A.signature.region_params = 0);
+ assert (List.length fdef.A.signature.type_params = 0);
+ assert (fdef.A.arg_count = 0);
+
+ (* Create the evaluation context *)
+ let ctx = initialize_context type_context fun_defs in
+
+ (* Initialize the inputs as symbolic values *)
+ raise Unimplemented
+
+ (* (* Initialize the remaining local variables as Bottom *)
+ 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
+ match eval_function_body config ctx fdef.A.body with
+ | [ Ok _ ] -> Ok ()
+ | [ Error err ] -> Error err
+ | _ ->
+ (* We execute the concrete interpreter: there shouldn't be any branching *)
+ failwith "Unreachable"*)
+
+ (** Execute the symbolic interpreter on a list of functions.
+
+ TODO: for now we ignore the functions which contain loops, because
+ they are not supported by the symbolic interpreter.
+ *)
+ let test_symbolic_functions (type_defs : T.type_def list)
(fun_defs : A.fun_def list) : unit =
+ let no_loop_funs = List.filter CfimAstUtils.fun_def_has_loops fun_defs in
let test_fun (def : A.fun_def) : unit =
- if fun_def_is_unit def then
- 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 ()
+ let type_ctx = { C.type_defs } in
+ let res = test_symbolic_function type_ctx fun_defs def.A.def_id in
+ if List.for_all Result.is_ok res then ()
+ else failwith "Unit test failed (symbolic execution)"
in
List.iter test_fun fun_defs
end
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index d4de318b..80725bab 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -410,7 +410,7 @@ let expand_bottom_value_from_projection (config : C.config)
during whose evaluation we got stuck *)
let projection' =
fst
- (Utilities.list_split_at p.projection
+ (Utils.list_split_at p.projection
(List.length p.projection - remaining_pes))
in
let p' = { p with projection = projection' } in
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 91035574..6b06a27f 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -421,6 +421,54 @@ let eval_non_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
(* Return *)
Ok ctx)
+(** Instantiate a function signature, introducing fresh abstraction ids and
+ region ids. This is mostly used in preparation of function calls, when
+ evaluating in symbolic mode of course.
+
+ Note: there are no region parameters, because they should be erased.
+ *)
+let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
+ (ctx : C.eval_ctx) : C.eval_ctx * A.inst_fun_sig =
+ (* Generate fresh abstraction ids and create a substitution from region
+ * group ids to abstraction ids *)
+ let ctx, rg_abs_ids_bindings =
+ List.fold_left_map
+ (fun ctx rg ->
+ let ctx, abs_id = C.fresh_abstraction_id ctx in
+ (ctx, (rg.A.id, abs_id)))
+ ctx sg.regions_hierarchy
+ in
+ let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t =
+ List.fold_left
+ (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp)
+ A.RegionGroupId.Map.empty rg_abs_ids_bindings
+ in
+ let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id =
+ A.RegionGroupId.Map.find rg_id asubst_map
+ in
+ (* Generate fresh regions and their substitutions *)
+ let ctx, _, rsubst, _ =
+ Subst.fresh_regions_with_substs sg.region_params ctx
+ in
+ (* Generate the type substitution
+ * Note that we need the substitution to map the type variables to
+ * [rty] types (not [ety]). In order to do that, we convert the
+ * type parameters to types with regions. This is possible only
+ * if those types don't contain any regions.
+ * This is a current limitation of the analysis: there is still some
+ * work to do to properly handle full type parametrization.
+ * *)
+ let rtype_params = List.map ety_no_regions_to_rty type_params in
+ let tsubst =
+ Subst.make_type_subst
+ (List.map (fun v -> v.T.index) sg.type_params)
+ rtype_params
+ in
+ (* Substitute the signature *)
+ let inst_sig = Subst.substitute_signature asubst rsubst tsubst sg in
+ (* Return *)
+ (ctx, inst_sig)
+
(** Evaluate a statement *)
let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
: (C.eval_ctx * statement_eval_res) eval_result list =
@@ -661,7 +709,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx)
let ctx = C.ctx_push_var ctx ret_var (C.mk_bottom ret_var.var_ty) in
(* 2. Push the input values *)
- let input_locals, locals = Utilities.list_split_at locals def.A.arg_count in
+ let input_locals, locals = Utils.list_split_at locals def.A.arg_count in
let inputs = List.combine input_locals args in
(* Note that this function checks that the variables and their values
have the same type (this is important) *)
@@ -697,43 +745,9 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
(* Retrieve the (correctly instantiated) signature *)
let def = C.ctx_lookup_fun_def ctx fid in
let sg = def.A.signature in
- (* Generate fresh abstraction ids and create a substitution from region
- * group ids to abstraction ids *)
- let ctx, rg_abs_ids_bindings =
- List.fold_left_map
- (fun ctx rg ->
- let ctx, abs_id = C.fresh_abstraction_id ctx in
- (ctx, (rg.A.id, abs_id)))
- ctx sg.regions_hierarchy
- in
- let asubst_map : V.AbstractionId.id A.RegionGroupId.Map.t =
- List.fold_left
- (fun mp (rg_id, abs_id) -> A.RegionGroupId.Map.add rg_id abs_id mp)
- A.RegionGroupId.Map.empty rg_abs_ids_bindings
- in
- let asubst (rg_id : A.RegionGroupId.id) : V.AbstractionId.id =
- A.RegionGroupId.Map.find rg_id asubst_map
- in
- (* Generate fresh regions and their substitutions *)
- let ctx, _, rsubst, _ =
- Subst.fresh_regions_with_substs sg.region_params ctx
- in
- (* Generate the type substitution
- * Note that we need the substitution to map the type variables to
- * [rty] types (not [ety]). In order to do that, we convert the
- * type parameters to types with regions. This is possible only
- * if those types don't contain any regions.
- * This is a current limitation of the analysis: there is still some
- * work to do to properly handle full type parametrization.
- * *)
- let rtype_params = List.map ety_no_regions_to_rty type_params in
- let tsubst =
- Subst.make_type_subst
- (List.map (fun v -> v.T.index) sg.type_params)
- rtype_params
- in
- (* Substitute the signature *)
- let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
+ (* Instantiate the signature and introduce fresh abstraction and region ids
+ * while doing so *)
+ let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
(* Sanity check *)
assert (List.length args = def.A.arg_count);
(* Evaluate the function call *)
@@ -755,10 +769,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
mk_fresh_symbolic_proj_comp T.RegionId.Set.empty ret_sv_ty ctx
in
let ret_value = mk_typed_value_from_proj_comp ret_spc in
- let ret_av = V.ASymbolic (V.AProjLoans ret_spc.V.svalue) in
- let ret_av : V.typed_avalue =
- { V.value = ret_av; V.ty = ret_spc.V.svalue.V.sv_ty }
- in
+ let ret_av = mk_aproj_loans_from_symbolic_value ret_spc.V.svalue in
(* Evaluate the input operands *)
let ctx, args = eval_operands config ctx args in
let args_with_rtypes = List.combine args inst_sg.A.inputs in
@@ -768,8 +779,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(fun ((arg, rty) : V.typed_value * T.rty) ->
arg.V.ty = Subst.erase_regions rty)
args_with_rtypes);
- (* Generate the abstractions from the region groups and add them to the context *)
- let gen_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
+ (* Create the abstractions from the region groups and add them to the context *)
+ let create_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx =
let abs_id = rg.A.id in
let parents =
List.fold_left
@@ -797,7 +808,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(* Return *)
ctx
in
- let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in
+ let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in
(* Move the return value to its destination *)
let ctx = assign_to_place config ctx ret_value dest in
(* Synthesis *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 5e0375d0..cc54cd24 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -37,11 +37,17 @@ let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
{ var_id; projection = [] }
+(** Create a fresh symbolic value *)
+let mk_fresh_symbolic_value (ty : T.rty) (ctx : C.eval_ctx) :
+ C.eval_ctx * V.symbolic_value =
+ let ctx, sv_id = C.fresh_symbolic_value_id ctx in
+ let svalue = { V.sv_id; V.sv_ty = ty } in
+ (ctx, svalue)
+
(** Create a fresh symbolic proj comp *)
let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty)
(ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp =
- let ctx, sv_id = C.fresh_symbolic_value_id ctx in
- let svalue = { V.sv_id; V.sv_ty = ty } in
+ let ctx, svalue = mk_fresh_symbolic_value ty ctx in
let sv = { V.svalue; rset_ended = ended_regions } in
(ctx, sv)
@@ -64,12 +70,24 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
mk_typed_value_from_proj_comp spc
-let mk_aproj_loans_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_avalue =
- let ty = sv.V.svalue.V.sv_ty in
- let proj = V.AProjLoans sv.V.svalue in
+let mk_aproj_loans_from_proj_comp (spc : V.symbolic_proj_comp) : V.typed_avalue
+ =
+ let ty = spc.V.svalue.V.sv_ty in
+ let proj = V.AProjLoans spc.V.svalue in
let value = V.ASymbolic proj in
{ V.value; ty }
+(** Create a Loans projector from a symbolic value.
+
+ Initializes the set of ended regions with `empty`.
+ *)
+let mk_aproj_loans_from_symbolic_value (svalue : V.symbolic_value) :
+ V.typed_avalue =
+ let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
+ let av = V.ASymbolic (V.AProjLoans spc.V.svalue) in
+ let av : V.typed_avalue = { V.value = av; V.ty = svalue.V.sv_ty } in
+ av
+
(** TODO: move *)
let borrow_is_asb (bid : V.BorrowId.id) (asb : V.abstract_shared_borrow) : bool
=
diff --git a/src/Print.ml b/src/Print.ml
index 90f3946b..de1952e1 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -843,7 +843,7 @@ module CfimAst = struct
(* Arguments *)
let inputs = List.tl def.locals in
- let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in
+ let inputs, _aux_locals = Utils.list_split_at inputs def.arg_count in
let args = List.combine inputs sg.inputs in
let args =
List.map
diff --git a/src/Utilities.ml b/src/Utilities.ml
deleted file mode 100644
index 6452d56f..00000000
--- a/src/Utilities.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(* Split a list at a given index [i] (the first list contains all the elements
- up to element of index [i], not included, the second one contains the remaining
- elements. Note that the first returned list has length [i].
- *)
-let rec list_split_at (ls : 'a list) (i : int) =
- if i < 0 then raise (Invalid_argument "list_split_at take positive integers")
- else if i = 0 then ([], ls)
- else
- match ls with
- | [] ->
- raise
- (Failure
- "The int given to list_split_at should be <= the list's length")
- | x :: ls' ->
- let ls1, ls2 = list_split_at ls' (i - 1) in
- (x :: ls1, ls2)
diff --git a/src/Utils.ml b/src/Utils.ml
index a285e869..16ee7252 100644
--- a/src/Utils.ml
+++ b/src/Utils.ml
@@ -1,3 +1,20 @@
+(* Split a list at a given index [i] (the first list contains all the elements
+ up to element of index [i], not included, the second one contains the remaining
+ elements. Note that the first returned list has length [i].
+*)
+let rec list_split_at (ls : 'a list) (i : int) =
+ if i < 0 then raise (Invalid_argument "list_split_at take positive integers")
+ else if i = 0 then ([], ls)
+ else
+ match ls with
+ | [] ->
+ raise
+ (Failure
+ "The int given to list_split_at should be <= the list's length")
+ | x :: ls' ->
+ let ls1, ls2 = list_split_at ls' (i - 1) in
+ (x :: ls1, ls2)
+
exception Found
(** Utility exception
diff --git a/src/main.ml b/src/main.ml
index 2d2518c7..b4537c3a 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -46,4 +46,4 @@ let () =
log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
(* Test the unit functions *)
- I.Test.test_all_unit_functions m.types m.functions
+ I.Test.test_unit_functions m.types m.functions