diff options
| -rw-r--r-- | src/CfimOfJson.ml | 2 | ||||
| -rw-r--r-- | src/Expressions.ml | 2 | ||||
| -rw-r--r-- | src/Interpreter.ml | 107 | ||||
| -rw-r--r-- | src/Print.ml | 5 | ||||
| -rw-r--r-- | src/main.ml | 2 |
5 files changed, 55 insertions, 63 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index f3527e17..265a4c7b 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -5,7 +5,7 @@ different from what `serde_rs` generates (because it uses [Yojson.Safe.t] and not [Yojson.Basic.t]). - TODO: we should check that the integer values are in the proper range + TODO: we should check all that the integer values are in the proper range *) open Yojson.Basic diff --git a/src/Expressions.ml b/src/Expressions.ml index 38ee1ff6..6a7e92a0 100644 --- a/src/Expressions.ml +++ b/src/Expressions.ml @@ -1,5 +1,3 @@ -(** TODO: the name "Expression" is not correct - change that *) - open Types open Values diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 53cef961..03f31aee 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -12,7 +12,6 @@ open ValuesUtils (* TODO: Change state-passing style to : st -> ... -> (st, v) *) (* TODO: check that the value types are correct when evaluating *) -(* TODO: module Type = T, etc. *) (* TODO: for debugging purposes, we might want to put use eval_ctx everywhere (rather than only env) *) @@ -2468,62 +2467,62 @@ and eval_function_body (config : C.config) (ctx : C.eval_ctx) | Unit | Break _ | Continue _ -> failwith "Inconsistent state" | Return -> Ok ctx) -(** Test a unit function (taking no arguments) by evaluating it in an empty +module Test = struct + (** Test a unit function (taking no arguments) by evaluating it in an empty environment - - TODO: put in a sub-module *) -let test_unit_function (type_defs : T.type_def list) (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 - - (* Debug *) - L.log#ldebug - (lazy ("test_unit_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 = - { - C.type_context = type_defs; - C.fun_context = fun_defs; - C.type_vars = []; - C.env = []; - C.symbolic_counter = V.SymbolicValueId.generator_zero; - C.borrow_counter = V.BorrowId.generator_zero; - } - in + let test_unit_function (type_defs : T.type_def list) + (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 + + (* Debug *) + L.log#ldebug + (lazy ("test_unit_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 = + { + C.type_context = type_defs; + C.fun_context = fun_defs; + C.type_vars = []; + C.env = []; + C.symbolic_counter = V.SymbolicValueId.generator_zero; + C.borrow_counter = V.BorrowId.generator_zero; + } + in - (* Put the (uninitialized) local variables *) - let ctx = C.ctx_push_uninitialized_vars ctx fdef.A.locals in + (* Put 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 - match eval_function_body config ctx fdef.A.body with - | Error err -> Error err - | Ok _ -> Ok () + (* Evaluate the function *) + let config = { C.mode = C.ConcreteMode; C.check_invariants = true } in + match eval_function_body config ctx fdef.A.body with + | Error err -> Error err + | Ok _ -> Ok () -(** Small helper: return true if the function is a unit function (no parameters, + (** Small helper: return true if the function is a unit function (no parameters, no arguments) - TODO: move *) -let fun_def_is_unit (def : A.fun_def) : bool = - def.A.arg_count = 0 - && List.length def.A.signature.region_params = 0 - && List.length def.A.signature.type_params = 0 - && 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) - (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 - | Error _ -> failwith "Unit test failed" - | Ok _ -> () - else () - in - List.iter test_fun fun_defs + let fun_def_is_unit (def : A.fun_def) : bool = + def.A.arg_count = 0 + && List.length def.A.signature.region_params = 0 + && List.length def.A.signature.type_params = 0 + && 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) + (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 + | Error _ -> failwith "Unit test failed" + | Ok _ -> () + else () + in + List.iter test_fun fun_defs +end diff --git a/src/Print.ml b/src/Print.ml index 6d7a6c68..99788123 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -1,5 +1,3 @@ -(* TODO: use one letter abbreviations for modules *) - open Identifiers module T = Types module TU = TypesUtils @@ -29,12 +27,9 @@ module Types = struct let assumed_ty_to_string (_ : T.assumed_ty) : string = "Box" - (* TODO: This is probably not the most OCaml-like way of doing this *) type 'r type_formatter = { r_to_string : 'r -> string; - (* TODO: remove this and put the name everywhere instead? *) type_var_id_to_string : T.TypeVarId.id -> string; - (* TODO: remove this and put the name everywhere instead? *) type_def_id_to_string : T.TypeDefId.id -> string; } diff --git a/src/main.ml b/src/main.ml index 52fd8ea4..da8f71ff 100644 --- a/src/main.ml +++ b/src/main.ml @@ -22,4 +22,4 @@ let () = log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n")); (* Test the unit functions *) - I.test_all_unit_functions m.types m.functions + I.Test.test_all_unit_functions m.types m.functions |