1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
import Out.Sail.Sail
import Out.Sail.BitVec
open Sail
abbrev bits k_n := (BitVec k_n)
/-- Type quantifiers: k_a : Type -/
inductive option (k_a : Type) where
| Some (_ : k_a)
| None (_ : Unit)
open option
abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
/-- Type quantifiers: x : Int -/
def __id (x : Int) : Int :=
x
/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
if (LE.le len (Sail.BitVec.length v))
then (Sail.BitVec.truncate v len)
else (Sail.BitVec.zeroExtend v len)
/-- Type quantifiers: n : Nat, n ≥ 0 -/
def sail_ones (n : Nat) : (BitVec n) :=
(Complement.complement (BitVec.zero n))
/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
if (GE.ge l n)
then (HShiftLeft.hShiftLeft (sail_ones n) i)
else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
(HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
/-- Type quantifiers: n : Int, m : Int -/
def _shl_int_general (m : Int) (n : Int) : Int :=
if (GE.ge n 0)
then (Int.shiftl m n)
else (Int.shiftr m (Neg.neg n))
/-- Type quantifiers: n : Int, m : Int -/
def _shr_int_general (m : Int) (n : Int) : Int :=
if (GE.ge n 0)
then (Int.shiftr m n)
else (Int.shiftl m (Neg.neg n))
/-- Type quantifiers: m : Int, n : Int -/
def fdiv_int (n : Int) (m : Int) : Int :=
if (Bool.and (LT.lt n 0) (GT.gt m 0))
then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
else if (Bool.and (GT.gt n 0) (LT.lt m 0))
then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
else (Int.tdiv n m)
/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(HSub.hSub n (HMul.hMul m (fdiv_int n m)))
/-- Type quantifiers: k_a : Type -/
def is_none (opt : (Option k_a)) : Bool :=
match opt with
| some _ => false
| none => true
/-- Type quantifiers: k_a : Type -/
def is_some (opt : (Option k_a)) : Bool :=
match opt with
| some _ => true
| none => false
/-- Type quantifiers: k_n : Int -/
def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
(HAppend.hAppend str (BitVec.toHex x))
/-- Type quantifiers: x : Int -/
def concat_str_dec (str : String) (x : Int) : String :=
(HAppend.hAppend str (Int.repr x))
def sail_main (_ : Unit) : SailM Unit := do
(print_endline_effect "Hello, World!")
def initialize_registers (_ : Unit) : Unit :=
()
def main (_ : List String) : IO UInt32 := do
main_of_sail_main ⟨default, (), default, default, default⟩ sail_main
return 0
|
