Add Mbool memory chunk to improve compilation of computations at type _Bool

aarch64/Asmexpand.ml

@@ -270,7 +270,7 @@ let expand_builtin_memcpy  sz al args =
 let expand_builtin_vload_common chunk base ofs res =
   let addr = ADimm(base, ofs) in
   match chunk, res with
-  | Mint8unsigned, BR(IR res) ->
+  | (Mbool | Mint8unsigned), BR(IR res) ->
      emit (Pldrb(W, res, addr))
   | Mint8signed, BR(IR res) ->
      emit (Pldrsb(W, res, addr))
@@ -313,7 +313,7 @@ let expand_builtin_vload chunk args res =
 let expand_builtin_vstore_common chunk base ofs src =
   let addr = ADimm(base, ofs) in
   match chunk, src with
-  | (Mint8signed | Mint8unsigned), BA(IR src) ->
+  | (Mbool | Mint8signed | Mint8unsigned), BA(IR src) ->
      emit (Pstrb(src, addr))
   | (Mint16signed | Mint16unsigned), BA(IR src) ->
      emit (Pstrh(src, addr))

aarch64/Asmgen.v

@@ -992,14 +992,16 @@ Definition transl_load (chunk: memory_chunk) (addr: Op.addressing)
       do rd <- ireg_of dst; transl_addressing 4 addr args (Pldrw_a rd) k
   | Many64 =>
       do rd <- ireg_of dst; transl_addressing 8 addr args (Pldrx_a rd) k
+  | _ =>
+      Error (msg "Asmgen.transl_load")
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
                         (args: list mreg) (src: mreg) (k: code) : res code :=
   match chunk with
-  | Mint8unsigned | Mint8signed =>
+  | Mint8unsigned =>
       do r1 <- ireg_of src; transl_addressing 1 addr args (Pstrb r1) k
-  | Mint16unsigned | Mint16signed =>
+  | Mint16unsigned =>
       do r1 <- ireg_of src; transl_addressing 2 addr args (Pstrh r1) k
   | Mint32 =>
       do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw r1) k
@@ -1013,6 +1015,8 @@ Definition transl_store (chunk: memory_chunk) (addr: Op.addressing)
       do r1 <- ireg_of src; transl_addressing 4 addr args (Pstrw_a r1) k
   | Many64 =>
       do r1 <- ireg_of src; transl_addressing 8 addr args (Pstrx_a r1) k
+  | _ =>
+      Error (msg "Asmgen.transl_store")
   end.
 
 (** Register-indexed loads and stores *)

aarch64/Asmgenproof1.v

@@ -1673,27 +1673,19 @@ Lemma transl_store_correct:
   /\ forall r, data_preg r = true -> rs' r = rs r.
 Proof.
   intros. destruct vaddr; try discriminate. 
-  set (chunk' := match chunk with Mint8signed => Mint8unsigned
-                                | Mint16signed => Mint16unsigned
-                                | _ => chunk end).
   assert (A: exists sz insn,
                 transl_addressing sz addr args insn k = OK c
              /\ (forall ad rs', exec_instr ge fn (insn ad) rs' m =
-                              exec_store ge chunk' ad rs'#(preg_of src) rs' m)).
-  {
-    unfold chunk'; destruct chunk; monadInv H;
+                              exec_store ge chunk ad rs'#(preg_of src) rs' m)).
+  { destruct chunk; monadInv H;
     try rewrite (ireg_of_eq _ _ EQ); try rewrite (freg_of_eq _ _ EQ);
     do 2 econstructor; (split; [eassumption|auto]).
   }
   destruct A as (sz & insn & B & C).
   exploit transl_addressing_correct. eexact B. eexact H0. intros (ad & rs' & P & Q & R).
-  assert (X: Mem.storev chunk' m (Vptr b i) rs#(preg_of src) = Some m').
-  { rewrite <- H1. unfold chunk'. destruct chunk; auto; simpl; symmetry.
-    apply Mem.store_signed_unsigned_8.
-    apply Mem.store_signed_unsigned_16. }
-  assert (Y: exec_store ge chunk' ad rs'#(preg_of src) rs' m =
+  assert (Y: exec_store ge chunk ad rs'#(preg_of src) rs' m =
              Next (nextinstr rs') m').
-  { unfold exec_store. rewrite Q, R, X by auto with asmgen. auto. }
+  { unfold exec_store. rewrite Q, R, H1 by auto with asmgen. auto. }
   econstructor; split.
   eapply exec_straight_opt_right. eexact P.
   apply exec_straight_one. rewrite C, Y; eauto. Simpl. 

aarch64/Conventions1.v

@@ -380,7 +380,7 @@ Definition return_value_needs_normalization (t: rettype) : bool :=
   | Archi.Apple => false
   | Archi.AAPCS64 =>
       match t with
-      | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
+      | Tbool | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
       | _ => false
       end
   end.

arm/Asmexpand.ml

@@ -179,7 +179,7 @@ let offset_in_range chunk ofs =
 
 let expand_builtin_vload_common chunk base ofs res =
   match chunk, res with
-  | Mint8unsigned, BR(IR res) ->
+  | (Mbool | Mint8unsigned), BR(IR res) ->
      emit (Pldrb (res, base, SOimm ofs))
   | Mint8signed, BR(IR res) ->
      emit (Pldrsb (res, base, SOimm ofs))
@@ -232,7 +232,7 @@ let expand_builtin_vload chunk args res =
 
 let expand_builtin_vstore_common chunk base ofs src =
   match chunk, src with
-  | (Mint8signed | Mint8unsigned), BA(IR src) ->
+  | (Mbool | Mint8signed | Mint8unsigned), BA(IR src) ->
      emit (Pstrb (src, base, SOimm ofs))
   | (Mint16signed | Mint16unsigned), BA(IR src) ->
      emit (Pstrh (src, base, SOimm ofs))

arm/Asmgen.v

@@ -727,12 +727,8 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
                        (args: list mreg) (src: mreg) (k: code) :=
   match chunk with
-  | Mint8signed =>
-      transl_memory_access_int Pstrb mk_immed_mem_small src addr args k
   | Mint8unsigned =>
       transl_memory_access_int Pstrb mk_immed_mem_word src addr args k
-  | Mint16signed =>
-      transl_memory_access_int Pstrh mk_immed_mem_small src addr args k
   | Mint16unsigned =>
       transl_memory_access_int Pstrh mk_immed_mem_small src addr args k
   | Mint32 =>

arm/Asmgenproof1.v

@@ -1565,17 +1565,8 @@ Lemma transl_load_correct:
    /\ rs'#(preg_of dst) = v
    /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. destruct chunk; simpl in H.
-  eapply transl_load_int_correct; eauto.
-  eapply transl_load_int_correct; eauto.
-  eapply transl_load_int_correct; eauto.
-  eapply transl_load_int_correct; eauto.
-  eapply transl_load_int_correct; eauto.
-  discriminate.
-  eapply transl_load_float_correct; eauto.
-  eapply transl_load_float_correct; eauto.
-  discriminate.
-  discriminate.
+  intros. destruct chunk; simpl in H; try discriminate;
+  eauto using transl_load_int_correct, transl_load_float_correct.
 Qed.
 
 Lemma transl_store_correct:
@@ -1587,21 +1578,8 @@ Lemma transl_store_correct:
       exec_straight ge fn c rs m k rs' m'
    /\ forall r, data_preg r = true -> preg_notin r (destroyed_by_store chunk addr) -> rs'#r = rs#r.
 Proof.
-  intros. destruct chunk; simpl in H.
-- assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m').
-    rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_8.
-  clear H1. eapply transl_store_int_correct; eauto.
-- eapply transl_store_int_correct; eauto.
-- assert (Mem.storev Mint16unsigned m a (rs (preg_of src)) = Some m').
-    rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_16.
-  clear H1. eapply transl_store_int_correct; eauto.
-- eapply transl_store_int_correct; eauto.
-- eapply transl_store_int_correct; eauto.
-- discriminate.
-- eapply transl_store_float_correct; eauto.
-- eapply transl_store_float_correct; eauto.
-- discriminate.
-- discriminate.
+  intros. destruct chunk; simpl in H; try discriminate;
+  eauto using transl_store_int_correct, transl_store_float_correct.
 Qed.
 
 End CONSTRUCTORS.

arm/SelectOp.vp

@@ -452,6 +452,7 @@ Nondetfunction singleofintu (e: expr) :=
 
 Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
   match chunk with
+  | Mbool => true
   | Mint8signed => true
   | Mint8unsigned => true
   | Mint16signed => true
@@ -466,6 +467,7 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
 
 Definition can_use_Aindexed2shift (chunk: memory_chunk) (s: shift): bool :=
   match chunk with
+  | Mbool => false
   | Mint8signed => false
   | Mint8unsigned => true
   | Mint16signed => false

backend/CSE.v

@@ -284,6 +284,7 @@ Definition kill_loads_after_store
 
 Definition store_normalized_range (chunk: memory_chunk) : aval :=
   match chunk with
+  | Mbool => Uns Ptop 1
   | Mint8signed => Sgn Ptop 8
   | Mint8unsigned => Uns Ptop 8
   | Mint16signed => Sgn Ptop 16

backend/CSEproof.v

@@ -495,6 +495,7 @@ Lemma store_normalized_range_sound:
 Proof.
   intros. unfold Val.load_result; remember Archi.ptr64 as ptr64.
   destruct chunk; simpl in *; destruct v; auto.
+- inv H. apply is_uns_1 in H4; destruct H4; subst i; auto.
 - inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto.
 - inv H. rewrite is_uns_zero_ext in H4 by lia. rewrite H4; auto.
 - inv H. rewrite is_sgn_sign_ext in H4 by lia. rewrite H4; auto.

backend/Inliningproof.v

@@ -767,9 +767,7 @@ Proof.
     destruct (zle sz 2). extlia.
     destruct (zle sz 4). extlia.
     auto.
-  destruct chunk; simpl in *; auto.
-  apply Z.divide_1_l.
-  apply Z.divide_1_l.
+  destruct chunk; simpl in *; auto using Z.divide_1_l.
   apply H2; lia.
   apply H2; lia.
 Qed.

backend/NeedDomain.v

@@ -725,7 +725,7 @@ Qed.
 
 Definition store_argument (chunk: memory_chunk) :=
   match chunk with
-  | Mint8signed | Mint8unsigned => I (Int.repr 255)
+  | Mbool | Mint8signed | Mint8unsigned => I (Int.repr 255)
   | Mint16signed | Mint16unsigned => I (Int.repr 65535)
   | _ => All
   end.
@@ -756,6 +756,8 @@ Proof.
   change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto.
 - InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod.
   change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto.
+- InvAgree. apply SAME. simpl; f_equal. apply encode_int_8_mod.
+  change 8 with (Int.size (Int.repr 255)). apply iagree_eqmod; auto.
 - InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod.
   change 16 with (Int.size (Int.repr 65535)). apply iagree_eqmod; auto.
 - InvAgree. apply SAME. simpl; f_equal. apply encode_int_16_mod.
@@ -775,6 +777,9 @@ Lemma store_argument_load_result:
 Proof.
   unfold store_argument; intros; destruct chunk;
   auto using Val.load_result_lessdef; InvAgree; simpl.
+- apply Val.norm_bool_lessdef.
+  apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8).
+  auto. lia.
 - apply sign_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8).
   auto. compute; auto.
 - apply zero_ext_sound with (v := Vint i) (w := Vint i0) (x := All) (n := 8).

backend/Stacking.v

@@ -62,6 +62,32 @@ Fixpoint restore_callee_save_rec (rl: list mreg) (ofs: Z) (k: Mach.code) :=
 Definition restore_callee_save (fe: frame_env) (k: Mach.code) :=
   restore_callee_save_rec fe.(fe_used_callee_save) fe.(fe_ofs_callee_save) k.
 
+(** * Simplification of loads and stores *)
+
+(** Some memory loads and stores don't correspond directly to a processor
+    instruction.  For instance, there's only one "store 8 bits" instruction
+    for the three memory chunks [Mint8unsigned],  [Mint8signed], [Mbool].
+    Here, we map all three chunks to [Mint8unsigned] stores
+    and have only one processor instruction for the latter. *)
+
+Definition simplify_store (chunk: memory_chunk) : memory_chunk :=
+  match chunk with
+  | Mbool => Mint8unsigned
+  | Mint8signed => Mint8unsigned
+  | Mint16signed => Mint16unsigned
+  | _ => chunk
+  end.
+
+(** Likewise, there is no "load Boolean" instruction that does exactly
+    what a load with chunk [Mbool] does.  We replace [Mbool] loads
+    with [Mint8unsigned] loads, which are always more defined. *)
+
+Definition simplify_load (chunk: memory_chunk) : memory_chunk :=
+  match chunk with
+  | Mbool => Mint8unsigned
+  | _ => chunk
+  end.
+
 (** * Code transformation. *)
 
 (** Translation of operations and addressing mode.
@@ -134,9 +160,9 @@ Definition transl_instr
   | Lop op args res =>
       Mop (transl_op fe op) args res :: k
   | Lload chunk addr args dst =>
-      Mload chunk (transl_addr fe addr) args dst :: k
+      Mload (simplify_load chunk) (transl_addr fe addr) args dst :: k
   | Lstore chunk addr args src =>
-      Mstore chunk (transl_addr fe addr) args src :: k
+      Mstore (simplify_store chunk) (transl_addr fe addr) args src :: k
   | Lcall sig ros =>
       Mcall sig ros :: k
   | Ltailcall sig ros =>

backend/Stackingproof.v

@@ -1310,6 +1310,42 @@ Qed.
 
 End FRAME_PROPERTIES.
 
+(** * Simplification of loads and stores *)
+
+Lemma simplify_load_correct: forall chunk m a v,
+  Mem.loadv chunk m a = Some v ->
+  exists v', Mem.loadv (simplify_load chunk) m a = Some v' /\ Val.lessdef v v'.
+Proof.
+  intros. destruct a; simpl in *; try discriminate.
+  destruct chunk; simpl; try (exists v; auto; fail).
+  rewrite Mem.load_bool_int8_unsigned in H.
+  destruct (Mem.load Mint8unsigned m b (Ptrofs.unsigned i)) as [v'|]; simpl in H; inv H.
+  exists v'; auto using Val.norm_bool_is_lessdef.
+Qed.
+
+Lemma simplify_store_correct: forall chunk m a v m',
+  Mem.storev chunk m a v = Some m' ->
+  Mem.storev (simplify_store chunk) m a v = Some m'.
+Proof.
+  intros. destruct a; simpl in *; try discriminate. rewrite <- H. symmetry.
+  destruct chunk; simpl; auto.
+- apply Mem.store_bool_unsigned_8.
+- apply Mem.store_signed_unsigned_8.
+- apply Mem.store_signed_unsigned_16.
+Qed.
+
+Lemma simplify_load_destroyed: forall chunk addr,
+  destroyed_by_load (simplify_load chunk) addr = destroyed_by_load chunk addr.
+Proof.
+  intros; destruct chunk; reflexivity.
+Qed.
+
+Lemma simplify_store_destroyed: forall chunk addr,
+  destroyed_by_store (simplify_store chunk) addr = destroyed_by_store chunk addr.
+Proof.
+  intros; destruct chunk; reflexivity.
+Qed.
+
 (** * Call stack invariants *)
 
 (** This is the memory assertion that captures the contents of the stack frames
@@ -1919,12 +1955,16 @@ Proof.
   apply sep_proj2 in SEP. apply sep_proj2 in SEP. apply sep_proj1 in SEP. eexact SEP.
   eauto. eauto.
   intros [v' [C D]].
+  exploit simplify_load_correct; eauto. 
+  intros [v'' [E F]].
+  assert (G: Val.inject j v v'').
+  { inv F; auto. inv D; auto. }
   econstructor; split.
   apply plus_one. econstructor.
   instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
-  eexact C. eauto.
+  eexact E. eauto.
   econstructor; eauto with coqlib.
-  apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto.
+  apply agree_regs_set_reg. rewrite transl_destroyed_by_load, simplify_load_destroyed. apply agree_regs_undef_regs; auto. auto.
   apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto.
 
 - (* Lstore *)
@@ -1942,9 +1982,9 @@ Proof.
   econstructor; split.
   apply plus_one. econstructor.
   instantiate (1 := a'). rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved.
-  eexact C. eauto.
+  apply simplify_store_correct. eexact C. eauto.
   econstructor. eauto. eauto. eauto.
-  rewrite transl_destroyed_by_store. apply agree_regs_undef_regs; auto.
+  rewrite transl_destroyed_by_store, simplify_store_destroyed. apply agree_regs_undef_regs; auto.
   apply agree_locs_undef_locs. auto. apply destroyed_by_store_caller_save.
   auto. eauto with coqlib.
   eapply frame_undef_regs; eauto.