summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-28 00:04:22 +0100
committerSon Ho2022-01-28 00:04:22 +0100
commitb4ecf513020b2d5bfdfb7b9e2a721feab6e6998e (patch)
tree024899cb85a6835d73d2bda5b68c986f1f7ad6f1
parent4fcc9f5ca26bec31d1c4d6ead1578e96337dd329 (diff)
Remove the Aggregated variant from SymbolicAst.meta as it is included in
the Assignment variant
-rw-r--r--src/InterpreterExpressions.ml8
-rw-r--r--src/PrintPure.ml3
-rw-r--r--src/Pure.ml4
-rw-r--r--src/SymbolicAst.ml2
-rw-r--r--src/SymbolicToPure.ml4
-rw-r--r--src/SynthesizeSymbolic.ml6
6 files changed, 3 insertions, 24 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 34bfd574..ce9489a9 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -592,9 +592,7 @@ let eval_rvalue_aggregate (config : C.config)
let ty = T.Adt (T.Tuple, [], tys) in
let aggregated : V.typed_value = { V.value = v; ty } in
(* Call the continuation *)
- let expr = cf aggregated ctx in
- (* Synthesize the symbolic AST *)
- S.synthesize_aggregated_value aggregated None expr
+ cf aggregated ctx
| E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
(* Sanity checks *)
let type_def = C.ctx_lookup_type_def ctx def_id in
@@ -613,9 +611,7 @@ let eval_rvalue_aggregate (config : C.config)
let aty = T.Adt (T.AdtId def_id, regions, types) in
let aggregated : V.typed_value = { V.value = Adt av; ty = aty } in
(* Call the continuation *)
- let expr = cf aggregated ctx in
- (* Synthesize the symbolic AST *)
- S.synthesize_aggregated_value aggregated None expr
+ cf aggregated ctx
in
(* Compose and apply *)
comp eval_ops compute cf
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 5223fb21..f78e4a97 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -340,9 +340,6 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
let meta_to_string (fmt : ast_formatter) (meta : meta) : string =
let meta =
match meta with
- | Aggregate (p, rv) ->
- let p = match p with None -> "_" | Some p -> mplace_to_string fmt p in
- "@aggregate(" ^ p ^ " := " ^ typed_rvalue_to_string fmt rv ^ ")"
| Assignment (p, rv) ->
"@assign(" ^ mplace_to_string fmt p ^ " := "
^ typed_rvalue_to_string fmt rv
diff --git a/src/Pure.ml b/src/Pure.ml
index 89748bdd..7e5aca47 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -201,9 +201,7 @@ type let_bindings =
*)
(** Meta-information stored in the AST *)
-type meta =
- | Aggregate of mplace option * typed_rvalue
- | Assignment of mplace * typed_rvalue
+type meta = Assignment of mplace * typed_rvalue
(** **Rk.:** here, [expression] is not at all equivalent to the expressions
used in CFIM. They are lambda-calculus expressions, and are thus actually
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 07afd914..4eca712a 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -50,8 +50,6 @@ type call = {
*)
type meta =
- | Aggregate of mplace option * V.typed_value
- (** We generated an aggregate value *)
| Assignment of mplace * V.typed_value
(** We generated an assignment (destination, assigned value) *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 4fa8e54c..8b31bffa 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -1246,10 +1246,6 @@ and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
let e = translate_expression e ctx in
let meta =
match meta with
- | S.Aggregate (p, rv) ->
- let p = translate_opt_mplace p in
- let rv = typed_value_to_rvalue ctx rv in
- Aggregate (p, rv)
| S.Assignment (p, rv) ->
let p = translate_mplace p in
let rv = typed_value_to_rvalue ctx rv in
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index f86d40f0..c1dcff87 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -139,12 +139,6 @@ let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
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 : mplace option)
- (expr : expression option) : expression option =
- match expr with
- | None -> None
- | Some expr -> Some (Meta (Aggregate (place, aggr_v), expr))
-
let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
expression option =
match expr with