diff options
Diffstat (limited to '')
| -rw-r--r-- | TODO.md | 7 | ||||
| -rw-r--r-- | src/Assumed.ml | 22 | ||||
| -rw-r--r-- | src/Translate.ml | 17 | ||||
| -rw-r--r-- | src/main.ml | 5 |
4 files changed, 45 insertions, 6 deletions
@@ -15,6 +15,11 @@ backward calls (because they may panic!) - calls which don't take inputs (can happen with backward functions - for instance, if a rust function only returns shared borrows) + - monadic lets to matches + - no tuple deconstruction on returned monadic values (introduce intermediate + variables to deconstruct in two times) + - matching on values (ex.: `let Cons hd tl = ls in` ~~> + `match ls with | Nil -> Panic | Cons hd tl -> ...`) 1. reorder the branches of matches @@ -64,6 +69,8 @@ while in the case of `s1` we should ignore the outer borrow (what we give back actually has type `T`...) +10. Write "bodies" for the assumed functions. + * write a function to check that the code we are about to synthesize is in the proper subset. In particular: * borrow overwrites 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; |