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
|
\begin{figure}
\numberrules
Expressions in l-value position:
\begin{pannel}
\irule
E(\id) = b
--------------------------------------------------
G, E |- \id^\tau, M \evallvalue (b, 0), \E0, M
\end \label{rule:1}
\irule
% G, E |- a, M \evalexpr {\tt Vptr}(\loc), \tr, M'
G, E |- a, M \evalexpr \loc, \tr, M'
--------------------------------------------------
G, E |- (\hbox{"*"}a)^\tau, M \evallvalue \loc, \tr, M'
\end \label{rule:2}
\irule
G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 \\
G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\
"add" (v_1, \tau_1, v_2, \tau_2) = \some{\loc}
--------------------------------------------------
G, E |- (\unannot{a_1}{\tau_1} [\unannot{a_2}{\tau_2}])^\tau, M \evallvalue \loc, \cat {\tr_1} \tr_2, M_2
\end \label{rule:3}
\irule
G, E |- \unannot{a}{\tau}, M \evallvalue (b,\ofs), \tr, M' \\
\tau = "Tstruct" (\id, \fl) &
% "type_of" (a) = "Tstruct" (\id, \fl) &
"field_offset" (f, \fl) = \some{\delta}
--------------------------------------------------
G, E |- (\unannot{a}{\tau} \dot f)^{\tau_s}, M \evallvalue (b,\ofs + "repr" (\delta)), \tr, M'
\end \label{rule:4}
\irule
G, E |- \unannot{a}{\tau}, M \evallvalue \loc, \tr, M' &
\tau = "Tunion" (\id, \fl)
--------------------------------------------------
G, E |- (\unannot{a}{\tau} \dot f)^{\tau_u}, M \evallvalue \loc, \tr, M'
\end \label{rule:5}
\end{pannel}
Expressions in r-value position:
\begin{pannel}
\irule
G, E |- \unannot{a}\tau, M \evallvalue \loc, \tr, M' &
"loadval" (\tau, M', \loc) = \some{v}
--------------------------------------------------
G, E |- \unannot{a}\tau, M \evalexpr v, \tr, M'
\end \label{rule:6}
\irule
G, E |- a, M \evallvalue \loc, \tr, M'
--------------------------------------------------
G, E |- (\hbox{"&"}a)^\tau, M \evalexpr \loc, \tr, M'
\end \label{rule:7}
\irule
G, E |- \unannot{a_1}{\tau_1}, M \evalexpr v_1, \tr_1, M_1 &
G, E |- \unannot{a_2}{\tau_2}, M_1 \evalexpr v_2, \tr_2, M_2 \\
"eval_binary_operation" (\op, v_1,\tau_1, v_2,\tau_2) = \some{v}
--------------------------------------------------
G, E |- (\unannot{a_1}{\tau_1} \op \, \unannot{a_2}{\tau_2})^\tau, M \evalexpr v, \cat \tr_1 \tr_2, M_2
\end \label{rule:8}
\irule
G, E |- \unannot{a}{\tau_a}, M \evalexpr v', \tr, M' &
"cast" (v',\tau_a,\tau) = \some{v}
--------------------------------------------------
G, E |- ((\tau)\unannot{a}{\tau_a}))^\tau, M \evalexpr v, \tr, M'
\end \label{rule:9}
\end{pannel}
\caption{Selected rules of the dynamic semantics of Clight (expression evaluation)}
\label{fig:dynsem1}
\end{figure}
|
