diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/Pure.ml | 1 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 70 | ||||
-rw-r--r-- | compiler/SynthesizeSymbolic.ml | 2 | ||||
-rw-r--r-- | tests/coq/hashmap/Hashmap_Funs.v | 12 | ||||
-rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Funs.v | 12 | ||||
-rw-r--r-- | tests/coq/misc/Loops.v | 38 | ||||
-rw-r--r-- | tests/fstar/hashmap/Hashmap.Funs.fst | 6 | ||||
-rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst | 6 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 20 |
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 |