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
92
93
94
95
|
import Out.Sail.Sail
import Out.Sail.BitVec
open PreSail
set_option maxHeartbeats 1_000_000_000
set_option maxRecDepth 1_000_000
set_option linter.unusedVariables false
set_option match.ignoreUnusedAlts true
open Sail
abbrev Register := PEmpty
abbrev RegisterType : Register -> Type := PEmpty.elim
abbrev exception := Unit
abbrev SailM := PreSailM RegisterType trivialChoiceSource exception
XXXXXXXXX
import Out.Sail.Sail
import Out.Sail.BitVec
import Out.Sail.IntRange
import Out.Defs
import Out.Specialization
import Out.FakeReal
set_option maxHeartbeats 1_000_000_000
set_option maxRecDepth 1_000_000
set_option linter.unusedVariables false
set_option match.ignoreUnusedAlts true
open Sail
namespace Out.Functions
/-- Type quantifiers: k_ex448# : Bool, k_ex447# : Bool -/
def neq_bool (x : Bool) (y : Bool) : Bool :=
(! (x == y))
/-- Type quantifiers: x : Int -/
def __id (x : Int) : Int :=
x
/-- Type quantifiers: n : Int, m : Int -/
def _shl_int_general (m : Int) (n : Int) : Int :=
bif (n ≥b 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 :=
bif (n ≥b 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 :=
bif ((n <b 0) && (m >b 0))
then ((Int.tdiv (n +i 1) m) -i 1)
else
(bif ((n >b 0) && (m <b 0))
then ((Int.tdiv (n -i 1) m) -i 1)
else (Int.tdiv n m))
/-- Type quantifiers: m : Int, n : Int -/
def fmod_int (n : Int) (m : Int) : Int :=
(n -i (m *i (fdiv_int n m)))
/-- Type quantifiers: k_n : Int -/
def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
(HAppend.hAppend str (BitVec.toFormatted x))
/-- Type quantifiers: x : Int -/
def concat_str_dec (str : String) (x : Int) : String :=
(HAppend.hAppend str (Int.repr x))
def multi_line (_ : Unit) : Unit :=
let _ : Unit := (print_endline "Hello, World!")
(print_endline "Hello, World!")
def test (_ : Unit) : Unit :=
let _ : Unit := (print_endline "'")
let _ : Unit := (print_endline "\"")
(print_endline "'")
def initialize_registers (_ : Unit) : Unit :=
()
def sail_model_init (x_0 : Unit) : Unit :=
(initialize_registers ())
end Out.Functions
|
