1(* 2 fun load_path_add x = loadPath := !loadPath @ [concat Globals.HOLDIR x]; 3 load_path_add "/examples/mc-logic"; 4 load_path_add "/examples/ARM/v4"; 5 load_path_add "/tools/mlyacc/mlyacclib"; 6 app load ["arm_compilerLib", "wordsTheory"] 7*) 8 9open HolKernel boolLib bossLib Parse; 10open arm_compilerLib; 11open wordsTheory; 12 13val _ = optimise_code := true; 14val _ = abbrev_code := false; 15 16val _ = new_theory "arm_compiler_demo"; 17 18(* 19 20INTRODUCTION 21 22This file illustrates, through examples, how the ARM compiler from 23arm_progLib can be used. The compiler's top-level function is 24 25 arm_progLib.arm_compile (def:thm) (ind:thm) (as_proc:arm_code_format) 26 27Here def is a definition, ind is the induction rule produced by Define 28and as_proc is a flag indicating what the format of the resulting ARM 29code ought to take (e.g. procedure or not). 30 31In order to keep the presentation consice we define test_compile and 32test_compile_proc: 33 34*) 35 36fun find_ind_thm def = let 37 val tm = (fst o dest_eq o concl o SPEC_ALL) def 38 val name = (fst o dest_const) ((fst o dest_comb) tm handle e => tm) 39 in fetch "-" (name^"_ind") handle e => TRUTH end; 40 41fun test_compile' as_proc q = let 42 val def = Define q 43 val ind = find_ind_thm def 44 val (th,strs) = arm_compile def ind as_proc 45 (* val _ = map print (["\n\n\n"] @ strs @ ["\n\n\n"]) *) 46 in (def,ind,th) end; 47 48fun test_compile q = test_compile' InLineCode q; 49val test_compile_proc = test_compile' 50 51(* 52 53The compiler expects def to be a function where variables have names 54r0,r1,r2,...,r12 or m0,m1,m2 .... The variable names tells the compiler 55how to assign physical resources to each logical variable, e.g. 56 57 r1 - becomes register 1 58 m5 - becomes memory location at address stack pointer + 5 59 60The functions it accepts must conform to the following grammar. 61Let r range over register names (r0,r1,r2,etc), m range over 62memory locations (m0,m1,m2,etc), f over function names, 63i over natural numbers (<32) and w over 8-bit word constants. 64 65 p ::= let r = exp in p 66 | let m = r in p 67 | let (v,v,...,v) = f (v,v,...,v) in p 68 | if g then p else p 69 | (v,v,...,v) 70 71 v ::= r | m 72 g ::= ~ g | r cmp mode | r && mode = 0w 73 cmp ::= = | < | <+ | <= | <=+ 74 exp ::= m | mode | ~ mode | r op mode | r * r 75 op ::= + | - | && | ?? | !! 76 mode ::= w | r | r << i | r >> i | r >>> i 77 78The only dissallowed combination of the above is "let ri = rj * rk in ..." 79in which ri and rj must not be the same variable name. (There are also some 80restrictions regarding varaible names in function calls.) 81 82Notice that the grammer from above dissallows: 83 84 let r0 = (if r1 < r2 then 5w else r6) in P 85 86Such conditionals need to be expanded out, e.g. 87 88 if r1 < r2 then 89 let r0 = 5w in P 90 else 91 let r0 = r6 in P 92 93A naive compilation would duplicate the code for P. We optimise 94"common code tails" and that way, to a large extent, avoid duplication 95of code (See section of shared-tails for more). 96 97*) 98 99 100(* TEST: constant functions *) 101 102val (load_const_def,_,load_const_arm) = test_compile ` 103 load_const : word32 # word32 # word32 = 104 let r0 = 0w in 105 let r1 = 45w in 106 let r2 = ~r1 in 107 (r0,r1,r2)`; 108 109(* Each let-expression is compiled into one ARM instruction or 110 procedure call. The code for load_const above becomes: 111 112 mov r0, #0 113 mov r1, #45 114 mvn r2, r1 115*) 116 117 118(* TEST: nonrecursive functions *) 119 120val (garble_def,_,garble_arm) = test_compile ` 121 garble (r2:word32,r3:word32,r4:word32) = 122 let r1 = r2 + r3 in 123 let r2 = r1 - r3 << 5 in 124 let r3 = r2 * r3 in 125 let r1 = r1 + 4w in 126 let r2 = r3 && r2 >>> 30 in 127 let r2 = r2 << 16 in 128 let r2 = ~(r2 >>> 2) in 129 let r3 = r2 !! r1 in 130 let r2 = r3 ?? 55w in 131 (r2,r3)`; 132 133(* Input and output are tuples. For garble_def we expect input in 134 register 2, 3 and 4; and produce output into registers 2 and 3. *) 135 136 137(* TEST: recursive functions *) 138 139val (mul32_def,mul32_ind,mul32_arm) = test_compile ` 140 mul32 (r0:word32,r1:word32,r2:word32) = 141 if r0 = 0w then (r0,r1,r2) else 142 let r2 = r1 + r2 in 143 let r0 = r0 - 1w in 144 mul32 (r0,r1,r2)`; 145 146val (fac32_def,fac32_ind,fac32_arm) = test_compile ` 147 fac32 (r0:word32,r1:word32) = 148 if r0 = 0w then r1 else 149 let r1 = r0 * r1 in 150 let r0 = r0 - 1w in 151 fac32 (r0,r1)`; 152 153(* Looping functions are required to be tail-recursive and 154 the recurive calls need to be identical to the left-hand side of 155 the definition of the function, i.e. 156 157 f (r1,r2) = let .... in f (r2,r3) 158 159 is not allowed, since (r1,r2) is not syntactically the same as (r2,r3). *) 160 161 162(* TEST: functions with multiple recursive calls *) 163 164val (recg_def,recg_ind,recg_arm) = test_compile ` 165 recg (r0:word32,r1:word32) = 166 if r0 = 0w then 167 r1 168 else if r0 = 2w then 169 (let r2 = r0 && r1 in r1) 170 else if r0 = r1 then 171 (let r2 = 5w:word32 in 172 let r3 = ~r2 in 173 let r1 = r0 * r1 in 174 let r0 = r0 - 1w in 175 recg(r0,r1)) 176 else 177 (let r1 = r0 * r1 in 178 let r3 = ~r1 in 179 let r0 = r0 - 1w in 180 recg(r0,r1))`; 181 182 183(* TEST: negative guard in if-then-else *) 184 185val (neg_test_def,_,neg_test_arm) = test_compile ` 186 neg_test (r0:word32,r1:word32) = 187 let r1 = r0 + r1 in 188 if ~(r0 = 0w) then 189 let r1 = r0 + r1 in 190 r1 191 else 192 let r1 = r1 + 4w in 193 r1`; 194 195 196(* TEST: various guards *) 197 198val (guard_test_def,_,guard_test_arm) = test_compile ` 199 guard_test (r0:word32,r1:word32,r2:word32,r3:word32) = 200 if 5w <= r2 then let r0 = r1 + 2w in r0 else 201 if r0 <+ 3w then let r0 = r1 + 3w in r0 else r0`; 202 203val (guard_test_def,_,guard_test_arm) = test_compile ` 204 guard_test (r0:word32,r1:word32,r2:word32,r3:word32) = 205 if r0 <= r2 then let r0 = r1 + 2w in r0 else 206 if r0 <+ 3w then let r0 = r1 + 3w in r0 else 207 if ~(r0 < 3w) then let r0 = r1 + 5w in r0 else 208 if r0 <+ r3 << 2 then let r0 = r1 + 6w in r0 else 209 if r3 << 2 <+ r3 then let r0 = r1 + 7w in r0 else 210 if ~(r3 >> 2 <+ r3) then let r0 = r1 + 8w in r0 else r0`; 211 212val (guard_loop_def,guard_loop_ind,guard_loop_arm) = test_compile ` 213 guard_loop (r0:word32) = 214 if r0 = 0w then r0 else 215 if r0 < 3w then 216 let r0 = r0 - 1w in guard_loop(r0) 217 else 218 let r0 = r0 - 1w in guard_loop(r0)` 219 220(* Notice that one of the branches in same_guard_def is unreachable. 221 The compiler will be unable to prove the unreachable path and drops it. 222 Hence the message from the compiler *) 223 224val (same_guard_def,_,same_guard_arm) = test_compile ` 225 same_guard (r0:word32,r1:word32,r2:word32,r3:word32) = 226 if r0 < 3w then let r0 = r1 + 1w in r0 else 227 if r0 < 3w then let r0 = r1 + 3w in r0 else r0`; 228 229 230(* TEST: conditional execution *) 231 232(* Here the compiler does not introduce a branch instead it executes 233 the addition conditionally. *) 234 235val (reg_min_def,_,reg_min_arm) = test_compile ` 236 reg_min (r0:word32,r1:word32) = 237 if r0 < r1 then 238 let r1 = r1 + r0 in r1 239 else 240 r1`; 241 242 243(* TEST: if-then-else shared tail elim *) 244 245(* In order to avoid duplication of code the compiler can pull out 246 tails that are shared across if-then-else branches. *) 247 248val (shared_tail_def,_,shared_tail_arm) = test_compile ` 249 shared_tail (r0:word32,r1:word32,r2:word32) = 250 if r1 < r2 then 251 let r1 = r2 in 252 let r0 = r1 + 5w in 253 let r2 = r0 + r1 in 254 r2 255 else 256 let r0 = r1 + 5w in 257 let r2 = r0 + r1 in 258 r2`; 259 260val (shared_tail2_def,_,shared_tail2_arm) = test_compile ` 261 shared_tail2 (r0:word32,r1:word32,r2:word32) = 262 if r1 < r2 then 263 if r2 < r0 then 264 let r1 = r2 + 1w in 265 let r0 = r1 - 5w in 266 let r0 = r0 - 5w in 267 r0 268 else 269 let r1 = r2 + 2w in 270 let r0 = r1 - 5w in 271 let r0 = r0 - 5w in 272 r0 273 else 274 if r2 < 5w then 275 let r1 = r2 + 3w in 276 let r0 = r1 - 5w in 277 let r0 = r0 - 5w in 278 r0 279 else 280 let r1 = r2 + 4w in 281 let r0 = r1 - 5w in 282 let r0 = r0 - 5w in 283 r0`; 284 285 286(* TEST: if-the-else shared front can be pulled out *) 287 288(* In some cases the front can be pulled out as illustrated 289 by the following code. The comparison instruction comes first 290 in the compiled code, then the move and the addition and at 291 the end subtraction is done conditionally. *) 292 293val (shared_front_def,_,shared_front_arm) = test_compile ` 294 shared_front (r0:word32,r1:word32,r2:word32) = 295 if r1 < r2 then 296 let r1 = 5w in 297 let r2 = r1 + r2 in 298 r2 299 else 300 let r1 = 5w in 301 let r2 = r1 + r2 in 302 let r2 = r2 - 4w in 303 r2`; 304 305 306(* TEST: memory accesses *) 307 308(* Memory accesses to the stack are done using variables names 309 m0,m1,m2 etc. Memory locations cannot be refered to in 310 expressions, e.g. 311 312 let m1 = m2 + 5w in ... 313 314 is not allowed, since there is no ARM instruction for 315 addition of memory locations. Instead: 316 317 let r0 = m2 in 318 let m1 = r0 + 5w in ... 319 320*) 321 322val (mem_swap_def,_,mem_swap_arm) = test_compile ` 323 mem_swap (m0:word32,m1:word32) = 324 let r0 = m0 in 325 let r1 = m1 in 326 let m0 = r1 in 327 let m1 = r0 in 328 (m0,m1)`; 329 330val (mem_as_temp_def,_,mem_as_temp_arm) = test_compile ` 331 mem_as_temp (r0:word32,r1:word32,r2:word32) = 332 let m1 = r0 in 333 let r1 = r1 + r2 in 334 let m2 = r1 in 335 let r2 = r1 + r2 in 336 let m3 = r2 in 337 m3`; 338 339 340(* TEST: function in-lining *) 341 342(* The compiler keeps track of previously compiled code. In order to 343 flush its memory call: 344 345 reset_compiled() 346*) 347 348val _ = reset_compiled(); 349 350val (fac32_acc_def,fac32_acc_ind,fac32_acc_arm) = test_compile ` 351 fac32_acc (r0:word32,r1:word32) = 352 if r0 = 0w then r1 else 353 let r1 = r0 * r1 in 354 let r0 = r0 - 1w in 355 fac32_acc (r0,r1)`; 356 357val (fac32_def,_,fac32_arm) = test_compile ` 358 fac32 (r0:word32) = 359 let r1 = 1w in 360 let r1 = fac32_acc (r0,r1) in 361 let r0 = r1 in 362 r0`; 363 364(* fac32 contains an instance of fac32_acc. Make sure that the 365 call to fac32_acc uses the variable names with which fac32_acc 366 was defined, e.g. calling it using 367 368 let r1 = fac32_acc (r3,r4) in 369 370 is not allowed since (r3,r4) is not syntactically equal to (r0,r1) 371 which was used in the definition of fac32_acc; similarly 372 373 let r9 = fac32_acc (r0,r1) in 374 375 is also malformed since the result of fac32_acc is stored in r0, 376 not in r9. 377*) 378 379(* 380-- fac_add_def makes Holmake fail, but works when run in an interacitve session 381 382val (fac_add_def,_,fac_add_arm) = test_compile ` 383 fac_add (r0:word32,r2:word32) = 384 let r0 = fac32(r0) in 385 let r0 = r0 + r2 in 386 r0`; 387*) 388 389(* Note that the compilation of fac_add would rightly fail, if r2 was 390 replaced by r1 in the definition of fac_add, since r1 is used 391 when fac32 executes. *) 392 393 394 395(* TEST: procedure calls *) 396 397val _ = reset_compiled(); 398 399(* If we compile fac32_acc as a procedure then calls to it will be 400 executed using the ARM instruction for procedure calls, i.e. 401 the BL (branch-and-link) instruction. *) 402 403val (fac32_acc_def,fac32_acc_ind,fac32_acc_arm) = test_compile_proc SimpleProcedure ` 404 fac32_acc (r0:word32,r1:word32) = 405 if r0 = 0w then r1 else 406 let r1 = r0 * r1 in 407 let r0 = r0 - 1w in 408 fac32_acc (r0,r1)`; 409 410val (fac32_def,_,fac32_arm) = test_compile ` 411 fac32 (r0:word32) = 412 let r1 = 1w in 413 let r1 = fac32_acc (r0:word32,r1:word32) in 414 let r0 = r1 in 415 r0`; 416 417(* Here fac32_acc was compiled using the option "SimpleProcedure", which means 418 that it will keep the return address in the link register (register 14) rather 419 than push it onto the stack. Functions compiled with the option 420 "SimpleProcedure" must not contain any procedure calls or direct use of 421 register 14. 422 423 Use the option "PushProcedure ([],0)" when the function to be compiled contains 424 procedure calls or uses register 14 as a temporary (which is allowed!). 425 The option "PushProcedure ([],0)" will push the return address onto the stack and 426 hence allows nested procedure calls. 427*) 428 429val (b1_def,_,b1_arm) = test_compile_proc (PushProcedure ([],0)) ` 430 b1 (r0:word32,r1:word32) = 431 let r0 = r1 * r0 in 432 r0`; 433 434val (b2_def,_,b2_arm) = test_compile_proc (PushProcedure ([],0)) ` 435 b2 (r0:word32,r1:word32,r2:word32) = 436 let r0 = b1(r0,r1) in 437 let r0 = r0 + r2 in 438 r0`; 439 440val (b3_def,_,b3_arm) = test_compile_proc (PushProcedure ([],0)) ` 441 b3 (r0:word32,r1:word32,r2:word32) = 442 let r0 = b2(r0,r1,r2) in 443 let r1 = r0 - 4w in 444 r1`; 445 446(* The option "PushProcedure" can also be used for context saving, e.g. 447 `PushProcedure (["r1","r2","r3"],0)` saves the state of registers 1, 2 and 3 448 (by pushing their values onto the stack on entry and popping them on exit). 449 450 Example: the function c1 (below) uses registers 11 and 12 as temporaries and 451 function c2 (also below) depends on the fact that the values in registers 11 452 and 12 are invariant across calls to c1. 453*) 454 455val (c1_def,_,c1_arm) = test_compile_proc (PushProcedure (["r11","r12"],0)) ` 456 c1 (r0:word32,r1:word32) = 457 let r11 = 5w in 458 let r12 = 6w in 459 let r0 = r1 * r11 in 460 let r0 = r0 ?? r12 in 461 r0`; 462 463val (c2_def,_,c2_arm) = test_compile_proc (PushProcedure ([],0)) ` 464 c2 (r0:word32,r1:word32,r11:word32) = 465 let r12 = r11 + r1 in 466 let r0 = c1(r0,r1) in 467 let r0 = r0 + r11 in 468 let r1 = r0 - r12 in 469 (r0,r1)`; 470 471 472(* TEST: procedure calls with memory accesses *) 473 474(* So far we have required that procedure/function calls are identical 475 to the definition of the function which they call, e.g. a call to 476 foo, defined by 477 478 foo (r0,m1) = 479 let ... in (r3,m2) , 480 481 must be of the form "let (r3,m2) = foo(r0,m1)", since the variable 482 names indicate in which resources the input/result values are stored. 483 484 However, the new option PushProcedure is an exception to the above 485 rule of thumb. The option PushProcedure alters the stack pointer, and 486 hence what used to be at offset, say, 5 from the stack pointer (i.e. m5) 487 may actually be at offset 6 (i.e. m6) from inside a subroutine. As 488 a result the numbers that follow variable names that refer to the stack 489 need to be shifted slightly when calling procedures that are complied 490 using PushProcedure. Example: 491*) 492 493val _ = reset_compiled(); 494 495(* foo is compiled to push the link register onto the stack. *) 496 497val (foo_def,_,foo_arm) = test_compile_proc (PushProcedure ([],0)) ` 498 foo (r0:word32,m1:word32) = 499 let r1 = m1 in 500 let r3 = r0 + r1 in 501 let r1 = r1 + 4w in 502 let m2 = r1 in 503 (r3,m2)`; 504 505(* When calling foo we must use "let (r3,m1) = foo(r0,m0)" since 506 the stack pointer is shifted by one *) 507 508val (supfoo_def,_,supfoo_arm) = test_compile_proc InLineCode ` 509 supfoo (r0,m0) = 510 let (r3,m1) = foo(r0,m0) in 511 let r2 = m1 in 512 (r2,r3)`; 513 514(* To illustrate how the stack elements work, let the following depict 515 a stack with q at the top, then z as the second element, then y and x, 516 517 ...|x|y|z|q| 518 519 One uses offset 0 to access q, offset 2 to access y. 520 521 Suppose we run supfoo on a stack with y on top and x second 522 523 ...|x|y| 524 525 then the execution starts by performing a call to foo, which pushes 526 the return address onto the stack: 527 528 ...|x|y|address| 529 530 We see that what used to be at offset i from the top of the stack 531 is now at offset i+1. When the procedure returns it pops the return 532 address off the stack, hence when "let r2 = m1" is to execute the 533 stack is the following (here z is the value which foo calculated): 534 535 ...|z|y| 536 537 The general case: PushProcedure (xs,i) will shift the stack pointer 538 by length xs + i + 1. 539*) 540 541 542 543(* TEST: procedure calls with register spilling *) 544 545(* Suppose all values used in a computation don't fit into the registers. 546 We can create temporary stack space by altering the stack poniter in 547 procedures that are compiled using the option PushProcedure. 548 549 PushProcedure (xs,i) shifts the stack pointer i steps, e.g. 550 When entering a function compiled with the option 551 PushProcedure (["r1","r2","r3"],2) it will start by pushing the return 552 address and values of registers 1, 2 and 3 onto the stack 553 554 ...|address|v1|v2|v3| 555 556 It then alters the stack pointer to add two more elements: 557 558 ...|address|v1|v2|v3|t1|t2| 559 560 The stack locations where address,v1,v2,v3 are stored (i.e. m5,m4,m3,m2) 561 must not be touched since these are used by the procedure context switch. 562 But the stack locations where the (unspecified) t1 and t2 are stored can be 563 used temporary scratch space. 564 565 Example below. 566*) 567 568val (temp_mem_def,_,temp_mem_arm) = test_compile_proc (PushProcedure (["r1","r2","r3"],2)) ` 569 temp_mem (r0:word32,m6:word32) = 570 let m0 = r0 in (* offset 0 used as temp *) 571 let r0 = m6 in (* offset 6 used as input *) 572 let r0 = r0 - 5w in 573 let m1 = r0 in (* offset 1 used as temp *) 574 let r1 = m1 in 575 let r1 = r1 + 6w in 576 let m7 = r1 in (* offset 7 used as result *) 577 let r0 = r1 + r0 in 578 (r0,m7)`; 579 580(* When "let m0 = r0" executes in temp_mem the stack is the following: 581 582 ...|x|y|address|v1|v2|v3|t1|t2| 583 584 temp_mem reads offset 6 (i.e. y) as input use offset 0 and 1 as temporary 585 memory locations and uses offset 7 to return output. 586*) 587 588val (temp_mem2_def,_,temp_mem2_arm) = test_compile_proc (PushProcedure (["r1"],3)) ` 589 temp_mem2 (r2:word32,r3:word32) = 590 let r0 = r2 + r3 in 591 let m0 = r0 in 592 let (r0,m1) = temp_mem(r0,m0) in 593 let r1 = m1 in 594 let r2 = r1 + r3 in 595 r2`; 596 597(* When "let r0 = r2 + r3" executes in temp_mem2 the stack is the following: 598 599 ...|address'|u1|t1|t2|t3| 600*) 601 602 603 604(* Joe's ECC example. *) 605 606(* The code becomes large in the following examples. 607 Hence, in order to cope we switch on "code abbrevaition". *) 608 609val _ = abbrev_code := true; 610val _ = reset_compiled(); 611 612val (load_751_def,_,load_751_arm) = test_compile ` 613 load_751 = 614 let r10 = 2w:word32 in 615 let r10 = r10 << 8 in 616 let r10 = r10 + 239w in r10`; 617 618val (field_neg_def,_,field_neg_arm) = test_compile ` 619 field_neg (r1:word32) = 620 if r1 = 0w then r1 else 621 let r10 = load_751 in 622 let r1 = r10 - r1 in r1`; 623 624val (field_add_def,_,field_add_arm) = test_compile ` 625 field_add (r0:word32,r1:word32) = 626 let r10 = load_751 in 627 let r0 = r1 + r0 in 628 if r0 < r10 then r0 else 629 let r0 = r0 - r10 in 630 r0`; 631 632val (field_sub_def,_,field_sub_arm) = test_compile ` 633 field_sub (r0,r1) = 634 let r1 = field_neg r1 in 635 let r0 = field_add (r0,r1) in 636 r0`; 637 638val (field_mult_aux_def,field_mult_aux_ind,field_mult_aux_arm) = test_compile ` 639 field_mult_aux (r2:word32,r3:word32,r4:word32) = 640 if r3 = 0w then r4 else 641 if r3 && 1w = 0w then 642 let r3 = r3 >>> 1 in 643 let r0 = r2 in 644 let r1 = r2 in 645 let r0 = field_add (r0,r1) in 646 let r2 = r0 in 647 field_mult_aux (r2:word32,r3:word32,r4:word32) 648 else 649 let r3 = r3 >>> 1 in 650 let r0 = r4 in 651 let r1 = r2 in 652 let r0 = field_add (r0,r1) in 653 let r4 = r0 in 654 let r0 = r2 in 655 let r1 = r2 in 656 let r0 = field_add (r0,r1) in 657 let r2 = r0 in 658 field_mult_aux (r2:word32,r3:word32,r4:word32)`; 659 660val (field_mult_def,_,field_mult_arm) = test_compile' SimpleProcedure ` 661 field_mult (r2,r3) = 662 let r4 = 0w in 663 let r4 = field_mult_aux (r2,r3,r4) in 664 r4`; 665 666val (field_exp_aux_def,field_exp_aux_ind,field_exp_aux_arm) = test_compile ` 667 field_exp_aux (r5:word32,r6:word32,r7:word32) = 668 if r6 = 0w then r7 else 669 if r6 && 1w = 0w then 670 let r6 = r6 >>> 1 in 671 let r2 = r5 in 672 let r3 = r5 in 673 let r4 = field_mult (r2,r3) in 674 let r5 = r4 in 675 field_exp_aux (r5:word32,r6:word32,r7:word32) 676 else 677 let r6 = r6 >>> 1 in 678 let r2 = r7 in 679 let r3 = r5 in 680 let r4 = field_mult (r2,r3) in 681 let r7 = r4 in 682 let r2' = r5 in 683 let r3' = r5 in 684 let r4' = field_mult (r2',r3') in 685 let r5 = r4' in 686 field_exp_aux (r5:word32,r6:word32,r7:word32)`; 687 688val (field_exp_def,_,field_exp_arm) = test_compile' (PushProcedure ([],0)) ` 689 field_exp (r5,r6) = 690 let r7 = 1w in 691 let r7 = field_exp_aux (r5,r6,r7) in 692 r7`; 693 694val (field_inv_def,_,field_inv_arm) = test_compile' (PushProcedure ([],0)) ` 695 field_inv r5 = 696 let r6 = 2w:word32 in 697 let r6 = r6 << 8 in 698 let r6 = r6 + 237w in 699 let r7 = field_exp (r5,r6) in 700 r7`; 701 702val (field_div_def,_,field_div_arm) = test_compile' (PushProcedure ([],0)) ` 703 field_div (r8,r9) = 704 let r5 = r9 in 705 let r7 = field_inv r5 in 706 let r2 = r8 in 707 let r3 = r7 in 708 let r4 = field_mult(r2,r3) in 709 r4`; 710 711val (both_zero_def,_,both_zero_arm) = test_compile' SimpleProcedure ` 712 both_zero (r1:word32,r2:word32) = 713 if r1 = 0w then 714 if r2 = 0w then 715 let r0 = 1w:word32 in (r0,r1,r2) 716 else 717 let r0 = 0w in (r0,r1,r2) 718 else 719 let r0 = 0w in (r0,r1,r2)`; 720 721val (both_eq_def,_,both_eq_arm) = test_compile ` 722 both_eq (r1:word32,r2:word32,r3:word32,r4:word32) = 723 if r1 = r3 then 724 if r2 = r4 then 725 let r0 = 1w:word32 in (r0,r1,r2,r3,r4) 726 else 727 let r0 = 0w in (r0,r1,r2,r3,r4) 728 else 729 let r0 = 0w in (r0,r1,r2,r3,r4)`; 730 731val (curve_neg_def,_,curve_neg_arm) = test_compile' (PushProcedure ([],0)) ` 732 curve_neg (r1:word32,r2:word32) = 733 let (r0,r1,r2) = both_zero(r1,r2) in 734 if r0 = 0w then 735 (r1,r2) 736 else 737 let r8 = r1 in 738 let r9 = r2 in 739 let r2 = 0w in 740 let r3 = r8 in 741 let r4 = field_mult(r2,r3) in 742 let r1 = r9 in 743 let r1 = field_neg r1 in 744 let r0 = r1 in 745 let r1 = r4 in 746 let r0 = field_sub(r0,r1) in 747 let r1 = 1w in 748 let r0 = field_sub(r0,r1) in 749 let r2 = r0 in 750 let r1 = r8 in 751 (r1,r2)`; 752 753val (curve_double_def,_,curve_double_arm) = test_compile' (PushProcedure (["r5","r6","r7","r8","r9"],3)) ` 754 curve_double (r1,r2) = 755 let (r0,r1,r2) = both_zero(r1,r2) in 756 if r0 = 0w then (r1,r2) else 757 let m1 = r1 in (* x1 *) 758 let m2 = r2 in (* y1 *) 759 let r2 = 2w in 760 let r3 = r2 in 761 let r4 = field_mult(r2,r3) in 762 let r5 = r4 in 763 let r2 = 0w in 764 let r3 = m1 in 765 let r4 = field_mult(r2,r3) in 766 let r0 = r5 in 767 let r1 = r4 in 768 let r0 = field_add(r0,r1) in 769 let r1 = 1w in 770 let r0 = field_add(r0,r1) in 771 if r0 = 0w then 772 let r1 = 1w in 773 let r2 = 0w in 774 (r1,r2) 775 else 776 let r11 = r0 in (* d *) 777 let r5 = m1 in 778 let r6 = 2w in 779 let r7 = field_exp(r5,r6) in 780 let r2 = 3w in 781 let r3 = r7 in 782 let r4 = field_mult(r2,r3) in 783 let r8 = r4 in 784 let r2 = 2w in 785 let r3 = 0w in 786 let r4 = field_mult(r2,r3) in 787 let r3 = m1 in 788 let r2 = r4 in 789 let r4 = field_mult(r2,r3) in 790 let r0 = r8 in 791 let r1 = r4 in 792 let r0 = field_add(r0,r1) in 793 let r10 = load_751 in 794 let r1 = r10 - 1w in 795 let r0 = field_add(r0,r1) in 796 let r9 = r0 in 797 let r3 = m2 in 798 let r2 = 0w in 799 let r4 = field_mult(r2,r3) in 800 let r0 = r9 in 801 let r1 = r4 in 802 let r0 = field_sub(r0,r1) in 803 let r8 = r0 in 804 let r9 = r11 in 805 let r4 = field_div(r8,r9) in 806 let r12 = r4 in (* l *) 807 let r5 = m1 in 808 let r6 = 3w in 809 let r7 = field_exp(r5,r6) in 810 let r1 = r7 in 811 let r1 = field_neg r1 in 812 let r7 = r1 in 813 let r10 = load_751 in 814 let r3 = m1 in 815 let r2 = r10 - 1w in 816 let r4 = field_mult(r2,r3) in 817 let r0 = r7 in 818 let r1 = r4 in 819 let r0 = field_add(r0,r1) in 820 let r7 = r0 in 821 let r2 = 2w in 822 let r3 = 0w in 823 let r4 = field_mult(r2,r3) in 824 let r0 = r7 in 825 let r1 = r4 in 826 let r0 = field_add(r0,r1) in 827 let r9 = r0 in 828 let r3 = m2 in 829 let r2 = 1w in 830 let r4 = field_mult(r2,r3) in 831 let r0 = r9 in 832 let r1 = r4 in 833 let r0 = field_sub(r0,r1) in 834 let r8 = r0 in 835 let r9 = r11 in 836 let r4 = field_div(r8,r9) in 837 let r11 = r4 in (* m *) 838 let r5 = r12 in 839 let r6 = 2w in 840 let r7 = field_exp(r5,r6) in 841 let r2 = 0w in 842 let r3 = r12 in 843 let r4 = field_mult(r2,r3) in 844 let r0 = r7 in 845 let r1 = r4 in 846 let r0 = field_add(r0,r1) in 847 let r1 = 0w in 848 let r0 = field_sub(r0,r1) in 849 let r7 = r0 in 850 let r3 = m1 in 851 let r2 = 2w in 852 let r4 = field_mult(r2,r3) in 853 let r0 = r7 in 854 let r1 = r4 in 855 let r0 = field_sub(r0,r1) in 856 let r9 = r0 in (* x *) 857 let r0 = r12 in 858 let r1 = 0w in 859 let r0 = field_add(r0,r1) in 860 let r1 = r0 in 861 let r1 = field_neg r1 in 862 let r2 = r1 in 863 let r3 = r9 in 864 let r4 = field_mult(r2,r3) in 865 let r0 = r4 in 866 let r1 = r11 in 867 let r0 = field_sub(r0,r1) in 868 let r1 = 1w in 869 let r0 = field_sub(r0,r1) in 870 let r2 = r0 in (* y *) 871 let r1 = r9 in (* x *) 872 (r1,r2)`; 873 874val (curve_add_def,_,curve_add_arm) = test_compile' (PushProcedure (["r5","r6","r7","r8","r9"],5)) ` 875 curve_add (r1,r2,r3,r4) = 876 let (r0,r1,r2,r3,r4) = both_eq(r1,r2,r3,r4) in 877 if r0 = 0w then 878 let (r1,r2) = curve_double (r1,r2) in 879 (r1,r2) 880 else 881 let (r0,r1,r2) = both_zero(r1,r2) in 882 if r0 = 0w then 883 let r1 = r3 in 884 let r2 = r4 in 885 (r1,r2) 886 else 887 let m1 = r1 in (* x1 *) 888 let m2 = r2 in (* y1 *) 889 let m3 = r3 in (* x2 *) 890 let m4 = r4 in (* y2 *) 891 let r1 = r3 in 892 let r2 = r4 in 893 let (r0,r1,r2) = both_zero(r1,r2) in 894 if r0 = 0w then 895 let r1 = m1 in 896 let r2 = m2 in 897 (r1,r2) 898 else 899 let r0 = m1 in 900 if r0 = r1 then 901 let r1 = 0w in 902 let r2 = 0w in 903 (r1,r2) 904 else 905 let r0 = m3 in 906 let r1 = m1 in 907 let r0 = field_sub(r0,r1) in 908 let r11 = r0 in (* d *) 909 let r0 = m4 in 910 let r1 = m2 in 911 let r0 = field_sub(r0,r1) in 912 let r8 = r0 in 913 let r9 = r11 in 914 let r4 = field_div(r8,r9) in 915 let r12 = r4 in (* l *) 916 let r2 = m2 in 917 let r3 = m3 in 918 let r4 = field_mult(r2,r3) in 919 let r9 = r4 in 920 let r2 = m4 in 921 let r3 = m1 in 922 let r4 = field_mult(r2,r3) in 923 let r0 = r9 in 924 let r1 = r4 in 925 let r0 = field_sub(r0,r1) in 926 let r8 = r0 in 927 let r9 = r11 in 928 let r4 = field_div(r8,r9) in 929 let r11 = r4 in (* m *) 930 let r2 = 0w in 931 let r3 = r12 in 932 let r4 = field_mult(r2,r3) in 933 let r9 = r4 in 934 let r5 = r12 in 935 let r6 = 2w in 936 let r7 = field_exp(r5,r6) in 937 let r0 = r7 in 938 let r1 = r9 in 939 let r0 = field_add(r0,r1) in 940 let r1 = 0w in 941 let r0 = field_sub(r0,r1) in 942 let r1 = m1 in 943 let r0 = field_sub(r0,r1) in 944 let r1 = m3 in 945 let r0 = field_sub(r0,r1) in 946 let r9 = r0 in (* x *) 947 let r0 = r12 in 948 let r1 = 0w in 949 let r0 = field_add(r0,r1) in 950 let r1 = r0 in 951 let r1 = field_neg r1 in 952 let r2 = r1 in 953 let r3 = r9 in 954 let r4 = field_mult(r2,r3) in 955 let r0 = r4 in 956 let r1 = r11 in 957 let r0 = field_sub(r0,r1) in 958 let r1 = 1w in 959 let r0 = field_sub(r0,r1) in (* y *) 960 let r1 = r9 in 961 let r2 = r0 in 962 (r1,r2)`; 963 964val (curve_mult_aux_def,curve_mult_aux_ind,curve_mult_aux_arm) = test_compile ` 965 curve_mult_aux (r5:word32,r6:word32,r7:word32,r8:word32,r9:word32) = 966 if r7 = 0w then (r8,r9) else 967 if r7 && 1w = 0w then 968 let r7 = r7 >>> 1 in 969 let r1 = r5 in 970 let r2 = r6 in 971 let (r1,r2) = curve_double (r1,r2) in 972 let r5 = r1 in 973 let r6 = r2 in 974 curve_mult_aux (r5,r6,r7,r8,r9) 975 else 976 let r7 = r7 >>> 1 in 977 let r1 = r5 in 978 let r2 = r6 in 979 let r3 = r8 in 980 let r4 = r9 in 981 let (r1,r2) = curve_add (r1,r2,r3,r4) in 982 let r8 = r1 in 983 let r9 = r2 in 984 let r1 = r5 in 985 let r2 = r6 in 986 let (r1,r2) = curve_double (r1,r2) in 987 let r5 = r1 in 988 let r6 = r2 in 989 curve_mult_aux (r5,r6,r7,r8,r9)`; 990 991val (curve_mult_def,_,curve_mult_arm) = test_compile' (PushProcedure ([],0)) ` 992 curve_mult (r5:word32,r6:word32,r7:word32) = 993 let r8 = 0w in 994 let r9 = 0w in 995 let (r8,r9) = curve_mult_aux (r5,r6,r7,r8,r9) in 996 (r8,r9)` 997 998(* 999 1000Use arm_flatten_code() to prove and print a concrete version of 1001the procedure call graph: 1002 1003val _ = arm_flatten_code (); 1004 1005It returns the correctness theorem of the last verified procedure with 1006the code flattened to one sequence with concrete procedure calls. 1007 1008Warning: this function is at present rather slow. 1009 1010*) 1011 1012val _ = export_theory(); 1013 1014