summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/Pure.ml1
-rw-r--r--compiler/PureMicroPasses.ml2
-rw-r--r--compiler/SymbolicToPure.ml70
-rw-r--r--compiler/SynthesizeSymbolic.ml2
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v12
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v12
-rw-r--r--tests/coq/misc/Loops.v38
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst6
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst6
-rw-r--r--tests/fstar/misc/Loops.Funs.fst20
10 files changed, 106 insertions, 63 deletions
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 777d4308..912e05fb 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -530,6 +530,7 @@ and meta =
| SymbolicAssignment of (var_id[@opaque]) * mvalue
(** Informationg linking a variable (from the pure AST) to an
expression.
+
We use this to guide the heuristics which derive pretty names.
*)
| MPlace of mplace (** Meta-information about the origin of a value *)
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index e670570b..3614487e 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1723,6 +1723,8 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_decl) :
^ Print.option_to_string T.RegionGroupId.to_string def.back_id
^ ")"));
+ log#ldebug (lazy ("original decl:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
+
(* First, find names for the variables which are unnamed *)
let def = compute_pretty_names def in
log#ldebug
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 531a13e9..c6ef4297 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -914,6 +914,13 @@ let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
| _ -> raise (Failure "Unreachable"))
| _ -> v
+(** Translate a symbolic value *)
+let symbolic_value_to_texpression (ctx : bs_ctx) (sv : V.symbolic_value) :
+ texpression =
+ (* Translate the type *)
+ let var = lookup_var_for_symbolic_value sv ctx in
+ mk_texpression_from_var var
+
(** Translate a typed value.
It is used, for instance, on values used as inputs for function calls.
@@ -988,9 +995,7 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (ectx : C.eval_ctx)
| V.MutBorrow (_, v) ->
(* Borrows are the identity in the extraction *)
translate v)
- | Symbolic sv ->
- let var = lookup_var_for_symbolic_value sv ctx in
- mk_texpression_from_var var
+ | Symbolic sv -> symbolic_value_to_texpression ctx sv
in
(* Debugging *)
log#ldebug
@@ -1288,6 +1293,14 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
let abs_ancestors = list_ancestor_abstractions ctx abs call_id in
(call_info.forward, abs_ancestors)
+(** Add meta-information to an expression *)
+let mk_meta_symbolic_assignments (vars : var list) (values : texpression list)
+ (e : texpression) : texpression =
+ let var_values = List.combine vars values in
+ List.fold_right
+ (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+ var_values e
+
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
match e with
| S.Return (ectx, opt_v) -> translate_return ectx opt_v ctx
@@ -1891,8 +1904,10 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
need to *transmit* to the loop backward function): they are not the
values consumed upon ending the abstraction (i.e., we don't use
[abs_to_consumed]) *)
- let back_inputs = T.RegionGroupId.Map.find rg_id ctx.backward_inputs in
- let back_inputs = List.map mk_texpression_from_var back_inputs in
+ let back_inputs_vars =
+ T.RegionGroupId.Map.find rg_id ctx.backward_inputs
+ in
+ let back_inputs = List.map mk_texpression_from_var back_inputs_vars in
(* If the function is stateful:
* - add the state input argument
* - generate a fresh state variable for the returned state
@@ -1953,7 +1968,39 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
* a value containing mutable borrows, which can't be the case... *)
assert (List.length inputs = List.length fwd_inputs);
next_e)
- else mk_let effect_info.can_fail output call next_e
+ else
+ (* Add meta-information - this is slightly hacky: we look at the
+ values consumed by the abstraction (note that those come from
+ *before* we applied the fixed-point context) and use them to
+ guide the naming of the output vars.
+
+ Also, we need to convert the backward outputs from patterns to
+ variables.
+
+ Finally, in practice, this works well only for loop bodies:
+ we do this only in this case.
+ TODO: improve the heuristics, to give weight to the hints for
+ instance.
+ *)
+ let next_e =
+ if ctx.inside_loop then
+ let consumed_values = abs_to_consumed ctx ectx abs in
+ let var_values = List.combine outputs consumed_values in
+ let var_values =
+ List.filter_map
+ (fun (var, v) ->
+ match var.Pure.value with
+ | PatVar (var, _) -> Some (var, v)
+ | _ -> None)
+ var_values
+ in
+ let vars, values = List.split var_values in
+ mk_meta_symbolic_assignments vars values next_e
+ else next_e
+ in
+
+ (* Create the let-binding *)
+ mk_let effect_info.can_fail output call next_e
and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
(e : S.expression) (ctx : bs_ctx) : texpression =
@@ -2335,16 +2382,7 @@ and translate_forward_end (ectx : C.eval_ctx)
We then remove all the meta information from the body *before* calling
{!PureMicroPasses.decompose_loops}.
*)
- let e =
- let var_values = List.combine loop_info.input_vars org_args in
- List.fold_right
- (fun (var, arg) e ->
- mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
- var_values e
- in
-
- (* Return *)
- e
+ mk_meta_symbolic_assignments loop_info.input_vars org_args e
and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 976b781d..6668c043 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -20,6 +20,8 @@ let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) :
| E.Copy p | E.Move p -> Some (mk_mplace p ctx)
| E.Constant _ -> None
+let mk_meta (m : meta) (e : expression) : expression = Meta (m, e)
+
let synthesize_symbolic_expansion (sv : V.symbolic_value)
(place : mplace option) (seel : V.symbolic_expansion option list)
(el : expression list option) : expression option =
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 9c65fb46..0d55b171 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -131,8 +131,8 @@ Fixpoint hash_map_insert_in_list_loop_back
if ckey s= key
then Return (ListCons ckey value tl)
else (
- l <- hash_map_insert_in_list_loop_back T n0 key value tl;
- Return (ListCons ckey cvalue l))
+ tl0 <- hash_map_insert_in_list_loop_back T n0 key value tl;
+ Return (ListCons ckey cvalue tl0))
| ListNil => let l := ListNil in Return (ListCons key value l)
end
end
@@ -365,8 +365,8 @@ Fixpoint hash_map_get_mut_in_list_loop_back
if ckey s= key
then Return (ListCons ckey ret tl)
else (
- l <- hash_map_get_mut_in_list_loop_back T n0 tl key ret;
- Return (ListCons ckey cvalue l))
+ tl0 <- hash_map_get_mut_in_list_loop_back T n0 tl key ret;
+ Return (ListCons ckey cvalue tl0))
| ListNil => Fail_ Failure
end
end
@@ -448,8 +448,8 @@ Fixpoint hash_map_remove_from_list_loop_back
| ListNil => Fail_ Failure
end
else (
- l <- hash_map_remove_from_list_loop_back T n0 key tl;
- Return (ListCons ckey t l))
+ tl0 <- hash_map_remove_from_list_loop_back T n0 key tl;
+ Return (ListCons ckey t tl0))
| ListNil => Return ListNil
end
end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 94a9e6a5..670e527a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -139,8 +139,8 @@ Fixpoint hashmap_hash_map_insert_in_list_loop_back
if ckey s= key
then Return (HashmapListCons ckey value tl)
else (
- l <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
- Return (HashmapListCons ckey cvalue l))
+ tl0 <- hashmap_hash_map_insert_in_list_loop_back T n0 key value tl;
+ Return (HashmapListCons ckey cvalue tl0))
| HashmapListNil =>
let l := HashmapListNil in Return (HashmapListCons key value l)
end
@@ -391,8 +391,8 @@ Fixpoint hashmap_hash_map_get_mut_in_list_loop_back
if ckey s= key
then Return (HashmapListCons ckey ret tl)
else (
- l <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
- Return (HashmapListCons ckey cvalue l))
+ tl0 <- hashmap_hash_map_get_mut_in_list_loop_back T n0 tl key ret;
+ Return (HashmapListCons ckey cvalue tl0))
| HashmapListNil => Fail_ Failure
end
end
@@ -490,8 +490,8 @@ Fixpoint hashmap_hash_map_remove_from_list_loop_back
| HashmapListNil => Fail_ Failure
end
else (
- l <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
- Return (HashmapListCons ckey t l))
+ tl0 <- hashmap_hash_map_remove_from_list_loop_back T n0 key tl;
+ Return (HashmapListCons ckey t tl0))
| HashmapListNil => Return HashmapListNil
end
end
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index ec77e4dd..bcbfc8df 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -147,8 +147,8 @@ Fixpoint list_nth_mut_loop_loop_back
then Return (ListCons ret tl)
else (
i0 <- u32_sub i 1%u32;
- l <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
- Return (ListCons x l))
+ tl0 <- list_nth_mut_loop_loop_back T n0 tl i0 ret;
+ Return (ListCons x tl0))
| ListNil => Fail_ Failure
end
end
@@ -217,7 +217,7 @@ Fixpoint get_elem_mut_loop_back
| ListCons y tl =>
if y s= x
then Return (ListCons ret tl)
- else (l <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y l))
+ else (tl0 <- get_elem_mut_loop_back n0 x tl ret; Return (ListCons y tl0))
| ListNil => Fail_ Failure
end
end
@@ -307,8 +307,8 @@ Fixpoint list_nth_mut_loop_with_id_loop_back
then Return (ListCons ret tl)
else (
i0 <- u32_sub i 1%u32;
- l <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
- Return (ListCons x l))
+ tl0 <- list_nth_mut_loop_with_id_loop_back T n0 i0 tl ret;
+ Return (ListCons x tl0))
| ListNil => Fail_ Failure
end
end
@@ -395,8 +395,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'a
then Return (ListCons ret tl0)
else (
i0 <- u32_sub i 1%u32;
- l <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
- Return (ListCons x0 l))
+ tl00 <- list_nth_mut_loop_pair_loop_back'a T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 tl00))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
@@ -428,8 +428,8 @@ Fixpoint list_nth_mut_loop_pair_loop_back'b
then Return (ListCons ret tl1)
else (
i0 <- u32_sub i 1%u32;
- l <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
- Return (ListCons x1 l))
+ tl10 <- list_nth_mut_loop_pair_loop_back'b T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 tl10))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
@@ -527,8 +527,8 @@ Fixpoint list_nth_mut_loop_pair_merge_loop_back
else (
i0 <- u32_sub i 1%u32;
p <- list_nth_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
- let (l, l0) := p in
- Return (ListCons x0 l, ListCons x1 l0))
+ let (tl00, tl10) := p in
+ Return (ListCons x0 tl00, ListCons x1 tl10))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
@@ -625,8 +625,8 @@ Fixpoint list_nth_mut_shared_loop_pair_loop_back
then Return (ListCons ret tl0)
else (
i0 <- u32_sub i 1%u32;
- l <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
- Return (ListCons x0 l))
+ tl00 <- list_nth_mut_shared_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x0 tl00))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
@@ -690,9 +690,9 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop_back
then Return (ListCons ret tl0)
else (
i0 <- u32_sub i 1%u32;
- l <-
+ tl00 <-
list_nth_mut_shared_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
- Return (ListCons x0 l))
+ Return (ListCons x0 tl00))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
@@ -756,8 +756,8 @@ Fixpoint list_nth_shared_mut_loop_pair_loop_back
then Return (ListCons ret tl1)
else (
i0 <- u32_sub i 1%u32;
- l <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
- Return (ListCons x1 l))
+ tl10 <- list_nth_shared_mut_loop_pair_loop_back T n0 tl0 tl1 i0 ret;
+ Return (ListCons x1 tl10))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
@@ -821,9 +821,9 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop_back
then Return (ListCons ret tl1)
else (
i0 <- u32_sub i 1%u32;
- l <-
+ tl10 <-
list_nth_shared_mut_loop_pair_merge_loop_back T n0 tl0 tl1 i0 ret;
- Return (ListCons x1 l))
+ Return (ListCons x1 tl10))
| ListNil => Fail_ Failure
end
| ListNil => Fail_ Failure
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 2074d02e..7137e92a 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -128,7 +128,7 @@ let rec hash_map_insert_in_list_loop_back
else
begin match hash_map_insert_in_list_loop_back t key value tl with
| Fail e -> Fail e
- | Return l -> Return (ListCons ckey cvalue l)
+ | Return tl0 -> Return (ListCons ckey cvalue tl0)
end
| ListNil -> let l = ListNil in Return (ListCons key value l)
end
@@ -413,7 +413,7 @@ let rec hash_map_get_mut_in_list_loop_back
else
begin match hash_map_get_mut_in_list_loop_back t tl key ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons ckey cvalue l)
+ | Return tl0 -> Return (ListCons ckey cvalue tl0)
end
| ListNil -> Fail Failure
end
@@ -514,7 +514,7 @@ let rec hash_map_remove_from_list_loop_back
else
begin match hash_map_remove_from_list_loop_back t key tl with
| Fail e -> Fail e
- | Return l -> Return (ListCons ckey x l)
+ | Return tl0 -> Return (ListCons ckey x tl0)
end
| ListNil -> Return ListNil
end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index d2b87305..f3b480c3 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -137,7 +137,7 @@ let rec hashmap_hash_map_insert_in_list_loop_back
else
begin match hashmap_hash_map_insert_in_list_loop_back t key value tl with
| Fail e -> Fail e
- | Return l -> Return (HashmapListCons ckey cvalue l)
+ | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
end
| HashmapListNil ->
let l = HashmapListNil in Return (HashmapListCons key value l)
@@ -442,7 +442,7 @@ let rec hashmap_hash_map_get_mut_in_list_loop_back
else
begin match hashmap_hash_map_get_mut_in_list_loop_back t tl key ret with
| Fail e -> Fail e
- | Return l -> Return (HashmapListCons ckey cvalue l)
+ | Return tl0 -> Return (HashmapListCons ckey cvalue tl0)
end
| HashmapListNil -> Fail Failure
end
@@ -553,7 +553,7 @@ let rec hashmap_hash_map_remove_from_list_loop_back
else
begin match hashmap_hash_map_remove_from_list_loop_back t key tl with
| Fail e -> Fail e
- | Return l -> Return (HashmapListCons ckey x l)
+ | Return tl0 -> Return (HashmapListCons ckey x tl0)
end
| HashmapListNil -> Return HashmapListNil
end
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 73539cf6..3e8425dd 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -140,7 +140,7 @@ let rec list_nth_mut_loop_loop_back
| Return i0 ->
begin match list_nth_mut_loop_loop_back t tl i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x l)
+ | Return tl0 -> Return (ListCons x tl0)
end
end
| ListNil -> Fail Failure
@@ -201,7 +201,7 @@ let rec get_elem_mut_loop_back
else
begin match get_elem_mut_loop_back x tl ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons y l)
+ | Return tl0 -> Return (ListCons y tl0)
end
| ListNil -> Fail Failure
end
@@ -290,7 +290,7 @@ let rec list_nth_mut_loop_with_id_loop_back
| Return i0 ->
begin match list_nth_mut_loop_with_id_loop_back t i0 tl ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x l)
+ | Return tl0 -> Return (ListCons x tl0)
end
end
| ListNil -> Fail Failure
@@ -379,7 +379,7 @@ let rec list_nth_mut_loop_pair_loop_back'a
| Return i0 ->
begin match list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x0 l)
+ | Return tl00 -> Return (ListCons x0 tl00)
end
end
| ListNil -> Fail Failure
@@ -412,7 +412,7 @@ let rec list_nth_mut_loop_pair_loop_back'b
| Return i0 ->
begin match list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x1 l)
+ | Return tl10 -> Return (ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
@@ -500,7 +500,7 @@ let rec list_nth_mut_loop_pair_merge_loop_back
begin match list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret
with
| Fail e -> Fail e
- | Return (l, l0) -> Return (ListCons x0 l, ListCons x1 l0)
+ | Return (tl00, tl10) -> Return (ListCons x0 tl00, ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
@@ -588,7 +588,7 @@ let rec list_nth_mut_shared_loop_pair_loop_back
begin match list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret
with
| Fail e -> Fail e
- | Return l -> Return (ListCons x0 l)
+ | Return tl00 -> Return (ListCons x0 tl00)
end
end
| ListNil -> Fail Failure
@@ -650,7 +650,7 @@ let rec list_nth_mut_shared_loop_pair_merge_loop_back
begin match
list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x0 l)
+ | Return tl00 -> Return (ListCons x0 tl00)
end
end
| ListNil -> Fail Failure
@@ -711,7 +711,7 @@ let rec list_nth_shared_mut_loop_pair_loop_back
begin match list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret
with
| Fail e -> Fail e
- | Return l -> Return (ListCons x1 l)
+ | Return tl10 -> Return (ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
@@ -773,7 +773,7 @@ let rec list_nth_shared_mut_loop_pair_merge_loop_back
begin match
list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret with
| Fail e -> Fail e
- | Return l -> Return (ListCons x1 l)
+ | Return tl10 -> Return (ListCons x1 tl10)
end
end
| ListNil -> Fail Failure
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:12:14 +0000