summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/ExtractToFStar.ml2
-rw-r--r--src/InterpreterBorrows.ml2
-rw-r--r--src/InterpreterStatements.ml17
-rw-r--r--src/InterpreterUtils.ml4
-rw-r--r--src/SymbolicAst.ml2
-rw-r--r--src/SymbolicToPure.ml21
-rw-r--r--src/SynthesizeSymbolic.ml6
-rw-r--r--src/Values.ml1
-rw-r--r--tests/hashmap/Hashmap.Clauses.Template.fst4
-rw-r--r--tests/hashmap/Hashmap.Funs.fst19
-rw-r--r--tests/hashmap/Hashmap.Types.fst4
-rw-r--r--tests/misc/Constants.fst123
12 files changed, 170 insertions, 35 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index c915aede..f2c481c0 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1363,7 +1363,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(qualif : fun_decl_qualif) (has_decreases_clause : bool) (def : fun_decl) :
unit =
- assert (def.is_global_body);
+ assert (not def.is_global_body);
(* Retrieve the function name *)
let def_name = ctx_get_local_function def.def_id def.back_id ctx in
(* (* Add the type parameters - note that we need those bindings only for the
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index a13ac786..6b920a51 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -436,7 +436,7 @@ let give_back_symbolic_value (_config : C.config)
assert (sv.sv_id <> nsv.sv_id);
(match nsv.sv_kind with
| V.SynthInputGivenBack | V.SynthRetGivenBack | V.FunCallGivenBack -> ()
- | V.FunCallRet | V.SynthInput -> failwith "Unrechable");
+ | V.FunCallRet | V.SynthInput | V.Global -> failwith "Unrechable");
(* Store the given-back value as a meta-value for synthesis purposes *)
let mv = nsv in
(* Substitution function, to replace the borrow projectors over symbolic values *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 31c3aabb..48620439 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -920,19 +920,10 @@ and eval_global (config : C.config) (dest : V.VarId.id) (gid : LA.GlobalDeclId.i
(eval_local_function_call_concrete config global.body_id [] [] [] place) cf ctx
| SymbolicMode ->
(* Treat the global as a fresh symbolic value *)
-
- (*
- let g = A.GlobalDeclId.Map.find gid ctx.global_context.global_decls in
- (eval_local_function_call_symbolic config g.body_id [] [] [] place) cf ctx
-
- failwith "TODO Got error later in translate_fun_decl>meta>expansion ~> lookup_var_for_symbolic_value";
- *)
-
- let rty = ety_no_regions_to_rty global.ty in
- let sval = mk_fresh_symbolic_value V.FunCallRet rty in
- let sval = mk_typed_value_from_symbolic_value sval in
- (assign_to_place config sval place) (cf Unit) ctx
-
+ let sval = mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty) in
+ let cc = assign_to_place config (mk_typed_value_from_symbolic_value sval) place in
+ let e = cc (cf Unit) ctx in
+ S.synthesize_global_eval gid sval e
(** Evaluate a switch *)
and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 47323cc2..6ef66f1d 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -238,8 +238,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
raise Found
else ()
| V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
- | V.SynthRetGivenBack ->
- ()
+ | V.SynthRetGivenBack -> ()
+ | V.Global -> ()
end
in
(* We use exceptions *)
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 9cab092d..fd490e43 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -65,6 +65,8 @@ type expression =
| Panic
| FunCall of call * expression
| EndAbstraction of V.abs * expression
+ | EvalGlobal of A.GlobalDeclId.id * V.symbolic_value * expression
+ (** A fresh symbolic value for the global *)
| Expansion of mplace option * V.symbolic_value * expansion
(** Expansion of a symbolic value.
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 16e48aef..81af6a8b 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -687,13 +687,7 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) :
List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars
let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
- try (V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var) with
- Not_found ->
- print_endline ("Missing " ^ Print.V.show_symbolic_value sv);
- V.SymbolicValueId.Map.iter (fun id (v : var) ->
- print_endline (" -- " ^ (Option.value v.basename ~default:""))
- ) ctx.sv_to_var;
- raise Not_found
+ V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var
(** Peel boxes as long as the value is of the form `Box<T>` *)
let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
@@ -1080,6 +1074,7 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
| Panic -> translate_panic ctx
| FunCall (call, e) -> translate_function_call config call e ctx
| EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx
+ | EvalGlobal (gid, sv, e) -> translate_global_eval config gid sv e ctx
| Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx
| Meta (meta, e) -> translate_meta config meta e ctx
@@ -1466,6 +1461,18 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
mk_let monadic given_back (mk_texpression_from_var input_var) e)
given_back_inputs next_e
+and translate_global_eval (config : config) (gid : A.GlobalDeclId.id)
+ (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx)
+ : texpression =
+ let (ctx, var) = fresh_var_for_symbolic_value sval ctx in
+ let decl = A.GlobalDeclId.Map.find gid ctx.global_context.llbc_global_decls in
+ let global_expr = { id = Global gid; type_args = [] } in
+ (* We use translate_fwd_ty to translate the global type *)
+ let ty = ctx_translate_fwd_ty ctx decl.ty in
+ let gval = { e = Qualif global_expr; ty } in
+ let e = translate_expression config e ctx in
+ mk_let false (mk_typed_pattern_from_var var None) gval e
+
and translate_expansion (config : config) (p : S.mplace option)
(sv : V.symbolic_value) (exp : S.expansion) (ctx : bs_ctx) : texpression =
(* Translate the scrutinee *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 95da38e6..fa244649 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -114,6 +114,12 @@ let synthesize_function_call (call_id : call_id)
in
Some (FunCall (call, expr))
+let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value) (expr : expression option)
+ : expression option =
+ match expr with
+ | None -> None
+ | Some e -> Some (EvalGlobal (gid, dest, e))
+
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)
diff --git a/src/Values.ml b/src/Values.ml
index 4585b443..13cd2580 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -65,6 +65,7 @@ type sv_kind =
*)
| SynthInputGivenBack
(** The value was given back upon ending one of the input abstractions *)
+ | Global (** The value is a global *)
[@@deriving show]
type symbolic_value = {
diff --git a/tests/hashmap/Hashmap.Clauses.Template.fst b/tests/hashmap/Hashmap.Clauses.Template.fst
index c1549e6b..2a3d9cb9 100644
--- a/tests/hashmap/Hashmap.Clauses.Template.fst
+++ b/tests/hashmap/Hashmap.Clauses.Template.fst
@@ -24,6 +24,10 @@ let hash_map_insert_in_list_decreases (t : Type0) (key : usize) (value : t)
(ls : list_t t) : nat =
admit ()
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
(** [hashmap::HashMap::{0}::move_elements_from_list]: decreases clause *)
unfold
let hash_map_move_elements_from_list_decreases (t : Type0)
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index 921ed142..397ee720 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -248,24 +248,23 @@ let rec hash_map_move_elements_fwd_back
(** [hashmap::HashMap::{0}::try_resize] *)
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
- let i = core_num_u32_max_c in
- begin match scalar_cast U32 Usize i with
+ begin match scalar_cast U32 Usize core_num_u32_max_c with
| Fail -> Fail
| Return max_usize ->
let capacity = vec_len (list_t t) self.hash_map_slots in
begin match usize_div max_usize 2 with
| Fail -> Fail
| Return n1 ->
- let (i0, i1) = self.hash_map_max_load_factor in
- begin match usize_div n1 i0 with
+ let (i, i0) = self.hash_map_max_load_factor in
+ begin match usize_div n1 i with
| Fail -> Fail
- | Return i2 ->
- if capacity <= i2
+ | Return i1 ->
+ if capacity <= i1
then
begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return i3 ->
- begin match hash_map_new_with_capacity_fwd t i3 i0 i1 with
+ | Return i2 ->
+ begin match hash_map_new_with_capacity_fwd t i2 i i0 with
| Fail -> Fail
| Return ntable ->
begin match
@@ -273,13 +272,13 @@ let hash_map_try_resize_fwd_back
with
| Fail -> Fail
| Return (ntable0, _) ->
- Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
+ Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
ntable0.hash_map_max_load ntable0.hash_map_slots)
end
end
end
else
- Return (Mkhash_map_t self.hash_map_num_entries (i0, i1)
+ Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
self.hash_map_max_load self.hash_map_slots)
end
end
diff --git a/tests/hashmap/Hashmap.Types.fst b/tests/hashmap/Hashmap.Types.fst
index 91ee26c6..f81f4185 100644
--- a/tests/hashmap/Hashmap.Types.fst
+++ b/tests/hashmap/Hashmap.Types.fst
@@ -19,3 +19,7 @@ type hash_map_t (t : Type0) =
hash_map_slots : vec (list_t t);
}
+(** [core::num::u32::{8}::MAX] *)
+let core_num_u32_max_body : result u32 = Return 4294967295
+let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
+
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index f5bd41cb..5cfb82d6 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -13,4 +13,125 @@ let x0_c : u32 = eval_global x0_body
let core_num_u32_max_body : result u32 = Return 4294967295
let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body
-(** [constants::X1] *) \ No newline at end of file
+(** [constants::X1] *)
+let x1_body : result u32 = Return core_num_u32_max_c
+let x1_c : u32 = eval_global x1_body
+
+(** [constants::X2] *)
+let x2_body : result u32 = Return 3
+let x2_c : u32 = eval_global x2_body
+
+(** [constants::incr] *)
+let incr_fwd (n : u32) : result u32 =
+ begin match u32_add n 1 with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::X3] *)
+let x3_body : result u32 =
+ begin match incr_fwd 32 with | Fail -> Fail | Return i -> Return i end
+let x3_c : u32 = eval_global x3_body
+
+(** [constants::mk_pair0] *)
+let mk_pair0_fwd (x : u32) (y0 : u32) : result (u32 & u32) = Return (x, y0)
+
+(** [constants::Pair] *)
+type pair_t (t1 t2 : Type0) = { pair_x : t1; pair_y : t2; }
+
+(** [constants::mk_pair1] *)
+let mk_pair1_fwd (x : u32) (y0 : u32) : result (pair_t u32 u32) =
+ Return (Mkpair_t x y0)
+
+(** [constants::P0] *)
+let p0_body : result (u32 & u32) =
+ begin match mk_pair0_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+let p0_c : (u32 & u32) = eval_global p0_body
+
+(** [constants::P1] *)
+let p1_body : result (pair_t u32 u32) =
+ begin match mk_pair1_fwd 0 1 with | Fail -> Fail | Return p -> Return p end
+let p1_c : pair_t u32 u32 = eval_global p1_body
+
+(** [constants::P2] *)
+let p2_body : result (u32 & u32) = Return (0, 1)
+let p2_c : (u32 & u32) = eval_global p2_body
+
+(** [constants::P3] *)
+let p3_body : result (pair_t u32 u32) = Return (Mkpair_t 0 1)
+let p3_c : pair_t u32 u32 = eval_global p3_body
+
+(** [constants::Wrap] *)
+type wrap_t (t : Type0) = { wrap_val : t; }
+
+(** [constants::Wrap::{0}::new] *)
+let wrap_new_fwd (t : Type0) (val0 : t) : result (wrap_t t) =
+ Return (Mkwrap_t val0)
+
+(** [constants::Y] *)
+let y_body : result (wrap_t i32) =
+ begin match wrap_new_fwd i32 2 with | Fail -> Fail | Return w -> Return w end
+let y_c : wrap_t i32 = eval_global y_body
+
+(** [constants::unwrap_y] *)
+let unwrap_y_fwd : result i32 = Return y_c.wrap_val
+
+(** [constants::YVAL] *)
+let yval_body : result i32 =
+ begin match unwrap_y_fwd with | Fail -> Fail | Return i -> Return i end
+let yval_c : i32 = eval_global yval_body
+
+(** [constants::get_z1::Z1] *)
+let get_z1_z1_body : result i32 = Return 3
+let get_z1_z1_c : i32 = eval_global get_z1_z1_body
+
+(** [constants::get_z1] *)
+let get_z1_fwd : result i32 = Return get_z1_z1_c
+
+(** [constants::add] *)
+let add_fwd (a : i32) (b : i32) : result i32 =
+ begin match i32_add a b with | Fail -> Fail | Return i -> Return i end
+
+(** [constants::Q1] *)
+let q1_body : result i32 = Return 5
+let q1_c : i32 = eval_global q1_body
+
+(** [constants::Q2] *)
+let q2_body : result i32 = Return q1_c
+let q2_c : i32 = eval_global q2_body
+
+(** [constants::Q3] *)
+let q3_body : result i32 =
+ begin match add_fwd q2_c 3 with | Fail -> Fail | Return i -> Return i end
+let q3_c : i32 = eval_global q3_body
+
+(** [constants::get_z2] *)
+let get_z2_fwd : result i32 =
+ begin match get_z1_fwd with
+ | Fail -> Fail
+ | Return i ->
+ begin match add_fwd i q3_c with
+ | Fail -> Fail
+ | Return i0 ->
+ begin match add_fwd q1_c i0 with
+ | Fail -> Fail
+ | Return i1 -> Return i1
+ end
+ end
+ end
+
+(** [constants::S1] *)
+let s1_body : result u32 = Return 6
+let s1_c : u32 = eval_global s1_body
+
+(** [constants::S2] *)
+let s2_body : result u32 =
+ begin match incr_fwd s1_c with | Fail -> Fail | Return i -> Return i end
+let s2_c : u32 = eval_global s2_body
+
+(** [constants::S3] *)
+let s3_body : result (pair_t u32 u32) = Return p3_c
+let s3_c : pair_t u32 u32 = eval_global s3_body
+
+(** [constants::S4] *)
+let s4_body : result (pair_t u32 u32) =
+ begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+let s4_c : pair_t u32 u32 = eval_global s4_body
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 07:13:16 +0000