1%if false  
2  Copyright (c) 2009, ETH Zurich.
3  All rights reserved.
4  
5  This file is distributed under the terms in the attached LICENSE file.
6  If you do not find this file, copies can be found by writing to:
7  ETH Zurich D-INFK, Haldeneggsteig 4, CH-8092 Zurich. Attn: Systems Group.
8%endif
9
10%include polycode.fmt
11
12%if false
13
14> module Eval where
15
16> import Data.Bits as B
17
18> import PureExpressions
19
20%endif
21
22\section{Functional core interpreter}
23\label{sec:semantics_core}
24
25
26In this Section, we implement an expression evaluator. Given
27any (correct) expression, it will compute the corresponding value. The
28implementation is decomposed in several steps. In Section
29\ref{sec:sub:eval_top}, we evaluate top-level expressions. Doing so,
30we rely on case-specific evaluators. This includes unary operators
31(Section \ref{sec:sub:eval_unary}), binary operators (Section
32\ref{sec:sub:eval_binary}), the sizeof operation (Section
33\ref{sec:sub:eval_sizeof}), the conditional operation (Section
34\ref{sec:sub:eval_test}), and the cast operation (Section
35\ref{sec:sub:eval_cast}).
36
37Note that the following functions are \emph{partial}: not all
38expressions can be successfully evaluated. Indeed, some operations are
39simply meaningless. For example, computing the sum of a structure and
40a float is illegal. Currently, we are simply ignore these errors and this might
41result in run-time errors of the DSL compiler. Satisfactory solutions of
42this problem exist, though. For example, we could implement a
43type-checker that would ensure the absence of run-time errors. Another
44approach would be improve our error handling code.
45
46
47\subsubsection{Top-level Evaluation}
48\label{sec:sub:eval_top}
49
50The purpose of this section is implement the following function:
51
52> symbEval :: PureExpr -> PureExpr
53
54That reduces a given expression to a value. Hence, for values, this is
55trivial:
56
57> symbEval Void = Void
58> symbEval x@(CLInteger _ _ _) = x
59> symbEval x@(CLFloat _) = x
60> symbEval x@(CLRef _ _ _) = x
61
62Then, for inductive constructions, we rely on the specific functions
63implemented in the following sections.
64
65> symbEval (Unary op x) = 
66>     symbEvalUnary op x'
67>         where x' = symbEval x
68>
69> symbEval (Binary op x y) = 
70>     symbEvalBinary op x' y'
71>         where x' = symbEval x
72>               y' = symbEval y
73>
74> symbEval (Sizeof typ) = symbEvalSizeof typ
75>
76> symbEval (Test x y z) = 
77>     symbEvalTest x' y z
78>         where x' = symbEval x
79>
80> symbEval (Cast t x) = 
81>     symbEvalCast t x'
82>         where x' = symbEval x
83
84
85\subsubsection{Unary Operator Evaluation}
86\label{sec:sub:eval_unary}
87
88For unary operators, we need to implement the following function:
89
90> symbEvalUnary :: UnaryOp -> PureExpr -> PureExpr
91
92Hence the following code:
93
94> symbEvalUnary Minus x =
95>     case x of 
96>       CLInteger Signed size x -> CLInteger Signed size (-x)
97>       CLFloat x -> CLFloat (-x)
98>       _ -> error "symbEvalUnary: minus on wrong type"
99>
100> symbEvalUnary Complement x = 
101>     case x of
102>       CLInteger sg sz x -> CLInteger sg sz (complement x)
103>       _ -> error "symbEvalUnary: complement on wrong type"
104>
105> symbEvalUnary Negation x =
106>     case x of 
107>       CLInteger sg sz 0 -> CLInteger sg sz 1
108>       CLInteger sg sz _ -> CLInteger sg sz 0
109>       _ -> error "symbEvalUnary: negation on wrong type"
110
111
112\subsubsection{Binary Operator Evaluation}
113\label{sec:sub:eval_binary}
114
115For binary operators, here is our goal:
116
117> symbEvalBinary :: BinaryOp -> PureExpr -> PureExpr -> PureExpr
118
119Achieved by the following, messy codes.
120
121\paragraph{Arithmetic Operations\\}
122
123> symbEvalBinary Plus (CLInteger sg si x) (CLInteger sg' si' y)
124>     | sg == sg' && si == si' = CLInteger sg si (x + y)
125>     | otherwise = error "symbEvalBinary: Plus undefined"
126> symbEvalBinary Plus (CLInteger _ _ x) (CLFloat y) =
127>     CLFloat ( (fromRational $ toRational x) + y )
128> symbEvalBinary Plus (CLFloat x) (CLInteger _ _ y) = 
129>     CLFloat ( x + (fromRational $ toRational y) )
130> symbEvalBinary Plus (CLFloat x) (CLFloat y) = CLFloat ( x + y)
131> symbEvalBinary Plus _ _ = error "symbEvalBinary: Plus undefined"
132
133More checks should be added here. For examples, we should ensure that
134the result of the subtraction of two unsigned numbers is still
135positive, or make it wrap.
136
137> symbEvalBinary Sub (CLInteger sg si x) (CLInteger sg' si' y)
138>     | sg == sg' && si == si' = CLInteger sg si (x - y)
139>     | otherwise = error "symbEvalBinary: Sub undefined"
140> symbEvalBinary Sub (CLInteger _ _ x) (CLFloat y) = 
141>     CLFloat ( (fromRational $ toRational x) - y )
142> symbEvalBinary Sub (CLFloat x) (CLInteger _ _ y) = 
143>     CLFloat ( x - (fromRational $ toRational y) )
144> symbEvalBinary Sub (CLFloat x) (CLFloat y) = CLFloat ( x - y)
145> symbEvalBinary Sub _ _ = error "symbEvalBinary: Sub undefined"
146>
147> symbEvalBinary Mul (CLInteger sg si x) (CLInteger sg' si' y) 
148>     | sg == sg' && si == si' = CLInteger sg si (x * y)
149>     | otherwise = error "symbEvalBinary: Mul undefined"
150> symbEvalBinary Mul (CLInteger _ _ x) (CLFloat y) = 
151>     CLFloat ( (fromRational $ toRational x) * y )
152> symbEvalBinary Mul (CLFloat x) (CLInteger _ _ y) = 
153>     CLFloat ( x * (fromRational $ toRational y) )
154> symbEvalBinary Mul (CLFloat x) (CLFloat y) = CLFloat ( x * y )
155> symbEvalBinary Mul _ _ = error "symbEvalBinary: Mul undefined"
156>
157> symbEvalBinary Div (CLInteger sg si x) (CLInteger sg' si' y)
158>     | sg == sg' && si == si' = CLInteger sg si (x `div` y)
159>     | otherwise = error "symbEvalBinary: Div undefined"
160> symbEvalBinary Div (CLInteger _ _ x) (CLFloat y) = 
161>     CLFloat ( (fromRational $ toRational x) / y )
162> symbEvalBinary Div (CLFloat x) (CLInteger _ _ y) = 
163>     CLFloat ( x / (fromRational $ toRational y) )
164> symbEvalBinary Div (CLFloat x) (CLFloat y) = CLFloat (x / y)
165> symbEvalBinary Div _ _ = error "symbEvalBinary: Div undefined"
166>
167> symbEvalBinary Mod (CLInteger sg si x) (CLInteger sg' si' y) 
168>     | sg == sg' && si == si' = CLInteger sg si (x `mod` y)
169>     | otherwise = error "symbEvalBinary: Mod undefined"
170> symbEvalBinary Mod _ _ = error "symbEvalBinary: Mod undefined"
171
172
173\paragraph{Boolean Operations\\}
174
175
176> symbEvalBinary Shl (CLInteger sg si x) (CLInteger sg' si' y) 
177>     | sg == sg' && si == si' = CLInteger sg si (shiftL x (fromInteger y))
178>     | otherwise = error "symbEvalBinary: Shl undefined"
179> symbEvalBinary Shl _ _ = error "symbEvalBinary: Shl undefined"
180>
181> symbEvalBinary Shr (CLInteger sg si x) (CLInteger sg' si' y) 
182>     | sg == sg' && si == si' = CLInteger sg si (shiftR x (fromInteger y))
183>     | otherwise = error "symbEvalBinary: Shr undefined"
184> symbEvalBinary Shr _ _ = error "symbEvalBinary: Shr undefined"
185>
186> symbEvalBinary AndBit (CLInteger sg si x) (CLInteger sg' si' y) 
187>     | sg == sg' && si == si' = CLInteger sg si (x B..|. y)
188>     | otherwise = error "symbEvalBinary: And undefined"
189> symbEvalBinary AndBit _ _ = error "symbEvalBinary: And undefined"
190>
191> symbEvalBinary OrBit (CLInteger sg si x) (CLInteger sg' si' y) 
192>     | sg == sg' && si == si' = CLInteger sg si (x B..&. y)
193>     | otherwise = error "symbEvalBinary: Or undefined"
194> symbEvalBinary OrBit _ _  = error "symbEvalBinary: Or undefined"
195>
196> symbEvalBinary XorBit (CLInteger sg si x) (CLInteger sg' si' y) 
197>     | sg == sg' && si == si' = CLInteger sg si (x `xor` y)
198>     | otherwise = error "symbEvalBinary: Xor undefined"
199> symbEvalBinary XorBit _ _ = error "symbEvalBinary: Xor undefined"
200
201
202\paragraph{Comparison Operations\\}
203
204
205> symbEvalBinary op (CLInteger sg si x) (CLInteger sg' si' y) 
206>     | sg == sg' && si == si' = symbEvalComp op x y
207>     | otherwise = error ("symbEvalBinary: " ++ show op ++ " undefined")
208> symbEvalBinary op (CLInteger _ _ x) (CLFloat y) = 
209>     symbEvalComp op (fromRational $ toRational x) y
210> symbEvalBinary op (CLFloat x) (CLInteger _ _ y) = 
211>     symbEvalComp op x (fromRational $ toRational y)
212> symbEvalBinary op (CLFloat x) (CLFloat y) = symbEvalComp op x y
213
214> symbEvalBinary Le _ _ = error "symbEvalBinary: Le undefined"
215> symbEvalBinary Leq _ _ = error "symbEvalBinary: Leq undefined"
216> symbEvalBinary Ge _ _ = error "symbEvalBinary: Leq undefined"
217> symbEvalBinary Geq _ _ = error "symbEvalBinary: Leq undefined"
218> symbEvalBinary Eq _ _ = error "symbEvalBinary: Leq undefined"
219> symbEvalBinary Neq _ _ = error "symbEvalBinary: Leq undefined"
220
221> symbEvalComp :: (Ord a, Num a) => BinaryOp -> a -> a -> PureExpr
222> symbEvalComp op x y =
223>     let cmp = case op of
224>                 Le -> (<)
225>                 Leq -> (<=)
226>                 Ge -> (>)
227>                 Geq -> (>=)
228>                 Eq -> (==)
229>                 Neq -> (/=) in
230>         if cmp x y then 
231>             CLInteger Unsigned TInt64 1 
232>         else CLInteger Unsigned TInt64 0
233
234\subsubsection{Sizeof Evaluation}
235\label{sec:sub:eval_sizeof}
236
237Our |sizeof| operator follows the corresponding C operation:
238
239> symbEvalSizeof :: TypeExpr -> PureExpr
240> symbEvalSizeof TVoid = CLInteger Unsigned TInt64 1
241> symbEvalSizeof (TInt _ TInt8) = CLInteger Unsigned TInt64 1
242> symbEvalSizeof (TInt _ TInt16) = CLInteger Unsigned TInt64 2
243> symbEvalSizeof (TInt _ TInt32) = CLInteger Unsigned TInt64 4
244> symbEvalSizeof (TInt _ TInt64) = CLInteger Unsigned TInt64 8
245> symbEvalSizeof TFloat = CLInteger Unsigned TInt64 4
246> symbEvalSizeof (TPointer _ _) = CLInteger Unsigned TInt64 8
247> symbEvalSizeof (TCompPointer _) = CLInteger Unsigned TInt64 8
248> symbEvalSizeof (TArray _ typ) = CLInteger Unsigned TInt64 8
249> symbEvalSizeof (TStruct _ _ fields) = CLInteger Unsigned TInt64 8
250> symbEvalSizeof (TUnion _ _ fields) = CLInteger Unsigned TInt64 8
251
252%if false 
253
254 symbEvalSizeof (TFunction _ _ _) = CLInteger Unsigned TInt64 1
255
256%endif
257
258
259\subsubsection{Conditionals Evaluation}
260\label{sec:sub:eval_test}
261
262The semantics of the conditional mimics a restricted version of the C
263standard: True corresponds to everything which is not a float or
264integer equal to zero. Hence, we evaluate the corresponding branch
265accordingly.
266
267> symbEvalTest :: PureExpr -> PureExpr -> PureExpr -> PureExpr
268> symbEvalTest (CLInteger _ _ 0) _ y = symbEval y
269> symbEvalTest (CLFloat 0) _ y = symbEval y
270> symbEvalTest _ x _ = symbEval x
271
272
273\subsubsection{Cast Evaluation}
274\label{sec:sub:eval_cast}
275
276Here is our stripped-down version of |cast|. It will probably deserve
277some work in the future, as it is quite restrictive. Also, it should
278ensure that the type modification are reflected on the data:
279converting a signed, negative number to an unsigned form changes the
280value of this number. This is currently unsupported.
281
282> symbEvalCast :: TypeExpr -> PureExpr -> PureExpr
283> symbEvalCast (TInt sg sz) (CLInteger sg' sz' x) 
284>     | sg' < sg && sz' < sz = CLInteger sg sz x
285>     | otherwise = error "symbEvalCast: illegal integer cast"
286> symbEvalCast TFloat (CLInteger _ _ x) = 
287>     CLFloat (fromRational $ toRational x)
288> symbEvalCast TFloat vx@(CLFloat x) = vx
289> symbEvalCast _ _ = 
290>     error "symbEvalCast: Not yet implemented/undefined cast"
291