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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
/// The following code generates the limits for the scalar types
fn test_modulo(x: i32, y: i32) {
println!("{} % {} = {}", x, y, x % y);
}
fn main() {
let ints_lower = [
"isize", "i8", "i16", "i32", "i64", "i128", "usize", "u8", "u16", "u32", "u64", "u128",
];
let ints_upper = [
"Isize", "I8", "I16", "I32", "I64", "I128", "Usize", "U8", "U16", "U32", "U64", "U128",
];
let can_fail_binops_lower = ["div", "rem", "add", "sub", "mul"];
let mut ints_pairs = vec![];
for i in 0..ints_lower.len() {
ints_pairs.push((&ints_lower[i], &ints_upper[i]));
}
// Generate the code to print the scalar ranges
for s in &ints_lower {
println!(
"println!(\"let {}_min = Z.of_string \\\"{{}}\\\"\", {}::MIN);",
s, s
);
println!(
"println!(\"let {}_max = Z.of_string \\\"{{}}\\\"\", {}::MAX);",
s, s
);
}
println!("\n");
// Generate the OCaml definitions for the ranges - this code is
// generated (comes from the above)
println!("let isize_min = Z.of_string \"{}\"", isize::MIN);
println!("let isize_max = Z.of_string \"{}\"", isize::MAX);
println!("let i8_min = Z.of_string \"{}\"", i8::MIN);
println!("let i8_max = Z.of_string \"{}\"", i8::MAX);
println!("let i16_min = Z.of_string \"{}\"", i16::MIN);
println!("let i16_max = Z.of_string \"{}\"", i16::MAX);
println!("let i32_min = Z.of_string \"{}\"", i32::MIN);
println!("let i32_max = Z.of_string \"{}\"", i32::MAX);
println!("let i64_min = Z.of_string \"{}\"", i64::MIN);
println!("let i64_max = Z.of_string \"{}\"", i64::MAX);
println!("let i128_min = Z.of_string \"{}\"", i128::MIN);
println!("let i128_max = Z.of_string \"{}\"", i128::MAX);
println!("let usize_min = Z.of_string \"{}\"", usize::MIN);
println!("let usize_max = Z.of_string \"{}\"", usize::MAX);
println!("let u8_min = Z.of_string \"{}\"", u8::MIN);
println!("let u8_max = Z.of_string \"{}\"", u8::MAX);
println!("let u16_min = Z.of_string \"{}\"", u16::MIN);
println!("let u16_max = Z.of_string \"{}\"", u16::MAX);
println!("let u32_min = Z.of_string \"{}\"", u32::MIN);
println!("let u32_max = Z.of_string \"{}\"", u32::MAX);
println!("let u64_min = Z.of_string \"{}\"", u64::MIN);
println!("let u64_max = Z.of_string \"{}\"", u64::MAX);
println!("let u128_min = Z.of_string \"{}\"", u128::MIN);
println!("let u128_max = Z.of_string \"{}\"", u128::MAX);
println!("\n");
// Generate the check_int_in_range body
for (lo, up) in &ints_pairs {
println!("| {} -> Z.leq {}_min i && Z.leq i {}_max", up, lo, lo);
}
println!("\n");
// Generate the scalar_value_get_value_range body
for s in &ints_upper {
println!("| {} i -> i", s);
}
println!("\n");
// Generate the mk_scalar body
for s in &ints_upper {
println!("| Types.{} -> Ok ({} i)", s, s);
}
println!("\n");
// Generate the code to print the scalar ranges in F*
for s in &ints_lower {
println!("println!(\"let {}_min : int = {{}}\", {}::MIN);", s, s);
println!("println!(\"let {}_max : int = {{}}\", {}::MAX);", s, s);
}
println!("\n");
// Generate the F* definitions for the ranges - this code is
// generated (comes from the above)
println!("let isize_min : int = {}", isize::MIN);
println!("let isize_max : int = {}", isize::MAX);
println!("let i8_min : int = {}", i8::MIN);
println!("let i8_max : int = {}", i8::MAX);
println!("let i16_min : int = {}", i16::MIN);
println!("let i16_max : int = {}", i16::MAX);
println!("let i32_min : int = {}", i32::MIN);
println!("let i32_max : int = {}", i32::MAX);
println!("let i64_min : int = {}", i64::MIN);
println!("let i64_max : int = {}", i64::MAX);
println!("let i128_min : int = {}", i128::MIN);
println!("let i128_max : int = {}", i128::MAX);
println!("let usize_min : int = {}", usize::MIN);
println!("let usize_max : int = {}", usize::MAX);
println!("let u8_min : int = {}", u8::MIN);
println!("let u8_max : int = {}", u8::MAX);
println!("let u16_min : int = {}", u16::MIN);
println!("let u16_max : int = {}", u16::MAX);
println!("let u32_min : int = {}", u32::MIN);
println!("let u32_max : int = {}", u32::MAX);
println!("let u64_min : int = {}", u64::MIN);
println!("let u64_max : int = {}", u64::MAX);
println!("let u128_min : int = {}", u128::MIN);
println!("let u128_max : int = {}", u128::MAX);
println!("\n");
// Generate the body for the ScalarTy definition
for (_lo, up) in &ints_pairs {
println!("| {}", up);
}
println!("\n");
// Generate the body for the max/min F* functions
for (lo, up) in &ints_pairs {
println!("| {} -> {}_min", up, lo);
}
println!("\n");
// Generate the scalar types for F*
for (lo, up) in &ints_pairs {
println!("type {} = scalar {}", lo, up);
}
println!("\n");
// Generate the unops (rk.: we need to manually filter `-` applied on
// unisgned numbers)
for binop in &can_fail_binops_lower {
for (lo, up) in &ints_pairs {
println!("let {}_{} = scalar_{} #{}", lo, binop, binop, up);
}
println!("");
}
println!("\n");
// Modulo tests
test_modulo(1, 2);
test_modulo(-1, 2);
test_modulo(1, -2);
test_modulo(-1, -2);
}
|
