Changeset 1743
 Timestamp:
 Feb 24, 2012, 3:45:54 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1742 r1743 317 317 \begin{center} 318 318 \begin{picture}(2, 2) 319 \put(0,20){\framebox(25,25)[c]{\texttt{v}}} 320 \put(26,20){\framebox(25,25)[c]{\texttt{4}}} 321 \put(51,20){\framebox(25,25)[c]{\texttt{cont}}} 322 \put(76,20){\framebox(25,25)[c]{\texttt{cont}}} 323 \put(101,20){\framebox(25,25)[c]{\texttt{cont}}} 319 \put(150,20){\framebox(25,25)[c]{\texttt{v}}} 320 \put(125,20){\framebox(25,25)[c]{\texttt{4}}} 321 \put(100,20){\framebox(25,25)[c]{\texttt{cont}}} 322 \put(75,20){\framebox(25,25)[c]{\texttt{cont}}} 323 \put(50,20){\framebox(25,25)[c]{\texttt{cont}}} 324 \put(15,10){\vector(1, 0){30}} 325 \put(25,20){\framebox(25,25)[c]{\texttt{\texttt{v1}}}} 326 \put(50,20){\framebox(25,25)[c]{\texttt{\texttt{v2}}}} 327 \put(75,20){\framebox(25,25)[c]{\texttt{\texttt{v3}}}} 328 \put(100,20){\framebox(25,25)[c]{\texttt{\texttt{v4}}}} 324 329 \end{picture} 325 330 \end{center} … … 331 336 \begin{displaymath} 332 337 \sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M) 338 \end{displaymath} 339 340 \begin{displaymath} 341 \texttt{load}^* (\mathtt{store}\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M) 333 342 \end{displaymath} 334 343 … … 382 391 383 392 \begin{displaymath} 384 \begin{diagram} 385 \mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME) 386 \end{diagram} 387 \end{displaymath} 393 \begin{array}{rcl} 394 \mathtt{Call(id,\ args,\ dst,\ pc),\ State(FRAME, FRAMES)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\ 395 & & \mathtt{PUSH(current\_frame[PC := after\_return])} 396 \end{array} 397 \end{displaymath} 398 399 In the case where the call is to an external function, we have: 400 401 \begin{displaymath} 402 \begin{array}{rcl} 403 \mathtt{Call(M(args), dst)}, & \stackrel{\mathtt{ret\_val = f(M(args))}}{\longrightarrow} & \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} \\ 404 \mathtt{PUSH(current\_frame[PC := after\_return])} & & 405 \end{array} 406 \end{displaymath} 407 408 then: 409 410 \begin{displaymath} 411 \begin{array}{rcl} 412 \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} 413 \end{array} 414 \end{displaymath} 415 416 In the case where the call is to an internal function, we have: 388 417 389 418 \begin{displaymath} … … 396 425 \begin{displaymath} 397 426 \begin{array}{rcl} 427 \mathtt{Call(M(args), dst)} & \longrightarrow & \mathtt{sp = alloc}, regs = \emptyset[ := PARAMS] \\ 428 \mathtt{PUSH(current\_frame[PC := after\_return])} & & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst) 429 \end{array} 430 \end{displaymath} 431 432 then: 433 434 \begin{displaymath} 435 \begin{array}{rcl} 436 \mathtt{sp = alloc}, regs = \emptyset[ := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\ 437 \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst) & & \mathtt{Return(M(ret\_val), dst, frames)} 438 \end{array} 439 \end{displaymath} 440 441 and finally: 442 443 \begin{displaymath} 444 \begin{array}{rcl} 445 \mathtt{free(sp)} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\ 446 \mathtt{Return(M(ret\_val), dst, frames)} & & 447 \end{array} 448 \end{displaymath} 449 450 \begin{displaymath} 451 \begin{array}{rcl} 398 452 \sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\ 399 453 \sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register} 400 \end{array} 454 \end{array} 401 455 \end{displaymath} 402 456
Note: See TracChangeset
for help on using the changeset viewer.