diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractToFStar.ml | 11 | ||||
| -rw-r--r-- | compiler/Pure.ml | 33 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 18 | ||||
| -rw-r--r-- | compiler/Translate.ml | 20 | ||||
| -rw-r--r-- | compiler/fstar/Primitives.fst | 7 |
5 files changed, 43 insertions, 46 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 |