summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/ExtractToFStar.ml11
-rw-r--r--compiler/Pure.ml33
-rw-r--r--compiler/SymbolicToPure.ml18
-rw-r--r--compiler/Translate.ml20
-rw-r--r--compiler/fstar/Primitives.fst7
-rw-r--r--tests/betree/Primitives.fst7
-rw-r--r--tests/betree_back_stateful/Primitives.fst7
-rw-r--r--tests/hashmap/Primitives.fst7
-rw-r--r--tests/hashmap_on_disk/Primitives.fst7
-rw-r--r--tests/misc/Primitives.fst7
10 files changed, 63 insertions, 61 deletions
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index a995d4a6..fc04ce90 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -1456,16 +1456,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
*)
let inputs_lvs =
let all_inputs = (Option.get def.body).inputs_lvs in
- (* We have to count:
- * - the forward inputs
- * - the state (if there is one)
- *)
- let num_fwd_inputs = def.signature.info.num_fwd_inputs in
- let num_fwd_inputs =
- if def.signature.info.effect_info.stateful_group then
- 1 + num_fwd_inputs
- else num_fwd_inputs
- in
+ let num_fwd_inputs = def.signature.info.num_fwd_inputs_with_state in
Collections.List.prefix num_fwd_inputs all_inputs
in
let _ =
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index cc29469a..fc18dbd3 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -511,11 +511,16 @@ type fun_effect_info = {
(** Meta information about a function signature *)
type fun_sig_info = {
- num_fwd_inputs : int;
- (** The number of input types for forward computation, ignoring the state *)
- num_back_inputs : int option;
+ num_fwd_inputs_no_state : int;
+ (** The number of input types for forward computation, ignoring the state (if there is one) *)
+ num_fwd_inputs_with_state : int;
+ (** The number of input types for forward computation, with the state (if there is one) *)
+ num_back_inputs_no_state : int option;
(** The number of additional inputs for the backward computation (if pertinent),
- ignoring the state *)
+ ignoring the state (if there is one) *)
+ num_back_inputs_with_state : int option;
+ (** The number of additional inputs for the backward computation (if pertinent),
+ with the state (if there is one) *)
effect_info : fun_effect_info;
}
@@ -524,14 +529,14 @@ type fun_sig_info = {
We have the following cases:
- forward function:
[in_ty0 -> ... -> in_tyn -> out_ty] (* pure function *)
- `in_ty0 -> ... -> in_tyn -> result out_ty` (* error-monad *)
- `in_ty0 -> ... -> in_tyn -> state -> result (state & out_ty)` (* state-error *)
+ [in_ty0 -> ... -> in_tyn -> result out_ty] (* error-monad *)
+ [in_ty0 -> ... -> in_tyn -> state -> result (state & out_ty)] (* state-error *)
- backward function:
- `in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm -> (back_out0 & ... & back_outp)` (* pure function *)
- `in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm ->
- result (back_out0 & ... & back_outp)` (* error-monad *)
- `in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
- result (state & (back_out0 & ... & back_outp))` (* state-error *)
+ [in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm -> (back_out0 & ... & back_outp)] (* pure function *)
+ [in_ty0 -> ... -> in_tyn -> back_in0 -> ... back_inm ->
+ result (back_out0 & ... & back_outp)] (* error-monad *)
+ [in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
+ result (state & (back_out0 & ... & back_outp))] (* state-error *)
Note that a stateful backward function takes two states as inputs: the
state received by the associated forward function, and the state at which
@@ -543,7 +548,7 @@ type fun_sig_info = {
(st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
]}
- The function's type should be given by `mk_arrows sig.inputs sig.output`.
+ The function's type should be given by [mk_arrows sig.inputs sig.output].
We provide additional meta-information:
- we divide between forward inputs and backward inputs (i.e., inputs specific
to the forward functions, and additional inputs necessary if the signature is
@@ -571,8 +576,8 @@ type fun_sig = {
fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
]}
Decomposed outputs:
- - forward function: [T]
- - backward function: [T; T] (for "x" and "y")
+ - forward function: [[T]]
+ - backward function: [[T; T]] (for "x" and "y")
*)
info : fun_sig_info; (** Additional information *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 74bc20ae..6b44a69c 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -644,11 +644,23 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
(* Type parameters *)
let type_params = sg.type_params in
(* Return *)
+ let num_fwd_inputs_no_state = List.length fwd_inputs in
+ let num_back_inputs_no_state =
+ if bid = None then None else Some (List.length back_inputs)
+ in
let info =
{
- num_fwd_inputs = List.length fwd_inputs;
- num_back_inputs =
- (if bid = None then None else Some (List.length back_inputs));
+ num_fwd_inputs_no_state;
+ num_fwd_inputs_with_state =
+ (* We use the fact that [fwd_state_ty] has length 1 if there is a state,
+ and 0 otherwise *)
+ num_fwd_inputs_no_state + List.length fwd_state_ty;
+ num_back_inputs_no_state;
+ num_back_inputs_with_state =
+ (* Length of [back_state_ty]: similar trick as for [fwd_state_ty] *)
+ Option.map
+ (fun n -> n + List.length back_state_ty)
+ num_back_inputs_no_state;
effect_info;
}
in
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 453e02db..e943c78a 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -134,7 +134,6 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
in
(* We need to initialize the input/output variables *)
- let num_forward_inputs = List.length fdef.signature.inputs in
let add_forward_inputs input_svs ctx =
match fdef.body with
| None -> ctx
@@ -189,23 +188,12 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
in
(* We need to ignore the forward inputs, and the state input (if there is) *)
- let fun_info =
- SymbolicToPure.get_fun_effect_info fun_context.fun_infos
- (A.Regular def_id) (Some back_id)
- in
let backward_inputs =
+ let sg = backward_sg.sg in
(* We need to ignore the forward state and the backward state *)
- (* TODO: this is ad-hoc and error-prone. We should group all this
- * information in the signature information. *)
- let fwd_state_n = if fun_info.stateful_group then 1 else 0 in
- let num_forward_inputs = num_forward_inputs + fwd_state_n in
- let back_state_n = if fun_info.stateful then 1 else 0 in
- let num_back_inputs =
- List.length backward_sg.sg.inputs
- - num_forward_inputs - back_state_n
- in
- Collections.List.subslice backward_sg.sg.inputs num_forward_inputs
- num_back_inputs
+ let num_forward_inputs = sg.info.num_fwd_inputs_with_state in
+ let num_back_inputs = Option.get sg.info.num_back_inputs_no_state in
+ Collections.List.subslice sg.inputs num_forward_inputs num_back_inputs
in
(* As we forbid nested borrows, the additional inputs for the backward
* functions come from the borrows in the return value of the rust function:
diff --git a/compiler/fstar/Primitives.fst b/compiler/fstar/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/compiler/fstar/Primitives.fst
+++ b/compiler/fstar/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
diff --git a/tests/betree_back_stateful/Primitives.fst b/tests/betree_back_stateful/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/betree_back_stateful/Primitives.fst
+++ b/tests/betree_back_stateful/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index b44fe9d1..96138e46 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -47,8 +47,8 @@ let mem_replace_back (a : Type0) (x : a) (y : a) : a = y
(*** Scalars *)
/// Rk.: most of the following code was at least partially generated
-let isize_min : int = -9223372036854775808
-let isize_max : int = 9223372036854775807
+let isize_min : int = -9223372036854775808 // TODO: should be opaque
+let isize_max : int = 9223372036854775807 // TODO: should be opaque
let i8_min : int = -128
let i8_max : int = 127
let i16_min : int = -32768
@@ -60,7 +60,7 @@ let i64_max : int = 9223372036854775807
let i128_min : int = -170141183460469231731687303715884105728
let i128_max : int = 170141183460469231731687303715884105727
let usize_min : int = 0
-let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max]
+let usize_max : int = 4294967295 // TODO: should be opaque
let u8_min : int = 0
let u8_max : int = 255
let u16_min : int = 0
@@ -149,6 +149,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
+// TODO: check the semantics of casts in Rust
let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 00:13:12 +0000