summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Assumed.ml22
-rw-r--r--src/Translate.ml17
-rw-r--r--src/main.ml5
3 files changed, 38 insertions, 6 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml
index fd11f30b..0e05e5b9 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -5,6 +5,28 @@
happens that we move a value out of a box before freeing this box).
Semantically speaking, we thus handle `Box::free` as a value drop and
not as a function call, and thus never need its signature.
+
+ TODO: implementing the concrete evaluation functions for the assumed
+ functions is really annoying (see
+ [InterpreterStatements.eval_non_local_function_call_concrete]).
+ I think it should be possible, in most situations, to write bodies which
+ model the behaviour of those unsafe functions. For instance, `Box::deref_mut`
+ should simply be:
+ ```
+ fn deref_mut<'a, T>(x : &'a mut Box<T>) -> &'a mut T {
+ &mut ( *x ) // box dereferencement is a primitive operation
+ }
+ ```
+
+ For vectors, we could "cheat" by using the index as a field index (vectors
+ would be encoded as ADTs with a variable number of fields). Of course, it
+ would require a bit of engineering, but it would probably be quite lightweight
+ in the end.
+ ```
+ Vec::get_mut<'a,T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T {
+ &mut ( ( *x ).i )
+ }
+ ```
*)
module T = Types
diff --git a/src/Translate.ml b/src/Translate.ml
index 043ed375..ecc97ed1 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -1,4 +1,3 @@
-open Errors
open InterpreterStatements
open Interpreter
module L = Logging
@@ -41,10 +40,14 @@ let translate_function_to_symbolics (config : C.partial_config)
(forward, backwards)
(** Translate a function, by generating its forward and backward translations. *)
-let translate_function (config : C.partial_config)
+let translate_function_to_pure (config : C.partial_config)
(type_context : C.type_context) (fun_context : C.fun_context)
(fun_sigs : Pure.fun_sig SymbolicToPure.RegularFunIdMap.t)
(fdef : A.fun_def) : pure_fun_translation =
+ (* Debug *)
+ log#ldebug
+ (lazy ("translate_function_to_pure: " ^ Print.name_to_string fdef.A.name));
+
let def_id = fdef.def_id in
(* Compute the symbolic ASTs *)
@@ -144,6 +147,9 @@ let translate_function (config : C.partial_config)
let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
Pure.type_def T.TypeDefId.Map.t * pure_fun_translation A.FunDefId.Map.t =
+ (* Debug *)
+ log#ldebug (lazy "translate_module_to_pure");
+
(* Compute the type and function contexts *)
let type_context, fun_context = compute_type_fun_contexts m in
@@ -165,11 +171,12 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
in
(* Translate all the functions *)
- let translations =
+ let pure_translations =
List.map
(fun (fdef : A.fun_def) ->
( fdef.def_id,
- translate_function config type_context fun_context fun_sigs fdef ))
+ translate_function_to_pure config type_context fun_context fun_sigs
+ fdef ))
m.functions
in
@@ -177,7 +184,7 @@ let translate_module_to_pure (config : C.partial_config) (m : M.cfim_module) :
let fun_defs =
List.fold_left
(fun m (def_id, trans) -> A.FunDefId.Map.add def_id trans m)
- A.FunDefId.Map.empty translations
+ A.FunDefId.Map.empty pure_translations
in
(* Return *)
diff --git a/src/main.ml b/src/main.ml
index aca1978c..46b54d55 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -54,6 +54,8 @@ let () =
expansion_log#set_level EL.Debug;
borrows_log#set_level EL.Debug;
invariants_log#set_level EL.Warning;
+ symbolic_to_pure_log#set_level EL.Debug;
+ translate_log#set_level EL.Debug;
(* Load the module *)
let json = Yojson.Basic.from_file !filename in
match cfim_module_of_json json with
@@ -73,7 +75,8 @@ let () =
(* Test the unit functions with the concrete interpreter *)
I.Test.test_unit_functions config m;
- (* Evaluate the symbolic interpreter on the functions - TODO: remove *)
+ (* Evaluate the symbolic interpreter on the functions, ignoring the
+ * functions which contain loops - TODO: remove *)
let synthesize = true in
I.Test.test_functions_symbolic config synthesize m;