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
|
\begin{figure}
\numberrules
Statements:
\begin{pannel}
\srule G, E |- "skip", M \evalstmt "Out_normal", \E0, M
\end
\label{rule:10}
\\[2mm]
\srule G, E |- "break", M \evalstmt "Out_break", \E0, M
\end
\label{rule:13}
\\[2mm]
\srule G, E |- "continue", M \evalstmt "Out_continue", \E0, M
\end
\label{rule:14}
\irule
G, E |- a, M \evalexpr v, \tr, M'
--------------------------------------------------
G, E |- a , M \evalstmt \out, \tr, M'
\end \label{rule:11}
\irule
G, E |- \unannot{a_1}{\tau}, M \evallvalue \loc, \tr_1, M_1 &
G, E |- \unannot{a_2}{\tau'}, M_1 \evalexpr v, \tr_2, M_2 \\
"storeval"(\tau,M_2,\loc,v) = \some{M_3}
--------------------------------------------------
G, E |- {(\unannot{a_1}{\tau} \hbox{" = "} \unannot{a_2}{\tau'})}^{\tau}, M \evalexpr v, \cat {\tr_1} \tr_2, M_3
\end \label{rule:12}
\\
\irule
G, E |- s_1, M \evalstmt "Out_normal", \tr_1, M_1 &
G, E |- s_2, M_1 \evalstmt \out, \tr_2, M_2
--------------------------------------------------
G, E |- (s_1 ; s_2), M \evalstmt \out, \cat {\tr_1} \tr_2, M_2
\end \label{rule:15}
\irule
G, E |- s_1, M \evalstmt out, \tr, M' &
out \not= "Out_normal"
--------------------------------------------------
G, E |- (s_1; s_2), M \evalstmt \out, \tr, M'
\end \label{rule:16}
\\
\irule
G, E |- a, M \evalexpr v, \tr, M' & "is_false"(v)
--------------------------------------------------
G, E |- ("while" (a) ~ s), M \evalstmt "Out_normal", \tr, M'
\end \label{rule:17}
\irule
G, E |- a, M \evalexpr v, \tr_1, M_1 & "is_true" (v) \\
G, E |- s, M_1 \evalstmt \out, \tr_2, M_2 \\
\out \in \{"Out_break", "Out_return", "Out_return" (v)\}
--------------------------------------------------
G, E |- ("while" (a)~s), M \evalstmt "Out_normal", \cat {\tr_1} \tr_2, M_2
\end \label{rule:18}
\irule
G, E |- a, M \evalexpr v_a, \tr_1, M_1 & "is_true" (v_a) \\
G, E |- s, M_1 \evalstmt ("Out_normal" \mid "Out_continue"), \tr_2, M_2 \\
G, E |- ("while" (a)~s), M_2 \evalstmt \out', \tr_3, M_3
--------------------------------------------------
G, E |- ("while" (a)~s), M \evalstmt \out', \cat {\cat {\tr_1} \tr_2} \tr_3, M_3
\end \label{rule:19}
\\
\srule
G, E |- ("return" \, \None), M \evalstmt "Out_return" , \tr, M
\end \label{rule:20}
\\
\irule
G, E |- a, M \evalexpr v, \tr, M'
--------------------------------------------------
G, E |- ("return" \some a), M \evalstmt "Out_return" (v), \tr, M'
\end \label{rule:21}
\end{pannel}
\caption{Selected rules of the dynamic semantics of Clight (statements execution)}
\label{fig:dynsem2}
\end{figure}
|
