## SectionD.13Exercise Sheet 13

#### Type Check

##### 1.Type Checking 1.
1. Take a look at the following C0p program and state the type environment $$\Gamma'$$ after execution of the Block rule, starting with the environment $$\Gamma = \{\}\text{.}$$

{
char c;
char *pc;
char **ppc;
int i;
int *pi;
i = 42;
...
}


2. Derive the type of the following expressions with respect to the type environment $$\Gamma'\text{.}$$

1. i - 42

2. *pc + i - 1337

3. **ppc - **&pc != 7198

3. Revisit the expression from Item D.13.1.b.i. Which type must i have so that you cannot apply any derivation rules to the expression?

202207281550

202207081400
Solution.
1. $$\displaystyle \{ \texttt{c} \mapsto \texttt{char}, \texttt{pc} \mapsto \texttt{char*}, \texttt{ppc} \mapsto \texttt{char**}, \texttt{i} \mapsto \texttt{int}, \texttt{pi} \mapsto \texttt{int*} \}$$

1. $$\mbox{}$$
2. $$\mbox{}$$
3. $$\mbox{}$$

Help:

$$\mbox{}$$

2. An arbitrary pointer type suffices, since BinArith is only applicable to integral types. If we for example chose the type of i as int*, we could try to apply the rules like this:

There is however no rule which can cast i to an int or a char.

##### 2.Type Checking 2.

Check whether the following program snippets contain type errors using the C0t type semantics. All snippets are inserted into the following context:

{
int a;
char c;
void* v;
char* cp;
int** i;

...
}


1. $$\mbox{}$$
{
cp = v;
while (cp)
a = v;
}

2. $$\mbox{}$$
{
i = &cp;
**i = c + a;
v = &i;
}

3. $$\mbox{}$$
{
cp = &c;
while (cp)
{
int* a;
a = c;
}
}

4. $$\mbox{}$$
{
if (a)
*cp = a;
else
*cp = &a;
}

5. $$\mbox{}$$
{
c = a;
if (c)
abort();
else
*i = &cp;
}

202207281550

202207081400
Solution.

Type environment: $$\Gamma = \{ \texttt{a} \mapsto \textbf{int}, \texttt{c} \mapsto \textbf{char}, \texttt{v} \mapsto \textbf{void*}, \texttt{cp} \mapsto \textbf{char*}, \texttt{i} \mapsto \textbf{int**} \}$$

1. The statement is not well-typed.

1. $$\mbox{}$$

2. $$\mbox{}$$

2. The statement is not well-typed.

1. $$\mbox{}$$

2. $$\mbox{}$$

3. $$\mbox{}$$

3. The statement is not well-typed.

1. $$\mbox{}$$

2. $$\mbox{}$$

3. $$\mbox{}$$

4. $$\mbox{}$$

4. The statement is not well-typed.

1. $$\mbox{}$$
2. $$\mbox{}$$

5. The statement is not well-typed.

1. $$\mbox{}$$

2. $$\mbox{}$$

##### 3.Type Checking 3.

Using the static semantics of C0t, check whether the given program contains type errors under the following type environment: $$\Gamma := \{ \CVar x \mapsto \CChar, \CVar y \mapsto \CPtr\CChar, \CVar z \mapsto \CInt, \CVar p \mapsto \CInt\CPtr\CPtr \}$$

{
x = *y + z;
*p = &z;
x = **p;
}


202207281550

202207081400
Solution.

The program is well-typed under the given type environment.

1. $$\mbox{}$$

2. $$\mbox{}$$

3. $$\mbox{}$$

#### CodeGen

##### 4.Code Generation: The Beginning.

Generate MIPS code for the following C0 programs. To this end, build the inference tree using the rules for code generation and write down the code sequence afterwards. Assume the environment $$\Gamma = \{ x \mapsto 0 \}\text{.}$$

1. (x - 2) + 3

2. if (x) x = 2; else x = 3;

3. while (1) x = x + 1;

202207281550

202207081400
Solution.
1. The following listings contain the code used in the derivation trees.

Subtree (1):
Complete derivation tree:

2. The following listings contain the code used in the derivation trees.

Subtree (A):
Subtree (B):
SubTree (C):
Complete derivation tree:

3. Using the rule for while-loops, we can generate the code for the loop. The final code is:

  b T0

L:
addiu $v0$sp 0

addiu $v1$sp 0
lw $v1 ($v1)
li $v2 1 addiu$v1 $v1$v2

sw $v1 ($v0)

T0:
li $v0 1 bnez$v0 L0


##### 5.Code Generation: Functions.

Compile the following function into MIPS code. To this end, use the code generation rules from the script.

int fac(int n) {
int res;
res = 1;
while (n > 1) {
res = res * n;
n = n - 1;
}
return res;
}


202207281550

202207081400
Solution.

    .global fac
#function prolog
fac:
subiu   $sp$sp 12  # offset = 1x LocalVar +1x Arg + ra =12
sw      $ra 8($sp)   # ra
sw      $a0 0($sp)    # int n
addiu   $t0$sp 4    # L-evaluation res
li      $t1 1 # make 1 sw$t1 ($t0) # store in res b while_end # jump while cond while_body: #res=res*n addiu$t0 $sp 4 # get address res (L-evaluation) addiu$t1 $sp 4 # get address res (R-evaluation) lw$t1 ($t1) # load res addiu$t2 $sp 0 # get address n lw$t2 ($t2) # load n mul$t3 $t1$t2  # mult res * n
sw      $t3 ($t0)    # store in res
#n=n-1
addiu   $t0$sp 0    # get address n (L-evaluation)
addiu   $t1$sp 0    # get address n (R-evaluation)
lw      $t1 ($t1)    # load n
li      $t2 1 # make 1 sub$t3 $t1$t2  # n-1
sw      $t3 ($t0)    # store in n

while_end:
addiu   $t0$sp 0    # get address n
lw      $t0 ($t0)    # load n
li      $t1 1 # make 1 sgt$t0 $t0$t1  # n > 1
bnez    $t0 while_body # if true do body again #end while #return res addiu$t0 $sp 4 # get address res lw$t0 ($t0) # load res move$v0 $t0 # move res to$v0 as return
#end return res

fac_end:
#function epilog
lw      $ra 8($sp)  # reset ra to org. val
addiu   $sp$sp 12  # reset sp offset
jr      $ra # jr  #### Hoare ##### 6.Hoare Logic. Use the rules for Hoare triples to derive a valid precondition $$P\text{.}$$ 1. $$\displaystyle \vdash\hoare{P}{\texttt{a = a + 2;}}{a == 42}$$ 2. $$\displaystyle \vdash\hoare{P}{\texttt{\{ a = b * c; b = c + a; c = c - 17; \}}}{\texttt{a == b} \land \texttt{b == c + 59}}$$ 3. $$\displaystyle \vdash\hoare{P}{\texttt{if (a == 0) abort(); else x = x + 1;}}{x > 0}$$ 4. $$\displaystyle \vdash\hoare{P}{\texttt{if (x < 0) y = -x; else y = x;}}{\texttt{y > 0} \land \texttt{X * X == y * y}}$$ 5. $$\displaystyle \vdash\hoare{P}{\texttt{x = x / z;}}{\texttt{x != 0} \land \texttt{z == 0}}$$ 202207281550 202207081400 Solution. 1. Using [Assign], we can derive: $$P = (a == 42)[a + 2 / a] = (a + 2 == 42) \Leftrightarrow (a == 40)$$ 2. $$\displaystyle P = (b * c == c + b * c \land c + b * c == c - 17 + 59) \Leftrightarrow (c == 0 \land b * c == 42) \Leftrightarrow \mathit{false}$$ 3. $$\displaystyle P = (\texttt{a == 0} \land \mathit{false}) \lor (\texttt{a != 0} \land \texttt{x + 1 > 0}) \Leftrightarrow (\texttt{a != 0} \land \texttt{x > -1})$$ 4. $$\displaystyle P = ((x < 0 \land (-x) > 0 \land X * X == (-x) * (-x)) \lor (\neg (x < 0) \land \texttt{x > 0} \land \texttt{X * X == x * x})) \Leftrightarrow (\texttt{x != 0} \land \texttt{X * X == x * x})$$ 5. $$\displaystyle P = (\texttt{z != 0} \land (\texttt{x / z != 0} \land \texttt{z == 0})) \Leftrightarrow \mathit{false}$$ ##### 7.Hoare Logic: Assignments. Find a valid precondition $$P$$ for the following Hoare triples. 1. $$\displaystyle \vdash\hoare{P}{\texttt{x = x - 1;}}{x == 5}$$ 2. $$\displaystyle \vdash\hoare{P}{\texttt{x = 7;}}{x == 5}$$ 3. $$\displaystyle \vdash\hoare{P}{\texttt{x = 7;}}{x == 7}$$ 4. $$\displaystyle \vdash\hoare{P}{\texttt{a = a - b;}}{a > b}$$ 202207281550 202207081400 Solution. Using the rule Assign, we can derive the following preconditions: 1. $$\displaystyle P = (x == 5)[x - 1 / x] = (x - 1 == 5) \Leftrightarrow (x == 6)$$ 2. $$\displaystyle P = (x == 5)[7 / x] = (7 == 5) \Leftrightarrow \mathit{false}$$ 3. $$\displaystyle P = (x == 7)[7 / x] = (7 == 7) \Leftrightarrow \mathit{true}$$ 4. $$\displaystyle P = (a > b)[a - b / a] = (a - b > b) \Leftrightarrow (a > 2b)$$ ##### 8.Trivial State Sets. Which sets of states are described by the assertions $$\mathit{true}$$ and $$\mathit{false}\text{?}$$ 202207281550 202207081400 Solution. The assertion $$\mathit{true}$$ describes the set of all states, i.e. $$\Sigma\text{.}$$ The assertion $$\mathit{false}$$ describes the empty set $$\emptyset\text{.}$$ ##### 9.Comparison. { q = 0; while (x >= y) { q = q + 1; x = x - y; } r = x; }  C0 program for division. $$r$$ contains the remainder of the division and $$q$$ the quotient. let div x y = if x < y then (1,x) else let (q,r) = div (x-y) y in (q+1,r)  OCaml program for division. \begin{equation*} div(x,y):=\begin{cases} (0,x) & (x \lt y) \\ (q+1,r) & (x \geq y), (q,r) = div(x-y, y) \\ \end{cases} \end{equation*} Recursive function for division. Prove for the OCaml program / the mathematical definition of div the specification $$0\leq x \land y > 0 \to q\cdot y + r = x \land 0\leq r \lt y\text{.}$$ Compare your proof to the correctness proof of the C0 program done using hoare logic. What are the similarities and differences? 202207281550 202207081400 Solution. { // {x = X & 0 <= x [2]} q = 0; // {q*y + x = X [3] & 0 <= x} while (x >= y) { // {q*y + x = X & 0 <= x & x >= y} // {q*y + x + y - y = X [b] & 0 <= x-y [a]} q = q + 1; // {q*y + x - y = X [b] & 0 <= x-y} x = x - y; // {q*y + x = X & 0 <= x} } // {q*y + x = X & 0 <= [2] x < y [1,c]} r = x; // {q*y + r = X & 0 <= r < y} }  The C0 program annotated with its correctness proof as performed using hoare logic. The numbers and letters in brackets show the correspondence to the induction proof. In hoare logic, the case for $$y\lt 0$$ is not considered as the program diverges. Nevertheless, the post-condition is able to prove $$0\lt y\text{.}$$ Proof by complete induction on $$x\text{.}$$ \begin{equation*} \text{IH: }\forall x'\lt x.~x'>0\to \forall m'~r'.~(m',r') = div~x'~y' \to m'y+r'=x' \land 0\leq r'\lt y \end{equation*} Case distinction on $$x\geq y\text{.}$$ Case $$x\lt y\text{.}$$ To show: \begin{equation*} \begin{array}{cl} 0\cdot y + x = x &(I) \\ 0\leq x \lt y &(II) \end{array} \end{equation*} (I) follows by reflexivity of equality and corresponds to [3]. The first inequality of (II) follows by assumption and corresponds to [2]. The second part is a consequence of the current case distinction and corresponds to [1]. Case $$x\geq y\text{.}$$ To show: \begin{equation*} \begin{array}{cl} m'\cdot y + r' + y = x &(I) \\ 0\leq r' \geq y &(II) \end{array} \end{equation*} for $$(m',r') = div~(x-y)~y\text{.}$$ We have $$x'=x-y > 0$$ from $$x\geq y$$ (current case). This step corresponds to [a]. To apply the induction hypothesis, $$x'=x-y \lt x$$ is needed which follows from the assumption $$y>0\text{.}$$ We get: \begin{equation*} \begin{array}{cl} m'\cdot y + r' = x-y &(IH_I) \\ 0\leq r' \geq y &(IH_{II}) \end{array} \end{equation*} (II) is a direct consequence of $$(IH_{II})$$ and corresponds to [c]. (I) follows from $$(IH_I)$$ using arithmetic and corresponds to [b]. ##### 10.Programs. Give programs that make the following Hoare triples valid for any Q. 1. $$\displaystyle \vdash\hoare{Q}{?}{\lfalse}$$ 2. $$\displaystyle \vdash\hoare{Q}{?}{\ltrue}$$ 3. $$\displaystyle \vdash\hoare{\lfalse}{?}{Q}$$ 4. $$\displaystyle \vdash\hoare{\ltrue}{?}{Q}$$ 202207281550 202207081400 Solution. 1. \begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare{Q\land\ltrue}{\{\}}{Q}$} \UnaryInfC{$\vdash\hoare{Q}{\texttt{while ($\ltrue$) \{\}}}{Q\land\neg\ltrue}$} \end{prooftree} \end{equation*} 2. \begin{equation*} \begin{prooftree} \AxiomC{$Q\simp\ltrue$} \AxiomC{} \UnaryInfC{$\vdash\hoare{\ltrue}{\{\}}{\ltrue}$} \BinaryInfC{$\vdash\hoare{Q}{\{\}}{\ltrue}$} \end{prooftree} \end{equation*} 3. \begin{equation*} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\hoare{\lfalse}{\texttt{abort();}}{Q}$} \end{prooftree} \end{equation*} 4. \begin{equation*} \begin{prooftree} \AxiomC{$\lfalse\simp Q$} \AxiomC{} \UnaryInfC{$\vdash\hoare{\ltrue\land\ltrue}{\{\}}{\ltrue}$} \UnaryInfC{$\vdash\hoare{\ltrue}{\texttt{while ($\ltrue$) \{\}}}{\ltrue\land\neg\ltrue}$} \BinaryInfC{$\vdash\hoare{\ltrue}{\texttt{while ($\ltrue$) \{\}}}{Q}$} \end{prooftree} \end{equation*} ##### 11.ReLU. Verify the following program d = x - y; if (d < 0) r = 0; else r = d;  against the specification $$(P,Q)$$ \begin{equation*} P = \ltrue \qquad Q = \underbrace{(\texttt{x - y < 0} \land \texttt{r = 0})}_{Q_1} \lor \underbrace{(\texttt{x - y >= 0} \land \texttt{r = x - y})}_{Q_2}. \end{equation*} 202207281550 202207081400 Solution. Let $$R := (\texttt{d == x - y})\text{.}$$ ##### 12.Primes. Consider the following algorithm to detect if a number is a prime or not: r = 1; i = 2; while (i < n) { // \ if (n % i == 0) // \ r = 0; // } =: s i++; // / } // /  Come up with a specification that expresses that the program checks if a number is a prime or not and verify it against that specification. 202207281550 202207081400 Solution. Let $$R := \texttt{r == 1} \liff\forall x. \texttt{x > 1 \limp x < n \limp n \% x != 0}\text{.}$$ Let $$I := i > 1 \land (\texttt{r == 1} \liff\forall x. \texttt{x > 1 \limp x < i \limp n \% x != 0})\text{.}$$ Let $$I' := i + 1 > 1 \land (\texttt{r == 1} \liff\forall x. \texttt{x > 1 \limp x < i + 1 \limp n \% x != 0})\text{.}$$ Let $$I'' := \texttt{r == 0}\land\texttt{i > 1}\land\texttt{n \% i == 0}\text{.}$$ Let $$I''' := \texttt{n \% i == 0}\land \texttt{i > 1}\text{.}$$ ##### 13.Soundness of if-then-else. Sketch a soundness proof for the if-then-else rule. Take the proof sketch for the block rule as a template. 202207281550 202207081400 Solution. The if-then-else rule is \begin{equation*} \begin{prooftree} \AxiomC{$\vdash\hoare{e\land P}{s_1}{Q}$} \AxiomC{$\vdash\hoare{\neg e\land P}{s_2}{Q}$} \BinaryInfC{$\vdash \hoare{\exprdef e\land P}{\CIf{e}{s_1}{s_2}}{Q} $} \end{prooftree}. \end{equation*} The induction hypothesis tells us that the Hoare triples in the premises are sound, so we have $$\models\hoare{e\land P}{s_1}{Q}$$ and $$\models\hoare{\neg e\land P}{s_2}{Q}\text{.}$$ We need to show that: \begin{equation*} \forall\sigma.\,(\sigma\models \exprdef e \land P)\limp \left(\forall c.\config{\CIf{e}{s_1}{s_n}}\sigma\bigstep c \limp(\exists \sigma'.\,c=\sigma'\land\sigma'\models Q)\right) \end{equation*} Let $$\sigma$$ be a state such that $$\sigma\models\exprdef e\land P$$ and let $$c$$ be a configuration such that \begin{equation*} \config{\CIf{e}{s_1}{s_n}}\sigma\bigstep c \end{equation*} holds. Because of $$\sigma\models\exprdef e\land P$$ we either have $$\sigma\models e\land P$$ or $$\sigma\models\neg e\land P\text{.}$$ Assume without loss of generality (the other case is analogous) that $$\sigma\models e\land P\text{.}$$ By inversion of the big step semantics we know that $$\config{s_1}{\sigma}\bigstep c\text{.}$$ If $$c$$ is not a state (i.e. $$\config{s_1}{\sigma}$$ gets stuck or is aborted), then this would contradict the first induction hypothesis $$\models\hoare{e\land P}{s_1}{Q}\text{.}$$ Thus, $$\config{s_1}{\sigma}$$ must terminate properly in some state $$\sigma'$$ with \begin{equation*} c = \sigma' \land\sigma'\models Q, \end{equation*} concluding the proof. #### All in one ##### 14.GCD. Consider the following C0 program that computes the greatest common divisor: while (a != b) if (a > b) // \ a = a - b; // \ else // } =: s b = b - a; // /  1. Compute the static semantics of this program. 2. Generate MIPS machine code for it according to the rules of the lecture. 3. Verify that this program is correct with respect to the specification $$(P,Q)$$ \begin{equation*} P = \texttt{a > 0} \land \texttt{b > 0}\land A == a\land B == b \qquad Q = \texttt{a == }\textit{gcd}(A,B) \end{equation*} Hint: Pick an appropriate loop invariant. 202207281550 202207081400 Solution. 1. Static semantics: 2. gcd: .globl subiu$sp $sp 12 sw$ra 8($sp) sw$a0 0($sp) sw$a1 4($sp) # c_while b T L: # c_if # c_binary # c_var addiu$t0 $sp 0 # c_LtoR lw$t0 $t0 # c_var addiu$t1 $sp 4 # c_LtoR lw$t1 $t1 slt$t0 $t1$t0
beqz  $t0 F # c_assign # c_binary # c_var addiu$t0 $sp 0 # c_LtoR lw$t0 $t0 # c_var addiu$t1 $sp 4 # c_LtoR lw$t1 $t1 subu$t0 $t0$t1
sw    $t0 0($sp)
b N
F:
# c_assign
# c_binary
# c_var
addiu $t0$sp 0
# c_LtoR
lw    $t0$t0
# c_var
addiu $t1$sp 4
# c_LtoR
lw    $t1$t1
subu  $t1$t0 $t1 sw$t1 4($sp) N: T: # c_binary # c_var addiu$t0 $sp 0 # c_LtoR lw$t0 $t0 # c_var addiu$t1 $sp 4 # c_LtoR lw$t1 $t1 xor$t0 $t0$t1
bnez  $t0 L gcd_end: # c_var addiu$t0 $sp 0 # c_LtoR lw$t0 $t0 addiu$v0 $t0 0 lw$ra 8($sp) addiu$sp $sp 12 jr$ra

Run
3. Let $$I := \texttt{a > 0 \land b > 0 }\land\textit{gcd}(\texttt{a,b})\texttt{ == }\textit{gcd}(A,B)\text{.}$$

The remaining proof obligation is (and analogously with a and b swapped):

\begin{equation*} I\land a > b\simp I[a-b/b]. \end{equation*}

Let $$a > b > 0$$ and let $$x\defeq\textit{gcd}(a,b)\text{.}$$ We have to show:

1. $$\displaystyle a - b > 0$$

2. $$\displaystyle b > 0$$

3. $$\displaystyle \textit{gcd}(a-b,b) = x\ (= \textit{gcd}(a,b) = \textit{gcd}(A,B))$$

The goals (i) and (ii) follow directly from the assumptions.

By the definition of $$\textit{gcd}\text{,}$$ there are $$n,m > 0$$ such that $$a = n x$$ and $$b = m x\text{,}$$ and $$x$$ is the greatest natural number with that property. Furthermore, we have $$n > m$$ and $$n - m > 0$$ and $$a - b = nx - mx = (n-m)x\text{.}$$ Thus $$x$$ is also a common divisor of $$a-b$$ and $$b\text{.}$$

Assume there is another common divisor $$x' > x\text{.}$$ Then there are $$n',m' > 0$$ such that:

\begin{equation*} a-b = n'x' \land b = m'x' \end{equation*}

But then we would have

\begin{equation*} a = n'x' + m'x' = (n'+m')x' \end{equation*}

and $$x'$$ would also be a common divisor of $$a$$ and $$b$$ which is a contradiction to the assumption $$x = \textit{gcd}(a,b)\text{.}$$

Consequently, $$\textit{gcd}(a-b,b) = x\text{.}$$