diff options
Diffstat (limited to '')
| -rw-r--r-- | TODO.md | 9 | ||||
| -rw-r--r-- | src/Interpreter.ml | 4 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 11 |
3 files changed, 19 insertions, 5 deletions
@@ -1,6 +1,6 @@ # TODO -0. add a meta-value in shared borrows to carry the shared value +0. sanity checks in symbolic to pure! 0. update the end borrows internal to abstractions to not introduce a Bottom @@ -8,6 +8,11 @@ 0. remove ABottom from avalue +0. micro-passes for pure: + - remove unused variables + - remove useless function calls *if* they are followed by associated + backward calls (because they may panic!) + 1. reorder the branches of matches 1. stateful maps/sets modules (hashtbl?) @@ -154,3 +159,5 @@ * fix the static regions (with projectors) Before that, introduce a sanity check to make sure we don't use static regions. + +* add a meta-value in shared borrows to carry the shared value diff --git a/src/Interpreter.ml b/src/Interpreter.ml index fbb7ef9b..d3e30519 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -47,8 +47,8 @@ module Test = struct 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. + Abstractions are introduced for the regions present in the function + signature. *) let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def) : C.eval_ctx = diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index a575e835..afca9398 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -856,9 +856,11 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : let inputs = List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs ] in + (* TODO: check that the inputs have the proper number and the proper type *) (* Retrieve the values given back by this function: those are the output * values *) let ctx, outputs = abs_to_given_back abs ctx in + (* TODO: check that the outputs have the proper number and the proper type *) (* Retrieve the function id, and register the function call in the context * if necessary *) let ctx, func = bs_ctx_register_backward_call abs ctx in @@ -906,9 +908,14 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) : assert (consumed = []); (* Retrieve the values given back upon ending this abstraction *) let ctx, given_back = abs_to_given_back abs ctx in - (* Link the inputs to those given back values - note that we must - * have the same number of values *) + (* Link the inputs to those given back values - note that this also + * checks we have the same number of values, of course *) let given_back_inputs = List.combine given_back inputs in + (* Sanity check *) + List.iter + (fun ((given_back, input) : typed_lvalue * var) -> + assert (given_back.ty = input.ty)) + given_back_inputs; (* Translate the next expression *) let e = translate_expression e ctx in (* Generate the assignments *) |