diff options
| -rw-r--r-- | src/PrintPure.ml | 2 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 43 | ||||
| -rw-r--r-- | src/Translate.ml | 1 |
3 files changed, 45 insertions, 1 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml index e5b58b9f..532278ea 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -227,7 +227,7 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string) let place_to_string (fmt : ast_formatter) (p : place) : string = (* TODO: improve that *) - let var = "@" ^ fmt.var_id_to_string p.var in + let var = fmt.var_id_to_string p.var in projection_to_string fmt var p.projection let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml new file mode 100644 index 00000000..f35ee2d6 --- /dev/null +++ b/src/PureMicroPasses.ml @@ -0,0 +1,43 @@ +(** The following module defines micro-passes which operate on the pure AST *) + +open Pure + +(** This function computes pretty names for the variables in the pure AST. It + relies on the "meta"-place information in the AST to generate naming + constraints. + + The way it works is as follows: + - we only modify the names of the unnamed variables + - whenever we see an rvalue/lvalue which is exactly an unnamed variable, + and this value is linked to some meta-place information which contains + a name and an empty path, we consider we should use this name + + For instance, the following situations happen: + - let's say we evaluate: + ``` + match (ls : List<T>) { + List::Cons(x, hd) => { + ... + } + } + ``` + + Actually, in MIR, we get: + ``` + tmp = discriminant(ls); + switch tmp { + 0 => { + x = (ls as Cons).0; + hd = (ls as Cons).1; + ... + } + } + ``` + If `ls` maps to a symbolic value upon evaluating the match in symbolic + mode, we expand this value upon evaluating `tmp = discriminant(ls)`. + However, at this point, we don't know which should be the names of + the symbolic values we introduce for the fields of `Cons`! Still, + the subsequent assignments actually give us the naming information we + were looking for. + *) +let compute_pretty_names () = () diff --git a/src/Translate.ml b/src/Translate.ml index 9de07519..e3f7bbb2 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -5,6 +5,7 @@ module T = Types module A = CfimAst module M = Modules module SA = SymbolicAst +module Micro = PureMicroPasses (** The local logger *) let log = L.translate_log |