summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterExpansion.ml12
-rw-r--r--src/InterpreterExpressions.ml5
-rw-r--r--src/InterpreterPaths.ml4
-rw-r--r--src/InterpreterStatements.ml2
-rw-r--r--src/PureMicroPasses.ml23
-rw-r--r--src/SymbolicAst.ml12
-rw-r--r--src/SymbolicToPure.ml6
-rw-r--r--src/SynthesizeSymbolic.ml42
8 files changed, 65 insertions, 41 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 77bf0bd8..625c63ef 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -265,7 +265,7 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
see
let expand_symbolic_value_shared_borrow (config : C.config)
- (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+ (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
(ref_ty : T.rty) : cm_fun =
fun cf ctx ->
(* First, replace the projectors on borrows.
@@ -381,7 +381,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
(** TODO: simplify and merge with the other expansion function *)
let expand_symbolic_value_borrow (config : C.config)
- (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+ (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
(region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) :
cm_fun =
fun cf ctx ->
@@ -426,7 +426,7 @@ let expand_symbolic_value_borrow (config : C.config)
[see_cf_l]: list of pairs (optional symbolic expansion, continuation)
*)
let apply_branching_symbolic_expansions_non_borrow (config : C.config)
- (sv : V.symbolic_value) (sv_place : SA.place option)
+ (sv : V.symbolic_value) (sv_place : SA.mplace option)
(see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun =
fun ctx ->
assert (see_cf_l <> []);
@@ -467,7 +467,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
TODO: rename [sp] to [sv]
*)
let expand_symbolic_value (config : C.config) (allow_branching : bool)
- (sp : V.symbolic_value) (sp_place : SA.place option) : cm_fun =
+ (sp : V.symbolic_value) (sp_place : SA.mplace option) : cm_fun =
fun cf ctx ->
(* Debug *)
log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
@@ -578,7 +578,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
switch. The continuation is thus for the execution *after* the switch.
*)
let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
- (sv_place : SA.place option) (int_type : T.integer_type)
+ (sv_place : SA.mplace option) (int_type : T.integer_type)
(tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun =
(* Sanity check *)
assert (sv.V.sv_ty = T.Integer int_type);
@@ -600,7 +600,7 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
(** See [expand_symbolic_value] *)
let expand_symbolic_value_no_branching (config : C.config)
- (sv : V.symbolic_value) (sv_place : SA.place option) : cm_fun =
+ (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
let allow_branching = false in
expand_symbolic_value config allow_branching sv sv_place
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 356bae2d..34bfd574 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -40,7 +40,8 @@ let expand_primitively_copyable_at_place (config : C.config)
| None -> cf ctx
| Some sv ->
let cc =
- expand_symbolic_value_no_branching config sv (Some (S.mk_place p ctx))
+ expand_symbolic_value_no_branching config sv
+ (Some (S.mk_mplace p ctx))
in
comp cc expand cf ctx
in
@@ -496,7 +497,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
let allow_branching = true in
let cc =
expand_symbolic_value config allow_branching sv
- (Some (S.mk_place p ctx))
+ (Some (S.mk_mplace p ctx))
in
(* This time the value is concrete: reevaluate *)
comp cc (eval_rvalue_discriminant_concrete config p) cf ctx
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 361ff981..bfb1aee3 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -482,7 +482,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
in
let prefix = { p with projection = proj } in
expand_symbolic_value_no_branching config sp
- (Some (Synth.mk_place prefix ctx))
+ (Some (Synth.mk_mplace prefix ctx))
| FailBottom (_, _, _) ->
(* We can't expand [Bottom] values while reading them *)
failwith "Found [Bottom] while reading a place"
@@ -512,7 +512,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
| FailSymbolic (_pe, sp) ->
(* Expand the symbolic value *)
expand_symbolic_value_no_branching config sp
- (Some (Synth.mk_place p ctx))
+ (Some (Synth.mk_mplace p ctx))
| FailBottom (remaining_pes, pe, ty) ->
(* Expand the [Bottom] value *)
fun cf ctx ->
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 16c66094..a1c58851 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -1002,7 +1002,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
mk_aproj_loans_value_from_symbolic_value regions ret_spc
in
let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in
- let dest_place = Some (S.mk_place dest ctx) in
+ let dest_place = Some (S.mk_mplace dest ctx) in
(* Evaluate the input operands *)
let cc = eval_operands config args in
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index f35ee2d6..cd64a288 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -33,11 +33,30 @@ open Pure
}
}
```
- If `ls` maps to a symbolic value upon evaluating the match in symbolic
+ If `ls` maps to a symbolic value `s0` 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 symbolic values we introduce for the fields of `Cons`!
+ Let's imagine we have (for the `Cons` branch): `s0 ~~> Cons s1 s2`.
+ The assigments lead to the following binding in the evaluation context:
+ ```
+ x -> s1
+ hd -> s2
+ ```
+
+ If at any moment we use `x` (as an operand to a function, to return,
+ etc.) we ...
+ TODO: finish explanations
+ TODO: meta-information for:
+ - unop
+ - binop
+ - assignments
+ - discriminant
+ - ...
+
the subsequent assignments actually give us the naming information we
were looking for.
+ - TODO: temporaries for binops which can fail/have preconditions
+ - TODO: reborrows just before calling functions.
*)
let compute_pretty_names () = ()
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index a3aedeab..c9ab87e0 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -9,7 +9,7 @@ module V = Values
module E = Expressions
module A = CfimAst
-type place = {
+type mplace = {
bv : Contexts.binder;
(** It is important that we store the binder, and not just the variable id,
because the most important information in a place is the name of the
@@ -18,7 +18,7 @@ type place = {
projection : E.projection;
(** We store the projection because we can, but it is actually not that useful *)
}
-(** In this module, [place] is meta information.
+(** "Meta"-place: a place stored as meta-data.
Whenever we need to introduce new symbolic variables, for instance because
of symbolic expansions, we try to store a "place", which gives information
@@ -40,9 +40,9 @@ type call = {
abstractions : V.AbstractionId.id list;
type_params : T.ety list;
args : V.typed_value list;
- args_places : place option list; (** Meta information *)
+ args_places : mplace option list; (** Meta information *)
dest : V.symbolic_value;
- dest_place : place option; (** Meta information *)
+ dest_place : mplace option; (** Meta information *)
}
(** **Rk.:** here, [expression] is not at all equivalent to the expressions
@@ -58,7 +58,7 @@ type expression =
| Panic
| FunCall of call * expression
| EndAbstraction of V.abs * expression
- | Expansion of place option * V.symbolic_value * expansion
+ | Expansion of mplace option * V.symbolic_value * expansion
(** Expansion of a symbolic value.
The place is "meta": it gives the path to the symbolic value (if available)
@@ -93,5 +93,5 @@ and expansion =
*)
and meta =
- | Aggregate of place option * V.typed_value
+ | Aggregate of mplace option * V.typed_value
(** We generated an aggregate value *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 5a3b3e96..63d0df1d 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -743,12 +743,12 @@ let translate_mprojection (p : E.projection) : projection =
List.filter_map translate_mprojection_elem p
(** Translate a "meta"-place *)
-let translate_mplace (p : S.place) : mplace =
+let translate_mplace (p : S.mplace) : mplace =
let name = p.bv.name in
let projection = translate_mprojection p.projection in
{ name; projection }
-let translate_opt_mplace (p : S.place option) : mplace option =
+let translate_opt_mplace (p : S.mplace option) : mplace option =
match p with None -> None | Some p -> Some (translate_mplace p)
(** Explore an abstraction value and convert it to a given back value
@@ -1118,7 +1118,7 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
e ))
given_back_inputs e
-and translate_expansion (p : S.place option) (sv : V.symbolic_value)
+and translate_expansion (p : S.mplace option) (sv : V.symbolic_value)
(exp : S.expansion) (ctx : bs_ctx) : expression =
(* Translate the scrutinee *)
let scrutinee_var = lookup_var_for_symbolic_value sv ctx in
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 7050c14b..7ba1da7f 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -5,22 +5,23 @@ module E = Expressions
module A = CfimAst
open SymbolicAst
-let mk_place (p : E.place) (ctx : Contexts.eval_ctx) : place =
+let mk_mplace (p : E.place) (ctx : Contexts.eval_ctx) : mplace =
let bv = Contexts.ctx_lookup_binder ctx p.var_id in
{ bv; projection = p.projection }
-let mk_opt_place (p : E.place option) (ctx : Contexts.eval_ctx) : place option =
- match p with None -> None | Some p -> Some (mk_place p ctx)
+let mk_opt_mplace (p : E.place option) (ctx : Contexts.eval_ctx) : mplace option
+ =
+ match p with None -> None | Some p -> Some (mk_mplace p ctx)
let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) :
- place option =
+ mplace option =
match op with
- | E.Copy p | E.Move p -> Some (mk_place p ctx)
+ | E.Copy p | E.Move p -> Some (mk_mplace p ctx)
| E.Constant _ -> None
-let synthesize_symbolic_expansion (sv : V.symbolic_value) (place : place option)
- (seel : V.symbolic_expansion option list) (exprl : expression list option) :
- expression option =
+let synthesize_symbolic_expansion (sv : V.symbolic_value)
+ (place : mplace option) (seel : V.symbolic_expansion option list)
+ (exprl : expression list option) : expression option =
match exprl with
| None -> None
| Some exprl ->
@@ -87,15 +88,15 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value) (place : place option)
Some (Expansion (place, sv, expansion))
let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
- (place : place option) (see : V.symbolic_expansion)
+ (place : mplace option) (see : V.symbolic_expansion)
(expr : expression option) : expression option =
let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
synthesize_symbolic_expansion sv place [ Some see ] exprl
let synthesize_function_call (call_id : call_id)
(abstractions : V.AbstractionId.id list) (type_params : T.ety list)
- (args : V.typed_value list) (args_places : place option list)
- (dest : V.symbolic_value) (dest_place : place option)
+ (args : V.typed_value list) (args_places : mplace option list)
+ (dest : V.symbolic_value) (dest_place : mplace option)
(expr : expression option) : expression option =
match expr with
| None -> None
@@ -116,26 +117,29 @@ let synthesize_function_call (call_id : call_id)
let synthesize_regular_function_call (fun_id : A.fun_id)
(call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
(type_params : T.ety list) (args : V.typed_value list)
- (args_places : place option list) (dest : V.symbolic_value)
- (dest_place : place option) (expr : expression option) : expression option =
+ (args_places : mplace option list) (dest : V.symbolic_value)
+ (dest_place : mplace option) (expr : expression option) : expression option
+ =
synthesize_function_call
(Fun (fun_id, call_id))
abstractions type_params args args_places dest dest_place expr
let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
- (arg_place : place option) (dest : V.symbolic_value)
- (dest_place : place option) (expr : expression option) : expression option =
+ (arg_place : mplace option) (dest : V.symbolic_value)
+ (dest_place : mplace option) (expr : expression option) : expression option
+ =
synthesize_function_call (Unop unop) [] [] [ arg ] [ arg_place ] dest
dest_place expr
let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
- (arg0_place : place option) (arg1 : V.typed_value)
- (arg1_place : place option) (dest : V.symbolic_value)
- (dest_place : place option) (expr : expression option) : expression option =
+ (arg0_place : mplace option) (arg1 : V.typed_value)
+ (arg1_place : mplace option) (dest : V.symbolic_value)
+ (dest_place : mplace option) (expr : expression option) : expression option
+ =
synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ]
[ arg0_place; arg1_place ] dest dest_place expr
-let synthesize_aggregated_value (aggr_v : V.typed_value) (place : place option)
+let synthesize_aggregated_value (aggr_v : V.typed_value) (place : mplace option)
(expr : expression option) : expression option =
match expr with
| None -> None
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 20:21:14 +0000