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
|
open AST
open ASTUtils
open Error
let value_as_int pos = function
| L_Int i -> (
try Z.to_int i
with Z.Overflow ->
failwith "Cannot slice with an integer more than machine size.")
| v ->
fatal_from pos (Error.MismatchType (PP.literal_to_string v, [ integer' ]))
let is_positive z = Z.sign z != -1
let is_strict_positive z = Z.sign z = 1
let bv_same_length b1 b2 = Bitvector.(length b1 = length b2)
let exp_real q z =
if Q.sign q = 0 then (
assert (Z.sign z >= 0) (* Case handled earlier *);
if Z.sign z = 0 then Q.one else Q.zero)
else
let q, z = if is_positive z then (q, z) else (Q.inv q, Z.neg z) in
let num = Q.num q and den = Q.den q in
let i = Z.to_int z in
let res_num = Z.pow num i and res_den = Z.pow den i in
Q.(res_num /// res_den)
let binop_values pos t op v1 v2 =
match (op, v1, v2) with
(* int -> int -> int *)
| PLUS, L_Int v1, L_Int v2 -> L_Int (Z.add v1 v2)
| MUL, L_Int v1, L_Int v2 -> L_Int (Z.mul v1 v2)
| MINUS, L_Int v1, L_Int v2 -> L_Int (Z.sub v1 v2)
| DIV, L_Int v1, L_Int v2 when is_strict_positive v2 && Z.divisible v1 v2 ->
L_Int (Z.divexact v1 v2)
| DIVRM, L_Int v1, L_Int v2 when is_strict_positive v2 ->
L_Int (Z.fdiv v1 v2) (* Division rounded towards minus infinity. *)
| MOD, L_Int v1, L_Int v2 when is_strict_positive v2 ->
L_Int Z.(sub v1 (mul v2 (fdiv v1 v2)))
(* We cannot use any rem function in Z as we need the rounded towards minus infinity reminder. *)
| POW, L_Int v1, L_Int v2 when is_positive v2 -> L_Int Z.(pow v1 (to_int v2))
| SHL, L_Int v1, L_Int v2 when is_positive v2 ->
L_Int Z.(shift_left v1 (to_int v2))
| SHR, L_Int v1, L_Int v2 when is_positive v2 ->
L_Int Z.(shift_right v1 (to_int v2))
(* int -> int -> bool*)
| EQ_OP, L_Int v1, L_Int v2 -> L_Bool (Z.equal v1 v2)
| NEQ, L_Int v1, L_Int v2 -> L_Bool (not (Z.equal v1 v2))
| LEQ, L_Int v1, L_Int v2 -> L_Bool (Z.leq v1 v2)
| LT, L_Int v1, L_Int v2 -> L_Bool (Z.lt v1 v2)
| GEQ, L_Int v1, L_Int v2 -> L_Bool (Z.geq v1 v2)
| GT, L_Int v1, L_Int v2 -> L_Bool (Z.gt v1 v2)
(* bool -> bool -> bool *)
| BAND, L_Bool b1, L_Bool b2 -> L_Bool (b1 && b2)
| BOR, L_Bool b1, L_Bool b2 -> L_Bool (b1 || b2)
| BEQ, L_Bool b1, L_Bool b2 -> L_Bool (b1 == b2)
| IMPL, L_Bool b1, L_Bool b2 -> L_Bool ((not b1) || b2)
| EQ_OP, L_Bool b1, L_Bool b2 -> L_Bool (b1 == b2)
| NEQ, L_Bool b1, L_Bool b2 -> L_Bool (b1 <> b2)
(* real -> real -> real *)
| PLUS, L_Real v1, L_Real v2 -> L_Real (Q.add v1 v2)
| MUL, L_Real v1, L_Real v2 -> L_Real (Q.mul v1 v2)
| MINUS, L_Real v1, L_Real v2 -> L_Real (Q.sub v1 v2)
| RDIV, L_Real v1, L_Real v2 -> L_Real (Q.div v1 v2)
| POW, L_Real q1, L_Int z2 when not (Q.sign q1 = 0 && Z.sign z2 < 0) ->
(* 0.0 ^ z is not defined for z < 0 *)
L_Real (exp_real q1 z2)
(* real -> real -> bool *)
| EQ_OP, L_Real v1, L_Real v2 -> L_Bool (Q.equal v1 v2)
| NEQ, L_Real v1, L_Real v2 -> L_Bool (not (Q.equal v1 v2))
| LEQ, L_Real v1, L_Real v2 -> L_Bool (Q.leq v1 v2)
| LT, L_Real v1, L_Real v2 -> L_Bool (Q.lt v1 v2)
| GEQ, L_Real v1, L_Real v2 -> L_Bool (Q.geq v1 v2)
| GT, L_Real v1, L_Real v2 -> L_Bool (Q.gt v1 v2)
(* bits -> bits -> bool *)
| EQ_OP, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_Bool (Bitvector.equal b1 b2)
| NEQ, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_Bool (not @@ Bitvector.equal b1 b2)
(* bits -> bits -> bits *)
| OR, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_BitVector (Bitvector.logor b1 b2)
| AND, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_BitVector (Bitvector.logand b1 b2)
| EOR, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_BitVector (Bitvector.logxor b1 b2)
| PLUS, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_BitVector
Bitvector.(
of_z (length b1) (Z.add (to_z_unsigned b1) (to_z_unsigned b2)))
| MINUS, L_BitVector b1, L_BitVector b2 when bv_same_length b1 b2 ->
L_BitVector
Bitvector.(
of_z (length b1) (Z.sub (to_z_unsigned b1) (to_z_unsigned b2)))
| BV_CONCAT, L_BitVector b1, L_BitVector b2 ->
L_BitVector (Bitvector.concat [ b1; b2 ])
(* bits -> integer -> bits *)
| PLUS, L_BitVector b1, L_Int z2 ->
L_BitVector Bitvector.(of_z (length b1) (Z.add (to_z_unsigned b1) z2))
| MINUS, L_BitVector b1, L_Int z2 ->
L_BitVector Bitvector.(of_z (length b1) (Z.sub (to_z_unsigned b1) z2))
(* string -> string -> bool *)
| EQ_OP, L_String s1, L_String s2 -> L_Bool (String.equal s1 s2)
| NEQ, L_String s1, L_String s2 -> L_Bool (not (String.equal s1 s2))
(* enum -> enum -> bool *)
| EQ_OP, L_Label s1, L_Label s2 -> L_Bool (String.equal s1 s2)
| NEQ, L_Label s1, L_Label s2 -> L_Bool (not (String.equal s1 s2))
(* Failure *)
| _ -> fatal_from pos (Error.UnsupportedBinop (t, op, v1, v2))
let unop_values pos t op v =
match (op, v) with
| NEG, L_Int i -> L_Int (Z.neg i)
| NEG, L_Real r -> L_Real (Q.neg r)
| BNOT, L_Bool b -> L_Bool (not b)
| NOT, L_BitVector bv -> L_BitVector (Bitvector.lognot bv)
| _ -> fatal_from pos (Error.UnsupportedUnop (t, op, v))
|
