diff options
| -rw-r--r-- | TODO.md | 11 | ||||
| -rw-r--r-- | src/Identifiers.ml | 2 | ||||
| -rw-r--r-- | src/Interpreter.ml | 7 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 2 | ||||
| -rw-r--r-- | src/Print.ml | 2 | ||||
| -rw-r--r-- | src/Utils.ml | 17 |
7 files changed, 17 insertions, 26 deletions
@@ -11,6 +11,8 @@ 3. fix the static regions (with projectors) +4. Add a `Collections.ml` file, with `Map` and `Set` + * write an interesting example to study with Jonathan * add option for: `allow_borrow_overwrites_on_input_values` @@ -58,6 +60,15 @@ * Some variables have the same name. It might be good to also print their id to disambiguate? +* it would be good to find a "core", which implements the rules (like + "end_borrow") and on top of which we build more complex functions which + chose in which order to apply the rules, etc. This way we would make very + explicit where we need to insert sanity checks, what the preconditions are, + where invariants might be broken, etc. + +* intensively test with PLT-redex + +* remove the config parameters when they are useless # DONE diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 56edc238..4ec5aab7 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -1,3 +1,5 @@ +open Collections + (** Signature for a module describing an identifier. We often need identifiers (for definitions, variables, etc.) and in diff --git a/src/Interpreter.ml b/src/Interpreter.ml index c998214b..2f0f52af 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2,15 +2,10 @@ module L = Logging module T = Types module A = CfimAst module M = Modules -open Utils open InterpreterUtils open InterpreterExpressions open InterpreterStatements -(* TODO: check that the value types are correct when evaluating *) -(* TODO: for debugging purposes, we might want to put use eval_ctx everywhere - (rather than only env) *) - (* TODO: it would be good to find a "core", which implements the rules (like "end_borrow") and on top of which we build more complex functions which chose in which order to apply the rules, etc. This way we would make very @@ -98,7 +93,7 @@ module Test = struct (* 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 + Collections.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 diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 8cf2b747..4482a507 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -413,7 +413,7 @@ let expand_bottom_value_from_projection (config : C.config) during whose evaluation we got stuck *) let projection' = fst - (Utils.list_split_at p.projection + (Collections.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 885d1bdc..1b06dd7f 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -829,7 +829,7 @@ and eval_local_function_call_concrete (config : C.config) (ctx : C.eval_ctx) let ctx = C.ctx_push_var ctx ret_var (mk_bottom ret_var.var_ty) in (* 2. Push the input values *) - let input_locals, locals = Utils.list_split_at locals def.A.arg_count in + let input_locals, locals = Collections.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) *) diff --git a/src/Print.ml b/src/Print.ml index 8067eae3..000874fe 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -863,7 +863,7 @@ module CfimAst = struct (* Arguments *) let inputs = List.tl def.locals in - let inputs, _aux_locals = Utils.list_split_at inputs def.arg_count in + let inputs, _aux_locals = Collections.List.split_at inputs def.arg_count in let args = List.combine inputs sg.inputs in let args = List.map diff --git a/src/Utils.ml b/src/Utils.ml index 16ee7252..a285e869 100644 --- a/src/Utils.ml +++ b/src/Utils.ml @@ -1,20 +1,3 @@ -(* 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 |