diff --git a/engine/lib/phases/phase_cf_into_monads.ml b/engine/lib/phases/phase_cf_into_monads.ml index feaf4428c..373c31f50 100644 --- a/engine/lib/phases/phase_cf_into_monads.ml +++ b/engine/lib/phases/phase_cf_into_monads.ml @@ -217,7 +217,8 @@ struct | Return { e; _ } -> let open KnownMonads in let e = dexpr e in - UB.call Core__ops__control_flow__ControlFlow__Break [ e ] span + UB.call_Constructor Core__ops__control_flow__ControlFlow__Break false + [ e ] span (to_typ @@ { monad = Some (MException e.typ); typ }) | [%inline_arms "dexpr'.*" - Let - Match - If - Continue - Break - QuestionMark diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 13bb37366..26e9f2570 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1195,9 +1195,22 @@ impl<'tcx, S: ExprState<'tcx>> SInto for rustc_middle::thir::Expr<'tcx> let hir_id = hir_id.map(|hir_id| hir_id.index()); let unrolled = self.unroll_scope(s); let rustc_middle::thir::Expr { span, kind, ty, .. } = unrolled; + let tcx = s.base().tcx; let contents = match macro_invocation_of_span(span, s).map(ExprKind::MacroInvokation) { Some(contents) => contents, None => match kind { + // Special treatment for `AnonConst`s, particularly for enum discriminants + rustc_middle::thir::ExprKind::NamedConst { def_id, substs, .. } + if substs.is_empty() + && tcx.def_kind(def_id) == rustc_hir::def::DefKind::AnonConst => + { + match tcx.const_eval_poly(def_id) { + Ok(value) if let Decorated {contents: box e @ ExprKind::Literal {..}, ..} = const_value_to_constant_expr(s, ty, value, span).into() => { + e + }, + _ => kind.sinto(s), + } + } rustc_middle::thir::ExprKind::NonHirLiteral { lit, .. } => { let cexpr: ConstantExpr = (ConstantExprKind::Literal(scalar_int_to_constant_literal(s, lit, ty))) diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap new file mode 100644 index 000000000..db03840f6 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap @@ -0,0 +1,53 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: coq + info: + name: enum-repr + manifest: enum-repr/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 +stderr = ''' +Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) + Finished dev [unoptimized + debuginfo] target(s) in XXs''' + +[stdout] +diagnostics = [] + +[stdout.files] +"Enum_repr.v" = ''' +(* File automatically generated by Hacspec *) +From Hacspec Require Import Hacspec_Lib MachineIntegers. +From Coq Require Import ZArith. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. + +Inductive t_Foo : Type := +| Foo_A : t_Foo +| Foo_B : t_Foo +| Foo_C : t_Foo. + +(*Not implemented yet? todo(item)*) + +Definition f (_ : unit) : int16 := + let _x := cast ((@repr WORDSIZE16 5).+(@repr WORDSIZE16 0)) : int16 in + cast ((@repr WORDSIZE16 9).+(@repr WORDSIZE16 0)). + +Definition ff__CONST : int16 := + cast ((@repr WORDSIZE16 1).+(@repr WORDSIZE16 0)). +''' diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap new file mode 100644 index 000000000..85b44ce93 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap @@ -0,0 +1,48 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: fstar + info: + name: enum-repr + manifest: enum-repr/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 +stderr = ''' +Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) + Finished dev [unoptimized + debuginfo] target(s) in XXs''' + +[stdout] +diagnostics = [] + +[stdout.files] +"Enum_repr.fst" = ''' +module Enum_repr +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_Foo = + | Foo_A : t_Foo + | Foo_B : t_Foo + | Foo_C : t_Foo + +let f (_: Prims.unit) : u16 = + let v__x:u16 = cast (5us +! 0us <: u16) <: u16 in + cast (9us +! 0us <: u16) <: u16 + +let ff__CONST: u16 = cast (1us +! 0us <: u16) <: u16 +''' diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap new file mode 100644 index 000000000..e97cb4ac8 --- /dev/null +++ b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap @@ -0,0 +1,89 @@ +--- +source: test-harness/src/harness.rs +expression: snapshot +info: + kind: + Translate: + backend: ssprove + info: + name: enum-repr + manifest: enum-repr/Cargo.toml + description: ~ + spec: + optional: false + broken: false + issue_id: ~ + positive: true + snapshot: + stderr: true + stdout: true + include_flag: ~ + backend_options: ~ +--- +exit = 0 +stderr = ''' +Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) + Finished dev [unoptimized + debuginfo] target(s) in XXs''' + +[stdout] +diagnostics = [] + +[stdout.files] +"Enum_repr.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. + +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +Definition t_Foo : choice_type := + ('unit ∐ 'unit ∐ 'unit). +Notation "'Foo_A_case'" := (inl (inl tt)) (at level 100). +Equations Foo_A {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_A := + solve_lift (ret_both (inl (inl (tt : 'unit)) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. +Notation "'Foo_B_case'" := (inl (inr tt)) (at level 100). +Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_B := + solve_lift (ret_both (inl (inr (tt : 'unit)) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. +Notation "'Foo_C_case'" := (inr tt) (at level 100). +Equations Foo_C {L : {fset Location}} {I : Interface} : both L I t_Foo := + Foo_C := + solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo. +Fail Next Obligation. + +(*Not implemented yet? todo(item)*) + +Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int16 := + f _ := + letb v__x := cast_int (WS2 := _) ((ret_both (5 : int16)) .+ (ret_both (0 : int16))) in + solve_lift (cast_int (WS2 := _) ((ret_both (9 : int16)) .+ (ret_both (0 : int16)))) : both L1 I1 int16. +Fail Next Obligation. + +Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 := + ff__CONST := + solve_lift (cast_int (WS2 := _) ((ret_both (1 : int16)) .+ (ret_both (0 : int16)))) : both L I int16. +Fail Next Obligation. +''' diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index 3c3bef810..b63251903 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -55,7 +55,11 @@ let early_returns (x: u32) : u32 = Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit = if x >. 3ul then - let! hoist2:Rust_primitives.Hax.t_Never = Core.Ops.Control_flow.ControlFlow.v_Break 0ul in + let! hoist2:Rust_primitives.Hax.t_Never = + Core.Ops.Control_flow.ControlFlow_Break 0ul + <: + Core.Ops.Control_flow.t_ControlFlow u32 Rust_primitives.Hax.t_Never + in Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist2) <: Core.Ops.Control_flow.t_ControlFlow u32 Prims.unit @@ -70,7 +74,9 @@ let early_returns (x: u32) : u32 = match true with | true -> let! hoist4:Rust_primitives.Hax.t_Never = - Core.Ops.Control_flow.ControlFlow.v_Break 34ul + Core.Ops.Control_flow.ControlFlow_Break 34ul + <: + Core.Ops.Control_flow.t_ControlFlow u32 Rust_primitives.Hax.t_Never in Core.Ops.Control_flow.ControlFlow_Continue (x, Rust_primitives.Hax.never_to_any hoist4 <: (u32 & u32)) @@ -88,14 +94,10 @@ let early_returns (x: u32) : u32 = Core.Ops.Control_flow.t_ControlFlow u32 (u32 & u32) in let! hoist8:Rust_primitives.Hax.t_Never = - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add - 123ul - hoist5 - <: - u32) - x - <: - u32) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist5 <: u32) x) + <: + Core.Ops.Control_flow.t_ControlFlow u32 Rust_primitives.Hax.t_Never in Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist8) <: @@ -157,9 +159,11 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8) | Core.Option.Option_None -> - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None - <: - Core.Option.t_Option u8) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) + (Core.Option.t_Option u8) else match x with | Core.Option.Option_Some hoist24 -> @@ -173,13 +177,17 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8) | Core.Option.Option_None -> - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None - <: - Core.Option.t_Option u8)) - | Core.Option.Option_None -> - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None + Core.Ops.Control_flow.ControlFlow_Break + (Core.Option.Option_None <: Core.Option.t_Option u8) <: - Core.Option.t_Option u8) + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) + (Core.Option.t_Option u8)) + | Core.Option.Option_None -> + Core.Ops.Control_flow.ControlFlow_Break + (Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) + (Core.Option.t_Option u8) in (match hoist26 with | Core.Option.Option_Some hoist27 -> @@ -192,9 +200,10 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. <: Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8 | Core.Option.Option_None -> - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None - <: - Core.Option.t_Option u8)) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8) | 4uy -> (match z with | Core.Option.Option_Some hoist16 -> @@ -203,9 +212,10 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. <: Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8 | Core.Option.Option_None -> - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Option.Option_None - <: - Core.Option.t_Option u8)) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Option.Option_None <: Core.Option.t_Option u8) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) u8) | _ -> Core.Ops.Control_flow.ControlFlow_Continue 12uy <: @@ -255,10 +265,10 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 = Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) u32 | Core.Result.Result_Err err -> let! _:Prims.unit = - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Result.Result_Err - (Core.Convert.f_from err <: u8 -> u32) - <: - Core.Result.t_Result u32 u32) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result u32 u32) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) Prims.unit in Core.Ops.Control_flow.ControlFlow_Continue x <: @@ -295,9 +305,11 @@ let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B = match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with | Core.Result.Result_Ok hoist33 -> let! hoist35:Rust_primitives.Hax.t_Never = - Core.Ops.Control_flow.ControlFlow.v_Break (Core.Result.Result_Ok hoist33 - <: - Core.Result.t_Result t_A t_B) + Core.Ops.Control_flow.ControlFlow_Break + (Core.Result.Result_Ok hoist33 <: Core.Result.t_Result t_A t_B) + <: + Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result t_A t_B) + Rust_primitives.Hax.t_Never in Core.Ops.Control_flow.ControlFlow_Continue (Rust_primitives.Hax.never_to_any hoist35) <: diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap index 01ca06526..d0056c9f5 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -18,6 +18,7 @@ info: stderr: true stdout: true include_flag: ~ + backend_options: ~ --- exit = 0 stderr = ''' @@ -77,14 +78,14 @@ Fail Next Obligation. Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := early_returns x := solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32)) - then letm[choice_typeMonad.result_bind_code int32] hoist2 := v_Break (ret_both (0 : int32)) in + then letm[choice_typeMonad.result_bind_code int32] hoist2 := ControlFlow_Break (ret_both (0 : int32)) in ControlFlow_Continue (never_to_any hoist2) else () in letb hoist3 := x >.? (ret_both (30 : int32)) in letm[choice_typeMonad.result_bind_code int32] hoist5 := ifb hoist3 then matchb ret_both (true : 'bool) with | true => - letm[choice_typeMonad.result_bind_code int32] hoist4 := v_Break (ret_both (34 : int32)) in + letm[choice_typeMonad.result_bind_code int32] hoist4 := ControlFlow_Break (ret_both (34 : int32)) in ControlFlow_Continue (solve_lift (never_to_any hoist4)) | _ => ControlFlow_Continue (solve_lift (ret_both (3 : int32))) @@ -93,7 +94,7 @@ Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 x .+ (ret_both (1 : int32))) in letb hoist6 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist5 in letb hoist7 := impl__u32__wrapping_add hoist6 x in - letm[choice_typeMonad.result_bind_code int32] hoist8 := v_Break hoist7 in + letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break hoist7 in ControlFlow_Continue (never_to_any hoist8))) : both L1 I1 int32. Fail Next Obligation. @@ -223,7 +224,7 @@ Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 solve_lift (run (ifb x >.? (ret_both (123 : int8)) then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist33 := ControlFlow_Continue (impl__map_err (Result_Err B) f_from) in letb hoist34 := Result_Ok hoist33 in - letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := v_Break hoist34 in + letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := ControlFlow_Break hoist34 in ControlFlow_Continue (never_to_any hoist35) else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). Fail Next Obligation. diff --git a/tests/enum-repr/Cargo.toml b/tests/enum-repr/Cargo.toml index cfc6cefdf..a67634836 100644 --- a/tests/enum-repr/Cargo.toml +++ b/tests/enum-repr/Cargo.toml @@ -6,4 +6,4 @@ edition = "2021" [dependencies] [package.metadata.hax-tests] -into."fstar+coq+ssprove" = { broken = false, snapshot = "none", issue_id = "162" } +into."fstar+coq+ssprove" = { broken = false, issue_id = "162" }