x86: remove support for explicit if-then-else in flag combinations

jasmin-lang · Oct 18, 2022 · 3aa0d35 · 3aa0d35
1 parent d321042
commit 3aa0d35
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 56 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -6,6 +6,13 @@
 - Support ARMv7 (Cortex-M4) as target architecture
   ([PR #242](https://github.com/jasmin-lang/jasmin/pull/242)).
 
+## Other changes
+
+- Explicit if-then-else in flag combinations is no longer supported
+  in x86 assembly generation; conditions that used to be supported
+  can be expressed using equality and disequality tests
+  ([PR #270](https://github.com/jasmin-lang/jasmin/pull/270)).
+
 # Jasmin 2022.09.0
 
 ## Bug fixes

diff --git a/proofs/compiler/x86_params.v b/proofs/compiler/x86_params.v
@@ -192,25 +192,6 @@ Fixpoint assemble_cond_r ii (e : pexpr) : cexec condt :=
       then ok NL_ct
       else Error (E.berror ii e "Invalid condition (NL)")
 
-  (* FIXME: We keep this by compatibility but it will be nice to remove it. *)
-  | Pif _ (Pvar v1) (Papp1 Onot (Pvar vn2)) (Pvar v2) =>
-      Let r1 := of_var_e_bool ii (gv v1) in
-      Let rn2 := of_var_e_bool ii (gv vn2) in
-      Let r2 := of_var_e_bool ii (gv v2) in
-      if [&& r1 == SF, rn2 == OF & r2 == OF]
-         || [&& r1 == OF, rn2 == SF & r2 == SF]
-      then ok L_ct
-      else Error (E.berror ii e "Invalid condition (L)")
-
-  | Pif _ (Pvar v1) (Pvar v2) (Papp1 Onot (Pvar vn2)) =>
-      Let r1 := of_var_e_bool ii (gv v1) in
-      Let r2 := of_var_e_bool ii (gv v2) in
-      Let rn2 := of_var_e_bool ii (gv vn2) in
-      if [&& r1 == SF, rn2 == OF & r2 == OF]
-         || [&& r1 == OF, rn2 == SF & r2 == SF]
-      then ok NL_ct
-      else Error (E.berror ii e "Invalid condition (NL)")
-
   | _ => Error (E.berror ii e "don't known how to compile the condition")
 
   end.

diff --git a/proofs/compiler/x86_params_proof.v b/proofs/compiler/x86_params_proof.v
@@ -334,46 +334,26 @@ Proof.
     move=> -/not_condtP /=.
     move=> ->.
     by exists (~~b).
-  + case => //=.
-    + move=> e1 _ e2 _ c v.
-      case: e1 => //= x1; case: e2 => //= x2; t_xrbindP => f1 /of_var_e_boolP ok_f1 f2 /of_var_e_boolP ok_f2.
-      case: ifP => // /orP hor [<-] v1 /(gxgetflag eqv ok_f1) hv1 v2 /(gxgetflag eqv ok_f2) hv2.
-      move=> /sem_sop2I /= [b1 [b2 [b3 [hb1 hb2 [<-] ->]]]].
-      move: (hv1 _ hb1) (hv2 _ hb2) => hfb1 hfb2.
-      exists (b1 == b2); last done.
-      by case: hor => /andP [] /eqP ? /eqP ?; subst f1 f2; rewrite hfb1 hfb2 //= eq_sym.
-    + move=> e1 hrec1 e2 hrec2 c v; t_xrbindP => c1 hc1 c2 hc2 hand v1 hv1 v2 hv2.
-      move=> /sem_sop2I /= [b1 [b2 [b3 [hb1 hb2 [<-] ->]]]].
-      have /(value_of_bool_uincl hb1) hec1 := hrec1 _ _ hc1 hv1.
-      have /(value_of_bool_uincl hb2) hec2 := hrec2 _ _ hc2 hv2.
-      have /= -> := and_condtP hand hec1 hec2.
-      by exists (b1 && b2).
-    move=> e1 hrec1 e2 hrec2 c v; t_xrbindP => c1 hc1 c2 hc2 hor v1 hv1 v2 hv2.
+  case => //=.
+  + move=> e1 _ e2 _ c v.
+    case: e1 => //= x1; case: e2 => //= x2; t_xrbindP => f1 /of_var_e_boolP ok_f1 f2 /of_var_e_boolP ok_f2.
+    case: ifP => // /orP hor [<-] v1 /(gxgetflag eqv ok_f1) hv1 v2 /(gxgetflag eqv ok_f2) hv2.
+    move=> /sem_sop2I /= [b1 [b2 [b3 [hb1 hb2 [<-] ->]]]].
+    move: (hv1 _ hb1) (hv2 _ hb2) => hfb1 hfb2.
+    exists (b1 == b2); last done.
+    by case: hor => /andP [] /eqP ? /eqP ?; subst f1 f2; rewrite hfb1 hfb2 //= eq_sym.
+  + move=> e1 hrec1 e2 hrec2 c v; t_xrbindP => c1 hc1 c2 hc2 hand v1 hv1 v2 hv2.
     move=> /sem_sop2I /= [b1 [b2 [b3 [hb1 hb2 [<-] ->]]]].
     have /(value_of_bool_uincl hb1) hec1 := hrec1 _ _ hc1 hv1.
     have /(value_of_bool_uincl hb2) hec2 := hrec2 _ _ hc2 hv2.
-    have /= -> := or_condtP hor hec1 hec2.
-    by exists (b1 || b2).
-  move=> t e _ e1 _ e2 _ c v /=.
-  case: e => //= v1; case: e1 => //= [v2 | [] //= e2'].
-  + case: e2 => //= -[] // [] //= vn2; t_xrbindP => f1 /of_var_e_boolP hf1 f2 /of_var_e_boolP hf2 fn2 /of_var_e_boolP hfn2.
-    case: ifP => // /orP hor [<-] b1 vv1 /(gxgetflag eqv hf1) hvb1/hvb1{hvb1}hvb1.
-    move=> vv2 vv2' /(gxgetflag eqv hf2) hvb2 ht2.
-    move=> ?? vvn2 /(gxgetflag eqv hfn2) hvnb2 /sem_sop1I /= [nb2 /hvnb2{hvnb2}hvnb2 ->].
-    move=> /truncate_valE [??] ?; subst.
-    move: ht2; rewrite /truncate_val /=; t_xrbindP => b2 /hvb2{hvb2}hvb2 ?; subst.
-    exists (if b1 then Vbool b2 else ~~ nb2); last done.
-    by case: hor => /and3P [/eqP ? /eqP ? /eqP ?]; subst; move: hvnb2; rewrite hvb1 hvb2 => -[<-] /=;
-      case: (b1); case: (b2).
-  case: e2' => //= v2; case: e2 => // vn2; t_xrbindP => f1 /of_var_e_boolP hf1 f2 /of_var_e_boolP hf2 fn2 /of_var_e_boolP hfn2.
-  case: ifP => // /orP hor [<-] b1 vv1 /(gxgetflag eqv hf1) hvb1/hvb1{hvb1}hvb1.
-  move=> ? vv2 vv2' /(gxgetflag eqv hf2) hvb2 /sem_sop1I /= [b2 /hvb2{hvb2}hvb2 ->].
-  move=> /truncate_valE [??] ?; subst.
-  move=> vvn2 /(gxgetflag eqv hfn2) hvnb2.
-  rewrite /truncate_val /=; t_xrbindP => nb2 /hvnb2{hvnb2}hvnb2 ??; subst.
-  exists (if b1 then Vbool (~~b2) else nb2); last done.
-  by case: hor => /and3P [/eqP ? /eqP ? /eqP ?]; subst; move: hvnb2; rewrite hvb1 hvb2 => -[<-] /=;
-      case: (b1); case: (b2).
+    have /= -> := and_condtP hand hec1 hec2.
+    by exists (b1 && b2).
+  move=> e1 hrec1 e2 hrec2 c v; t_xrbindP => c1 hc1 c2 hc2 hor v1 hv1 v2 hv2.
+  move=> /sem_sop2I /= [b1 [b2 [b3 [hb1 hb2 [<-] ->]]]].
+  have /(value_of_bool_uincl hb1) hec1 := hrec1 _ _ hc1 hv1.
+  have /(value_of_bool_uincl hb2) hec2 := hrec2 _ _ hc2 hv2.
+  have /= -> := or_condtP hor hec1 hec2.
+  by exists (b1 || b2).
 Qed.
 
 Lemma assemble_extra_op rip ii op lvs args op' lvs' args' op'' asm_args m m' s :