Merge pull request #56 from secure-foundations/remove-nops

Remove nops

arch/otbn/decls.i.vad

@@ -407,6 +407,14 @@ procedure li(inout dst: reg32, inline imm: uint32)
     this := this.(heap := old(this).heap);
 }
 
+procedure nop()
+    {:instruction Ins32(NOP)}
+{
+    reveal eval_code_opaque;
+    reveal valid_state_opaque;
+    this := this.(heap := old(this).heap);
+}
+
 procedure bn_add(inout dst: reg256, in src1: reg256, in src2: reg256, inline shift: shift_t, inline which_group: uint1)
     {:instruction Ins256(BN_ADD(dst, src1, src2, shift, which_group))}
     modifies
@@ -732,7 +740,7 @@ procedure comment(inline comment: string)
     reveal valid_state_opaque;
     this := this.(heap := old(this).heap);
 }
-
+    
 #verbatim
 } // end module vt_decls
 #endverbatim

arch/otbn/machine.s.dfy

@@ -3,6 +3,7 @@ include "../../lib/bv256_ops.dfy"
 
 module ot_machine {
     import Mul
+    import Seq
 
     import bv32_ops
     import bv256_ops
@@ -96,6 +97,7 @@ module ot_machine {
         | LI(xrd: reg32_t, imm32: uint32)
         | CSRRS(grd: reg32_t, csr: uint12, grs1: reg32_t)
         | ECALL
+        | NOP
 
     datatype ins256 =
         | BN_ADD(wrd: reg256_t, wrs1: reg256_t, wrs2: reg256_t, shift: shift_t, fg: uint1)
@@ -382,6 +384,56 @@ module ot_machine {
         | CNil
         | va_CCons(hd: code, tl: codes)
 
+/* control flow overlap detection */
+datatype simple_code =
+  | SIns
+  | SJump
+  | SWhile(s:seq<simple_code>)
+  | SBranch(s:seq<simple_code>)
+
+function method simplify_codes(c:codes) : seq<simple_code>
+{
+  match c 
+    case CNil => []
+    case va_CCons(hd, tl) => simplify_code(hd) + simplify_codes(tl)
+}
+
+// Intended to be called on the body of each top-level function.
+function method simplify_code(c:code) : seq<simple_code>
+{
+  match c
+    case Ins32(_) => [SIns]
+    case Ins256(_) => [SIns]
+    case Block(b) => simplify_codes(b)
+    case While(_, body) => [SWhile(simplify_code(body))]
+    case IfElse(_, tbody, fbody) => [SBranch(simplify_code(tbody))]
+    case Function(_, body) => [SJump]
+    case Comment(_) => []
+}
+
+predicate method has_overlap(c:simple_code) 
+{
+  match c
+    case SIns => false
+    case SJump => false
+    case SBranch(s) => false
+    case SWhile(s) =>
+      if |s| == 0 then false
+      else if (Seq.Last(s).SWhile? || Seq.Last(s).SBranch? || Seq.Last(s).SJump?) then true
+      else has_overlap_seq(s)
+}
+
+predicate method has_overlap_seq(s:seq<simple_code>)
+{
+  if |s| == 0 then false
+  else has_overlap(s[0]) || has_overlap_seq(s[1..])
+}
+
+predicate method while_overlap(c:code) 
+{
+  has_overlap_seq(simplify_code(c))
+}
+
 /* state definitions */
 
     datatype state = state(
@@ -714,6 +766,7 @@ module ot_machine {
                 case CSRRS(grd, csr, grs1) => eval_CSRRS(grd, csr, grs1)
                 case LI(xrd, imm32) => eval_LI(xrd, imm32)
                 case ECALL => this
+                case NOP => this
         }
 
         function method eval_ins256(wins: ins256): state

arch/otbn/modexp_printer.s.dfy

@@ -0,0 +1,22 @@
+include "vale.i.dfy"
+include "printer.s.dfy"
+include "../../gen/impl/otbn/modexp_var.i.dfy"
+
+module modexp_printer {
+
+import opened ot_machine
+import opened modexp_var
+import opened otbn_printer
+
+method Main()
+{
+    var p := new Printer({"modexp_var_3072_f4", "montmul"});
+    var comment := "/*\n  This code is generated by the veri-titan project: https://github.com/secure-foundations/veri-titan\n*/\n";
+    print(comment);
+
+    reveal va_code_modexp_var_3072_f4();
+    var c := va_code_modexp_var_3072_f4();
+    p.printTopLevelProc(c);
+}
+
+}

arch/otbn/printer.s.dfy

@@ -1,16 +1,13 @@
 include "vale.i.dfy"
-include "../../gen/impl/otbn/modexp_var.i.dfy"
 
 module otbn_printer {
     import opened integers
     import opened ot_machine
-    import opened modexp_var
 
 method printReg32(r:reg32_t)
 {
     match r
         case GPR(x) => print("x"); print(x);
-        // case RND => print("ERROR: rnd"); // TODO: Are we no longer modeling RND?
 }
 
 method printReg256(r:reg256_t)
@@ -96,6 +93,11 @@ method printIns32(ins:ins32)
 
         case ECALL => 
             print ("ecall ");
+
+        case BN_NOP =>
+            print("nop\n");
+
+
 }
 
 method printShift(shift:shift_t)
@@ -265,7 +267,7 @@ function method codeSize(c: code) : int
 {
     match c
         case Block(block) => blockSize(block)
-        case While(wcond, wbody) => codeSize(wbody) + 2 // +1 for inner loop and +1 for inner loop's nop
+        case While(wcond, wbody) => codeSize(wbody) + 1 // +1 for inner loop
         case IfElse(icond, tbody, fbody) => codeSize(tbody) + codeSize(fbody) + 1
         case Function(_, _) => 1
         case Ins32(ins) => 1
@@ -379,10 +381,9 @@ class Printer {
             case While(wcond, wbody) =>
             {
                 printIndent(); printWhileCond(wcond); print(", ");
-                print(codeSize(wbody) + 1); print("\n"); // + 1 for nop instruction
+                print(codeSize(wbody)); print("\n");
                 depth := depth + 1;
                 printCode(wbody);
-                printIndent(); print("nop\n"); // ensures different end addrs for nested loops
                 depth := depth - 1;
             }
             case Comment(com) => print(com);
@@ -403,23 +404,16 @@ class Printer {
                     print(".globl "); print(func_name); print("\n");
                 }
                 print(func_name); print(":\n");
+                var overlaps := has_overlap_seq(simplify_codes(res[i].1));
+                if overlaps {
+                  print("LOOP_ERROR detected:\n");
+                  print(simplify_codes(res[i].1));
+                }
                 printCode(Block(res[i].1));
                 printIndent(); print("ret\n\n");
             }
             i := i + 1;
         }
     }
 }
-
-method Main()
-{
-    var comment := "/*\n  This code is generated by the veri-titan project: https://github.com/secure-foundations/veri-titan\n*/\n";
-    print(comment);
-
-    var p := new Printer({"modexp_var_3072_f4", "montmul"});
-
-    reveal va_code_modexp_var_3072_f4();
-    p.printTopLevelProc(va_code_modexp_var_3072_f4());
-}
-
 }

arch/otbn/test_framework.s.dfy

@@ -0,0 +1,88 @@
+include "printer.s.dfy"
+include "../../gen/impl/otbn/nop_tests.i.dfy"
+
+/* 
+ A module for testing that OTBN code correctly includes NOP
+ instructions to avoid LOOP_ERRORs, as described in:
+ https://docs.opentitan.org/hw/ip/otbn/doc/#loop-nesting   
+*/
+module test_framework {
+    import opened integers
+    import opened ot_machine
+    import opened otbn_printer
+
+    import opened nop_tests
+
+method TestOverlap(p:Printer, name:string, c:code, overlap_expected:bool) 
+  modifies p
+{
+  match c
+    case Function(_, body) => {
+
+    var overlaps := has_overlap_seq(simplify_codes(body));
+    print("\nTesting loop overlap detection in " + name);
+
+    if overlaps != overlap_expected {
+      if overlap_expected {
+        print("\n  ERROR: Expected to find an overlap but didn't\n");
+      } else {
+        print("\n  ERROR: Did not expect overlap but I think I found one\n");
+      }
+
+      print("  Simplified code: "); print(simplify_codes(body)); print("\n");
+
+    } else {
+      print("\n  PASSED!\n");
+    }
+  }
+    case _ =>
+    {
+    print("ERROR: Expected a top-level function, found:\n" + name);
+    print("\n");
+  }
+}
+
+method Main()
+{
+    var p := new Printer({});
+
+    var c;
+    c := va_code_loop_overlap_nop();
+    TestOverlap(p, "loop_overlap_nop", c, false);
+    c := va_code_loop_overlap();
+    TestOverlap(p, "loop_overlap", c, true);
+    c := va_code_loop_no_overlap();
+    TestOverlap(p, "loop_no_overlap", c, false);
+    c := va_code_loop_overlap_inner_with_starting_ins();
+    TestOverlap(p, "loop_overlap_inner_with_starting_ins", c, true);
+    c := va_code_loop_overlap_inner_with_ending_ins();
+    TestOverlap(p, "loop_overlap_inner_with_ending_ins", c, false);
+    c := va_code_loop_if_overlap();
+    TestOverlap(p, "loop_if_overlap", c, true);
+    c := va_code_loop_if_with_starting_ins_overlap();
+    TestOverlap(p, "loop_if_with_starting_ins_overlap", c, true);
+    c := va_code_loop_if_with_ending_ins_no_overlap();
+    TestOverlap(p, "loop_if_with_ending_ins_no_overlap", c, false);
+    c := va_code_if_loop_no_overlap();
+    TestOverlap(p, "if_loop_no_overlap", c, false);
+    c := va_code_loop_loop_empty_overlap();
+    TestOverlap(p, "if_loop_loop_empty_overlap", c, true);
+    c := va_code_loop_if_empty_overlap();
+    TestOverlap(p, "if_loop_if_empty_overlap", c, true);
+    c := va_code_loop_function_overlap();
+    TestOverlap(p, "if_loop_function_overlap", c, true);
+
+    /* Examples provided in the OTBN documentation: */
+    c := va_code_otbn_ok_example_1();
+    TestOverlap(p, "otbn_ok_example_1", c, false);
+    c := va_code_otbn_ok_example_2();
+    TestOverlap(p, "otbn_ok_example_2", c, false);
+    c := va_code_otbn_ok_example_3();
+    TestOverlap(p, "otbn_ok_example_3", c, false);
+    c := va_code_otbn_nok_example_1();
+    TestOverlap(p, "otbn_nok_example_1", c, true);
+    c := va_code_otbn_nok_example_2();
+    TestOverlap(p, "otbn_nok_example_2", c, true);
+}
+
+}

build.py

@@ -50,7 +50,7 @@ def rules():
 OUTPUT_ELF_PATH = "gen/run_modexp.elf"
 
 DLL_SOURCES = {
-    "arch/otbn/printer.s.dfy": OTBN_ASM_PATH,
+     "arch/otbn/modexp_printer.s.dfy": OTBN_ASM_PATH,
     "arch/otbn/simulator.i.dfy": "gen/arch/otbn/sim.out", 
     "arch/riscv/printer.s.dfy": RISCV_ASM_PATH,
 }
@@ -59,7 +59,6 @@ def rules():
 CODE_DIRS = ["arch", "impl", "lib"]
 GEN_DIR = "gen"
 
-
 NL_FILES = {
     "lib/sub_mod_nl_lemmas.i.dfy",
     "lib/mul256_nl_lemma.i.dfy"}

impl/otbn/examples.i.vad

@@ -110,7 +110,6 @@ procedure loop_reg(inout dst:reg32, in cnt:reg32)
 //     bn_sel(w22, w30, w22, 0, 3);
 // }
 
-
 // procedure copy()
 //     requires
 //         xmem_addr_valid(xmem, x0 + 0);

impl/otbn/modexp_var.i.vad

@@ -390,6 +390,7 @@ procedure modexp_var_3072_f4(
         modexp_var_inv_peri_lemma(prev_a_view, a_view, i, vars.rsa);
 
         i := i + 1;
+        nop();
     }
 
     addi(x19, x23, 0);