Arm/lowering: use RSB for x = (y << n) - z; (#585)

(cherry picked from commit 0a2f1d5)

CHANGELOG.md

@@ -1,6 +1,12 @@
 
 # [unreleased]
 
+## New features
+
+- Instruction selection for arm-m4 turns `x = (y << n) - z`
+  into `x = #RSB(z, y << n)`
+  ([PR #585](https://github.com/jasmin-lang/jasmin/pull/585)).
+
 ## Bug fixes
 
 - Fix printing to EasyCrypt of ARMv7 instruction `bic`

compiler/tests/success/arm-m4/sub.jazz

@@ -49,6 +49,16 @@ fn sub(reg u32 arg0, reg u32 arg1) -> reg u32 {
     x -= arg0 >>r 31;
     [x] = x;
 
+    // RSB
+    x = (arg0 << 0) - arg1;
+    [x] = x;
+    x = (arg0 >>r 1) - arg1;
+    [x] = x;
+    x = (arg0 >>s 2) - arg1;
+    [x] = x;
+    x = (arg0 >> 3) - arg1;
+    [x] = x;
+
     // Conditionals.
     nf, zf, cf, vf, _ = #SUBS(x, 0);
 

compiler/tests/success/arm-m4/sub_using_RSB.jazz

@@ -0,0 +1,7 @@
+u32 MINUS_Q = -8380417;
+
+export fn __montgomery_reduce_8380417(reg u32 a) -> reg u32
+{
+  a = (a << 3) - a;
+  return a;
+}

proofs/compiler/arm_lowering.v

@@ -150,6 +150,9 @@ Definition get_arg_shift
   else
     None.
 
+Definition is_shift (ws : wsize) (e : pexpr) :=
+  if get_arg_shift ws [::e] is None then true else false.
+
 Definition arg_shift
   (mn : arm_mnemonic) (ws : wsize) (e : pexprs) : arm_op * seq pexpr :=
   let '(osh, es) :=
@@ -280,6 +283,9 @@ Definition lower_Papp2_op
         if is_mul e1 is Some (x, y)
         then Some (MLS, x, [:: y; e0 ])
         else
+        if is_shift ws e1 && ~~ (is_shift ws e0) then
+          Some (RSB, e1, [:: e0])
+        else
         Some (SUB, e0, [:: e1 ])
     | Odiv (Cmp_w Signed U32) =>
         Some (SDIV, e0, [:: e1 ])

proofs/compiler/arm_lowering_proof.v

@@ -843,7 +843,7 @@ Proof.
           match goal with
           | [ |- context[ is_mul ] ] => case: is_mulP => [???|]; subst
           end.
-
+      6: case: ifP => _.
       all: move=> [? ? ?] hsemop; subst mn e0' e1'.
       all: discriminate hhas_shift || clear hhas_shift.
 
@@ -858,10 +858,24 @@ Proof.
       all: have {hws0} hws0 := cmp_le_trans hws hws0.
       all: have {hws1} hws1 := cmp_le_trans hws hws1.
 
+      2:{
+        have [ws2 [wbase [wsham [hws2 hbase hsham hw1 [hfvbase hfvsham]]]]] :=
+          get_arg_shiftP hget_arg_shift hfve0 hseme0.
+        have hfves := disj_fvars_read_es3 hfve1 hfvbase hfvsham.
+        split; last done.
+        clear hfve1 hfvbase hfvsham hfves.
+        case/truncate_wordP: hw1 => _ hw1.
+        rewrite /= hseme1 hbase hsham {hseme1 hbase hsham} /=.
+        eexists; first reflexivity.
+        rewrite /exec_sopn /= /sopn_sem /= !truncate_word_le // {hws1 hws2} /=.
+        rewrite (wsub_zero_extend _ _ hws) wsub_wnot1.
+        rewrite !(zero_extend_idem _ hws).
+        by rewrite zero_extend_u hw1.
+      }
       all:
         have [ws2 [wbase [wsham [hws2 hbase hsham hw1 [hfvbase hfvsham]]]]] :=
           get_arg_shiftP hget_arg_shift hfve1 hseme1.
-      all: clear hfve1 hseme1 hget_arg_shift.
+
       all: have hfves := disj_fvars_read_es3 hfve0 hfvbase hfvsham.
       all: split; last done.
       all: clear hfve0 hfvbase hfvsham hfves.
@@ -927,6 +941,11 @@ Proof.
       match goal with
       | [ |- context[ is_mul ] ] => case: is_mulP => [???|]; subst
       end.
+  all:
+    repeat 
+      match goal with 
+      | [ |- context[ if _ then _ else _] ] => case: ifP => _
+      end.
 
   all: move=> [? ? ?] hsemop; subst mn e0' e1'.
   all: discriminate hhas_shift || clear hhas_shift.
@@ -949,16 +968,19 @@ Proof.
   all: move=> /= ?; subst w.
 
   all: have hfves := disj_fvars_read_es2 hfve0 hfve1.
-  6: have hfves' := disj_fvars_read_es2_app2 hfve1 hfve0.
-  7, 9: have hfves' := disj_fvars_read_es2_app2 hfve0 hfve1.
+  2: have hfves' := disj_fvars_read_es2 hfve1 hfve0.
+  7: have hfves' := disj_fvars_read_es2_app2 hfve1 hfve0.
+  8, 10: have hfves' := disj_fvars_read_es2_app2 hfve0 hfve1.
   all: split; last done.
+
   all: clear hfve0 hfve1 hfves.
 
   all: rewrite /=.
-  6: move: hseme0 => /=; t_xrbindP => ? -> ? -> /= hseme0.
-  7, 8: move: hseme1 => /=; t_xrbindP => ? -> ? -> /= hseme1.
+  7: move: hseme0 => /=; t_xrbindP => ? -> ? -> /= hseme0.
+  8, 9: move: hseme1 => /=; t_xrbindP => ? -> ? -> /= hseme1.
   all: try rewrite hseme0 {hseme0} /=.
   all: try rewrite hseme1 {hseme1} /=.
+
   all: eexists; first reflexivity.
 
   all: rewrite /exec_sopn /=.
@@ -980,12 +1002,12 @@ Proof.
   all: rewrite /=.
 
   1: rewrite (wadd_zero_extend _ _ hws).
-  2: rewrite (wsub_zero_extend _ _ hws) wsub_wnot1.
-  3: rewrite -(wand_zero_extend _ _ hws).
-  4: rewrite -(wor_zero_extend _ _ hws).
-  5: rewrite -(wxor_zero_extend _ _ hws).
-  9: rewrite (wmul_zero_extend _ _ hws).
-  1-5, 9: by rewrite !(zero_extend_idem _ hws).
+  2,3: rewrite (wsub_zero_extend _ _ hws) wsub_wnot1.
+  4: rewrite -(wand_zero_extend _ _ hws).
+  5: rewrite -(wor_zero_extend _ _ hws).
+  6: rewrite -(wxor_zero_extend _ _ hws).
+  10: rewrite (wmul_zero_extend _ _ hws).
+  1-6, 10: by rewrite !(zero_extend_idem _ hws).
 
   1: move: hseme0.
   2, 3: move: hseme1.