Add rip, eip, ip registers

mit-plv · Mar 5, 2025 · fd145f5 · fd145f5
1 parent 94e8fc2
commit fd145f5
Show file tree

Hide file tree

Showing 5 changed files with 48 additions and 33 deletions.
diff --git a/src/Assembly/EquivalenceProofs.v b/src/Assembly/EquivalenceProofs.v
@@ -1847,26 +1847,32 @@ Qed.
 (* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *)
 Lemma get_reg_set_reg_full s rn rn' v
   : get_reg (set_reg s rn v) rn'
-    = if ((rn <? ((fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)) && (rn =? rn'))%N%bool
+    = if ((rn <? ((fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)) && (rn =? rn') && negb (REG_beq (widest_register_of_index rn') rip))%N%bool
       then Some v
       else get_reg s rn'.
 Proof.
   cbv [get_reg set_reg].
-  break_innermost_match; split_andb; reflect_hyps; subst.
+  break_innermost_match; split_andb; reflect_hyps; subst; try reflexivity; try congruence.
   all: rewrite <- !Tuple.nth_default_to_list.
   all: rewrite [email protected]_to_list in *.
   all: unshelve erewrite Tuple.from_list_default_eq, Tuple.to_list_from_list, set_nth_nth_default_full;
     rewrite ?length_set_nth, ?Tuple.length_to_list; try easy.
   all: break_innermost_match; try lia; try reflexivity.
+  all: try (assert (rn = rn') by lia; subst); try congruence.
+  all: repeat match goal with
+      | [ H : ~(?a /\ ?b) |- _ ] => assert (~a) by intuition auto; clear H
+      end.
+  all: try lia.
   now rewrite nth_default_out_of_bounds by now rewrite Tuple.length_to_list; lia.
 Qed.
 
 (* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *)
 Local Lemma get_reg_set_reg_same s rn v
       (H : (rn < (fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)%N)
-  : get_reg (set_reg s rn v) rn = Some v.
+  : get_reg (set_reg s rn v) rn = if REG_beq (widest_register_of_index rn) rip then None else Some v.
 Proof.
-  rewrite get_reg_set_reg_full; break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; lia.
+  rewrite get_reg_set_reg_full; cbv [get_reg is_ip_register_index].
+  break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; try lia.
 Qed.
 
 Lemma compute_array_address_ok {opts : symbolic_options_computed_opt} {descr:description} G s s' base i idx base_val

diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v
@@ -3863,8 +3863,12 @@ Definition reverse_lookup_flag (st : flag_state) (i : idx) : option FLAG
        (List.find (fun v => option_beq N.eqb (Some i) (fst v))
                   (Tuple.to_list _ (Tuple.map2 (@pair _ _) st (CF, PF, AF, ZF, SF, OF)))).
 
+Definition is_ip_register_index (ri : N) : bool :=
+  REG_beq (widest_register_of_index ri) rip.
 Definition get_reg (st : reg_state) (ri : N) : option idx
-  := Tuple.nth_default None (N.to_nat ri) st.
+  := if is_ip_register_index ri
+     then None
+     else Tuple.nth_default None (N.to_nat ri) st.
 Definition set_reg (st : reg_state) (ri : N) (i : idx) : reg_state
   := Tuple.from_list_default None _ (ListUtil.set_nth
        (N.to_nat ri)

diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v
@@ -18,9 +18,9 @@ Local Set Implicit Arguments.
 Local Set Primitive Projections.
 
 Inductive REG :=
-|     rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15
-|     eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d
-|      ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w
+|     rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15  | rip
+|     eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | eip
+|      ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ip
 | ah | al | ch | cl | dh | dl | bh | bl |  spl |  bpl |  sil |  dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b
 .
 
@@ -276,11 +276,11 @@ Definition Lines := list Line.
 
 Definition reg_size (r : REG) : N :=
       match r with
-      |(    rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15 )
+      |(    rax |     rcx |     rdx |     rbx | rsp  | rbp  | rsi  | rdi  | r8  | r9  | r10  | r11  | r12  | r13  | r14  | r15  | rip)
        => 64
-      |(    eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d)
+      |(    eax |     ecx |     edx |     ebx | esp  | ebp  | esi  | edi  | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d | eip)
        => 32
-      |(     ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w)
+      |(     ax |      cx |      dx |      bx |  sp  |  bp  |  si  |  di  | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w | ip)
        => 16
       |(ah | al | ch | cl | dh | dl | bh | bl |  spl |  bpl |  sil |  dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b)
        => 8
@@ -354,6 +354,7 @@ Definition widest_register_of (r : REG) : REG :=
   | (r13b | r13w | r13d | r13) => r13
   | (r14b | r14w | r14d | r14) => r14
   | (r15b | r15w | r15d | r15) => r15
+  | (ip | eip | rip) => rip
   end.
 
 Definition widest_registers := Eval lazy in List.filter (fun x => REG_beq x (widest_register_of x)) (list_all REG).

diff --git a/src/Assembly/WithBedrock/Proofs.v b/src/Assembly/WithBedrock/Proofs.v
@@ -78,7 +78,7 @@ Qed.
 Import Map.Interface Map.Separation. (* for coercions *)
 Require Import bedrock2.Array.
 Require Import bedrock2.ZnWords.
-Require Import Rupicola.Lib.Tactics. (* for sepsimpl *)
+(*Require Import Rupicola.Lib.Tactics. (* for sepsimpl *)*)
 Import LittleEndianList.
 Import coqutil.Word.Interface.
 Definition cell64 wa (v : Z) : Semantics.mem_state -> Prop :=
@@ -268,7 +268,7 @@ Lemma init_symbolic_state_G_ok m G d G' ss
       (Hframe : frame m)
       (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list _ m.(machine_reg_state)))
   : R frame G' ss m
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg ss.(symbolic_reg_state) (reg_index reg)) = true)
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg ss.(symbolic_reg_state) (reg_index reg)) = true)
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
@@ -286,6 +286,7 @@ Proof.
          erewrite length_Forall2, Tuple.length_to_list
            by (eapply dag_gensym_n_G_ok; [ | eta_expand; reflexivity | ]; assumption).
          reflexivity. }
+       break_innermost_match; try congruence; [].
        erewrite map_nth_default with (x:=0%N); [ reflexivity | ].
        erewrite length_Forall2, Tuple.length_to_list
          by (eapply dag_gensym_n_G_ok; [ | eta_expand; reflexivity | ]; assumption).
@@ -317,7 +318,7 @@ Lemma init_symbolic_state_ok m G d
       (Hframe : frame m)
   : exists G',
     R frame G' ss m
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg ss.(symbolic_reg_state) (reg_index reg)) = true)
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg ss.(symbolic_reg_state) (reg_index reg)) = true)
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n).
 Proof.
@@ -353,6 +354,7 @@ Proof.
   cbv [R_reg] in Hreg.
   destruct Hreg as [Hreg Hreg'].
   rewrite <- Hreg'.
+  break_innermost_match_hyps; inversion_option.
   now apply Hreg.
 Qed.
 
@@ -614,7 +616,7 @@ Proof.
                | progress cbv [index_and_shift_and_bitcount_of_reg] in *
                | solve [ eauto ]
                | match goal with
-                 | [ H : (forall reg, Option.is_Some (Symbolic.get_reg ?s (reg_index reg)) = true)
+                 | [ H : (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg ?s (reg_index reg)) = true)
                      |- context[Symbolic.get_reg ?s (reg_index ?ri)] ]
                    => generalize (H ri); cbv [Option.is_Some]; break_innermost_match;
                       try congruence
@@ -1470,7 +1472,7 @@ Lemma build_merge_stack_placeholders_ok_R {opts : symbolic_options_computed_opt}
       (HR : R frame' G s ms)
       (Hrsp : (rsp_val - 8 * Z.of_nat (List.length stack_vals))%Z = word.unsigned base_stack_word_val)
       (Hframe : Lift1Prop.iff1 frame' (frame * array cell64 (word.of_Z 8) base_stack_word_val stack_vals)%sep)
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
       (Hrsp_val : Z.land rsp_val (Z.ones 64) = Z.land (Semantics.get_reg ms rsp) (Z.ones 64))
   : exists G',
     ((exists rsp_idx,
@@ -1485,7 +1487,7 @@ Lemma build_merge_stack_placeholders_ok_R {opts : symbolic_options_computed_opt}
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n)
     /\ R frame G' s' ms
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
 
 Proof.
   eapply build_merge_stack_placeholders_ok in H; [ | try eassumption .. ]; [ | destruct s; apply HR .. ]; [].
@@ -1789,7 +1791,7 @@ Lemma build_merge_base_addresses_ok_R
       (H : build_merge_base_addresses (dereference_scalar:=dereference_scalar) idxs reg_available s = Success (outputaddrs, s'))
       (Hreg_available_wide : Forall (fun reg => let '(rn, lo, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) reg_available)
       (HR : R frame' G s ms)
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
       (Hruntime_reg : get_asm_reg ms reg_available = runtime_reg)
       addr_vals addr_ptr_vals
       (Haddr_ptr_vals : List.map word.unsigned addr_ptr_vals = List.firstn (List.length idxs) runtime_reg)
@@ -1881,7 +1883,7 @@ Lemma build_merge_base_addresses_ok_R
     /\ gensym_dag_ok G' d'
     /\ (forall e n, eval G d e n -> eval G' d' e n)
     /\ R frame G' s' ms
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
 Proof.
   eapply build_merge_base_addresses_ok in H; [ | try eassumption .. ]; [ | destruct s; apply HR .. ]; [].
   destruct H as [G' H]; exists G'.
@@ -1902,7 +1904,7 @@ Proof.
     { Foralls_to_nth_error; intuition idtac. }
     { intros.
       match goal with
-      | [ H : (forall reg, Option.is_Some (Symbolic.get_reg ?s (reg_index reg)) = true)
+      | [ H : (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg ?s (reg_index reg)) = true)
           |- context[Symbolic.get_reg ?s (reg_index ?ri)] ]
         => generalize (H ri); cbv [Option.is_Some]; break_innermost_match;
            try congruence
@@ -1980,7 +1982,7 @@ Lemma mapM_GetReg_ok_R_full {opts : symbolic_options_computed_opt} {descr:descri
       (Hbounded : Forall (fun v => (0 <= v < 2^64)%Z) reg_vals)
       (Hregval_len : List.length regs = List.length reg_vals)
       (HR : R frame G s ms)
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
   : ((exists reg_idxs,
          List.map (get_reg r) (List.map reg_index regs) = List.map Some reg_idxs
          /\ Forall2 (eval_idx_Z G s') reg_idxs reg_vals)
@@ -1991,7 +1993,7 @@ Lemma mapM_GetReg_ok_R_full {opts : symbolic_options_computed_opt} {descr:descri
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n)
     /\ R frame G s' ms
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
 Proof.
   eapply mapM_GetReg_ok_bounded in H; [ | try eassumption .. ]; [ | destruct s; apply HR .. ]; [].
   all: intuition idtac.
@@ -2012,7 +2014,7 @@ Lemma mapM_GetReg_ok_R {opts : symbolic_options_computed_opt} {descr:description
       (reg_vals := List.map (Semantics.get_reg ms) regs)
       (Hwide : Forall (fun reg => let '(_, _, sz) := index_and_shift_and_bitcount_of_reg reg in sz = 64%N) regs)
       (HR : R frame G s ms)
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
   : ((exists reg_idxs,
          List.map (get_reg r) (List.map reg_index regs) = List.map Some reg_idxs
          /\ Forall2 (eval_idx_Z G s') reg_idxs reg_vals)
@@ -2023,7 +2025,7 @@ Lemma mapM_GetReg_ok_R {opts : symbolic_options_computed_opt} {descr:description
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n)
     /\ R frame G s' ms
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
 Proof.
   subst reg_vals.
   eapply mapM_GetReg_ok_R_full in H; [ eassumption | try eassumption .. ].
@@ -2042,15 +2044,15 @@ Lemma SymexLines_ok_R {opts : symbolic_options_computed_opt}
       (r := s.(symbolic_reg_state))
       (r' := s'.(symbolic_reg_state))
       (H : Symbolic.SymexLines asm s = Success (_tt, s'))
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
       (HR : R frame G s m)
   : exists m',
     Semantics.DenoteLines m asm = Some m'
     /\ gensym_dag_ok G d
     /\ (forall e n, eval G d e n -> eval G d' e n)
     /\ R frame G s' m'
     /\ same_mem_addressed s s'
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
 Proof.
   destruct _tt.
   pose proof H as H'; eapply SymexLines_mem_same in H'.
@@ -2121,7 +2123,7 @@ Lemma LoadArray_ok_R {opts : symbolic_options_computed_opt} {descr:description}
       (HR : R frame G s ms)
       (Hbase : eval_idx_Z G d base (Z.land base_val (Z.ones 64)))
       (Hbase_word_val : base_val = word.unsigned base_word_val)
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
   : ((exists (addrs : list idx),
          Permutation m (List.combine addrs idxs ++ m')
          /\ List.length idxs = len
@@ -2135,7 +2137,7 @@ Lemma LoadArray_ok_R {opts : symbolic_options_computed_opt} {descr:description}
             Forall2 (eval_idx_Z G d') idxs vals
             /\ Forall (fun v => 0 <= v < 2^64)%Z vals
             /\ R (frame * array cell64 (word.of_Z 8) base_word_val vals)%sep G s' ms)
-        /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true)).
+        /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true)).
 Proof.
   replace (Z.land base_val (Z.ones 64)) with base_val in Hbase
       by now (subst; rewrite Z.land_ones by lia; rewrite Z.mod_small by apply Properties.word.unsigned_range).
@@ -2433,7 +2435,7 @@ Lemma LoadOutputs_ok_R {opts : symbolic_options_computed_opt} {descr:description
                                        => dereference_scalar = true
                                      | _ => True
                                      end) outputaddrs)
-      (Hreg_good : forall reg, Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
+      (Hreg_good : forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r (reg_index reg)) = true)
   : (exists output_vals_words (output_vals' : list Z) (outputaddrs' : list (idx + list idx)) vals,
         output_vals' = List.map word.unsigned output_vals_words
         /\ Forall (fun v => (0 <= v < 2^64)%Z) output_vals'
@@ -2500,7 +2502,7 @@ Lemma LoadOutputs_ok_R {opts : symbolic_options_computed_opt} {descr:description
     /\ f = f'
     /\ gensym_dag_ok G d'
     /\ (forall e n, eval G d e n -> eval G d' e n)
-    /\ (forall reg, Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
+    /\ (forall reg, is_ip_register_index (reg_index reg) = false -> Option.is_Some (Symbolic.get_reg r' (reg_index reg)) = true).
 Proof.
   pose dereference_scalar as dereference_scalar'.
   pose proof (fun (*i*) rv (*(H : nth_error outputaddrs i = Some (inl (inl rv)))*) H1 => @Forall2_get_reg_of_R_regs G d r ms [rv] (Forall_cons _ H1 (Forall_nil _)) ltac:(destruct s; apply HR)).

diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v
@@ -1,5 +1,6 @@
 From Coq Require Import List.
 From Coq Require Import Lia.
+Require Import Crypto.Util.Option.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.
 From Coq Require Import NArith.
 From Coq Require Import ZArith.
@@ -318,13 +319,14 @@ Lemma get_reg_R_regs d s m (HR : R_regs d s m) ri :
 Proof using Type.
   cbv [Symbolic.get_reg]; intros.
   rewrite <-Tuple.nth_default_to_list in H.
-  cbv [nth_default] in H; BreakMatch.break_match_hyps; subst; [|solve[congruence] ].
-  destruct s,m; cbn in *; cbv [R_regs R_reg] in *.
+  break_innermost_match_hyps; inversion_option.
+  cbv [nth_default] in H; break_match_hyps; subst; [|solve[congruence] ].
+  destruct s,m; cbn -[is_ip_register_index] in *; cbv [R_regs R_reg] in *.
   eapply Tuple.fieldwise_to_list_iff in HR.
   eapply Forall.Forall2_forall_iff_nth_error in HR; cbv [Crypto.Util.Option.option_eq] in HR.
 
   rewrite Heqo in HR.
-  BreakMatch.break_match_hyps; [|solve[contradiction]].
+  break_match_hyps; [|solve[contradiction]].
   specialize (proj1 HR _ eq_refl).
   eexists; split; [eassumption|].