From e7fb00079ea8a26bf1dbb1820ff36b8a022cbf7f Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Tue, 17 Nov 2020 15:10:22 +0100
Subject: extend the aarch64 scheduling verifier to check builtins.

NB 1: the equality is purely syntactical on builtins.
This should not be a limit for our scheduler.

NB 2: the correctness proof remains to be done (only a skeleton is given).
---
 aarch64/Asmblockdeps.v | 63 ++++++++++++++++++++++++++++++++++++++++++++------
 1 file changed, 56 insertions(+), 7 deletions(-)

(limited to 'aarch64/Asmblockdeps.v')

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 25b9c5c5..309c5909 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -23,7 +23,7 @@
  *)
 
 Require Import AST.
-Require Import Asmblock.
+Require Import Asm Asmblock.
 Require Import Asmblockgenproof0 Asmblockprops.
 Require Import Values.
 Require Import Globalenvs.
@@ -42,6 +42,53 @@ Require Import Lia.
 
 Open Scope impure.
 
+(** auxiliary treatments of builtins *)
+
+Definition has_builtin(bb: bblock): bool :=
+ match exit bb with
+ | Some (Pbuiltin _ _ _) => true
+ | _ => false
+ end.
+
+Remark builtin_arg_eq_dreg: forall (a b: builtin_arg dreg), {a=b} + {a<>b}.
+Proof.
+  intros.
+  apply (builtin_arg_eq dreg_eq).
+Qed.
+
+Remark builtin_res_eq_dreg: forall (a b: builtin_res dreg), {a=b} + {a<>b}.
+Proof. 
+  intros. 
+  apply (builtin_res_eq dreg_eq).
+Qed.
+
+Definition assert_same_builtin (bb1 bb2: bblock): ?? unit := 
+  match exit bb1 with
+  | Some (Pbuiltin ef1 lbar1 brr1) =>
+     match exit bb2 with
+     | Some (Pbuiltin ef2 lbar2 brr2) => 
+        if (external_function_eq ef1 ef2) then
+           if (list_eq_dec builtin_arg_eq_dreg lbar1 lbar2) then
+              if (builtin_res_eq_dreg brr1 brr2) then RET tt
+              else FAILWITH "Different brr in Pbuiltin"
+           else FAILWITH "Different lbar in Pbuiltin"
+        else FAILWITH "Different ef in Pbuiltin"
+     | _ =>  FAILWITH "Expected a builtin: found something else" (* XXX: on peut raffiner le message d'erreur si nécessaire *)
+     end
+  | _ => RET tt (* ok *)
+  end.
+
+Lemma assert_same_builtin_correct (bb1 bb2: bblock):
+  WHEN assert_same_builtin bb1 bb2 ~> _ THEN
+    has_builtin bb1 = true -> exit bb1 = exit bb2.
+Proof.
+  unfold assert_same_builtin, has_builtin.
+  destruct (exit bb1) as [[]|]; simpl; try (wlp_simplify; congruence).
+  destruct (exit bb2) as [[]|]; wlp_simplify.
+Qed.
+Global Opaque assert_same_builtin.
+Local Hint Resolve assert_same_builtin_correct: wlp.
+
 (** Definition of [L] *)
 
 Module P<: ImpParam.
@@ -2072,13 +2119,13 @@ Qed.*)
 (*Proof.*)
   (*induction 1; simpl; econstructor; eauto.*)
 (*Qed.*)
-
+(*
 Lemma trans_body_app bdy1: forall bdy2,
    trans_body (bdy1++bdy2) = (trans_body bdy1) ++ (trans_body bdy2).
 Proof.
   induction bdy1; simpl; congruence.
 Qed.
-
+*)
 (*Theorem trans_block_perserves_permutation bdy1 bdy2 b:*)
   (*Permutation (bdy1 ++ bdy2) (body b) ->*)
   (*Permutation (trans_block b) ((trans_block_aux bdy1 (size b) (exit b))++(trans_body bdy2)).*)
@@ -2243,9 +2290,10 @@ Local Hint Resolve trans_state_match: core.
 Lemma bblock_simu_reduce:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
+  (has_builtin p1 = true -> exit p1 = exit p2) ->
   Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
 Proof.
-  unfold bblock_simu. intros p1 p2 H rs m rs' m' t EBB.
+  unfold bblock_simu. intros p1 p2 H BLT rs m rs' m' t EBB.
   generalize (H (trans_state (State rs m))); clear H.
   intro H. (* TODO How to define this correctly ?
   exploit (bisimu rs m (body p1) (trans_state (State rs m))); eauto.
@@ -2663,19 +2711,20 @@ Qed.
 Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}.
 
 Definition bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool :=
+  assert_same_builtin p1 p2;;
   if verb then
     IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2)
   else
     IST.bblock_simu_test reduce (trans_block p1) (trans_block p2).
 
-Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.
+Local Hint Resolve IST.bblock_simu_test_correct IST.verb_bblock_simu_test_correct: wlp.
 
 (** Main simulation (Impure) theorem *) 
 Theorem bblock_simu_test_correct verb p1 p2 :
   WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2.
 Proof.
-  wlp_simplify.
-Admitted.
+  wlp_simplify; eapply bblock_simu_reduce with (Ge:={| _genv := ge; _fn := fn; _lk := lk |}); eauto.
+Qed.
 (*Qed.*)
 Hint Resolve bblock_simu_test_correct: wlp.
 
-- 
cgit