From 4d262face34cb79d478823fd8db32cf02dc187f8 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 21 Jun 2023 18:57:33 +0100 Subject: Add SMTCoq solver as dependency --- src/hls/DeadBlocksproof.v | 50 +++++------ src/hls/Gible.v | 4 +- src/hls/GiblePargen.v | 13 +-- src/hls/GiblePargenproof.v | 6 +- src/hls/GiblePargenproofEquiv.v | 186 +++++++++++++++++++++++++++++++++++++--- src/hls/RTLParFU.v | 4 +- 6 files changed, 216 insertions(+), 47 deletions(-) (limited to 'src/hls') diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v index 8ac6d0d..1783213 100644 --- a/src/hls/DeadBlocksproof.v +++ b/src/hls/DeadBlocksproof.v @@ -3,30 +3,32 @@ both that the transformation ensures that generated functions are satisfying the predicate [wf_dfs_function] and that the transformation preserves the semantics. *) -Require Recdef. -Require Import FSets. -Require Import Coqlib. -Require Import Ordered. -Require Import Errors. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Globalenvs. -Require Import Op. -Require Import Registers. -Require Import Smallstep. -Require Import DeadBlocks. -Require Import Kildall. -Require Import Conventions. -Require Import Integers. -Require Import Floats. -Require Import Utils. -Require Import Events. -Require Import Gible. -Require Import GibleSeq. -Require Import Relation_Operators. -Require Import Vericertlib. +From Coq Require funind.Recdef. +From Coq Require Import FSets.FSets. +From Coq Require Import Program.Utils. +From Coq Require Import Relation_Operators. + +From compcert Require Import Errors. +From compcert Require Import Maps. +From compcert Require Import AST. +From compcert Require Import Integers. +From compcert Require Import Values. +From compcert Require Import Globalenvs. +From compcert Require Import Op. +From compcert Require Import Registers. +From compcert Require Import Smallstep. +From compcert Require Import Kildall. +From compcert Require Import Conventions. +From compcert Require Import Integers. +From compcert Require Import Floats. +From compcert Require Import Events. +From compcert Require Import Ordered. +From compcert Require Import Coqlib. + +From vericert Require Import DeadBlocks. +From vericert Require Import Gible. +From vericert Require Import GibleSeq. +From vericert Require Import Vericertlib. Unset Allow StrictProp. diff --git a/src/hls/Gible.v b/src/hls/Gible.v index cb080c5..b8feb37 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -39,8 +39,8 @@ Require Import compcert.common.Smallstep. Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. -Require Import Predicate. -Require Import Vericertlib. +Require Import vericert.hls.Predicate. +Require Import vericert.common.Vericertlib. Definition node := positive. Definition predicate := positive. diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index 736f461..25531a8 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -26,8 +26,11 @@ Require Import compcert.common.Values. Require Import compcert.lib.Floats. Require Import compcert.lib.Integers. Require Import compcert.lib.Maps. +Require compcert.common.Errors. Require compcert.verilog.Op. +Module Err := compcert.common.Errors. + Require Import vericert.common.Vericertlib. Require Import vericert.common.Monad. Require Import vericert.hls.GibleSeq. @@ -464,19 +467,19 @@ Top-level Functions Parameter schedule : GibleSeq.function -> GiblePar.function. Definition transl_function (f: GibleSeq.function) - : Errors.res GiblePar.function := + : Err.res GiblePar.function := let tfcode := fn_code (schedule f) in if check_scheduled_trees f.(GibleSeq.fn_code) tfcode then - Errors.OK (mkfunction f.(GibleSeq.fn_sig) + Err.OK (mkfunction f.(GibleSeq.fn_sig) f.(GibleSeq.fn_params) f.(GibleSeq.fn_stacksize) tfcode f.(GibleSeq.fn_entrypoint)) else - Errors.Error - (Errors.msg "GiblePargen: Could not prove the blocks equivalent."). + Err.Error + (Err.msg "GiblePargen: Could not prove the blocks equivalent."). Definition transl_fundef := transf_partial_fundef transl_function. -Definition transl_program (p : GibleSeq.program) : Errors.res GiblePar.program := +Definition transl_program (p : GibleSeq.program) : Err.res GiblePar.program := transform_partial_program transl_fundef p. diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 5d36ae9..b774b48 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -127,7 +127,7 @@ Qed. Definition state_lessdef := GiblePargenproofEquiv.match_states. Definition match_prog (prog : GibleSeq.program) (tprog : GiblePar.program) := - match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + match_program (fun cu f tf => transl_fundef f = OK tf) eq prog tprog. (* TODO: Fix the `bb` and add matches for them. *) Inductive match_stackframes: GibleSeq.stackframe -> GiblePar.stackframe -> Prop := @@ -177,7 +177,7 @@ Section CORRECTNESS. forall (b: Values.block) (f: GibleSeq.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. Proof using TRANSL. intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. @@ -187,7 +187,7 @@ Section CORRECTNESS. forall (v: Values.val) (f: GibleSeq.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. Proof using TRANSL. intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index 9e58981..1f3ad1c 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -41,6 +41,9 @@ Require vericert.common.NonEmpty. Module NE := NonEmpty. Import NE.NonEmptyNotation. +Module OE := MonadExtra(Option). +Import OE.MonadNotation. + #[local] Open Scope non_empty_scope. #[local] Open Scope positive. #[local] Open Scope pred_op. @@ -482,12 +485,50 @@ Proof. apply X. Defined. -Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool := +Require cohpred_theory.Predicate. +Require cohpred_theory.Smtpredicate. +Module TV := cohpred_theory.Predicate. +Module STV := cohpred_theory.Smtpredicate. + +Module TVL := TV.ThreeValued(PHashExpr). + +Fixpoint transf_pred_op {A} (p: @Predicate.pred_op A): @TV.pred A := + match p with + | Ptrue => TV.Ptrue + | Pfalse => TV.Pfalse + | Plit (b, p) => + if b then TV.Pbase p else TV.Pnot (TV.Pbase p) + | Pand p1 p2 => + TV.Pand (transf_pred_op p1) (transf_pred_op p2) + | Por p1 p2 => + TV.Por (transf_pred_op p1) (transf_pred_op p2) + end. + +(*| +This following equivalence checker takes two pred_pexpr, hashes them, and then +proves them equivalent. However, it's not quite clear whether this actually +proves that, given that ``pe1`` results in a value, then ``pe2`` will also +result in a value. The issue is that even though this proves that both hashed +predicates will result in the same value, how do we then show that the initial +predicates will also be correct and equivalent. +|*) + +Definition beq_pred_pexpr' (pe1 pe2: pred_pexpr): bool := if pred_pexpr_eqb pe1 pe2 then true else let (np1, h) := hash_predicate 1 pe1 (PTree.empty _) in let (np2, h') := hash_predicate 1 pe2 h in equiv_check np1 np2. +(*| +Given two predicated expressions, prove that they are equivalent. +|*) + +Definition beq_pred_pexpr (pe1 pe2: pred_pexpr): bool := + if pred_pexpr_eqb pe1 pe2 then true else + let (np1, h) := TVL.hash_predicate (transf_pred_op pe1) (Maps.PTree.empty _) in + let (np2, h') := TVL.hash_predicate (transf_pred_op pe2) h in + STV.check_smt_total (TV.equiv np1 np2). + Lemma inj_asgn_eg : forall a b, (a =? b)%positive = (a =? a)%positive -> a = b. Proof. intros. destruct (peq a b); subst. @@ -815,7 +856,7 @@ Section CORRECT. apply sem_pred_expr_cons_false; auto. now apply sem_pexpr_corr. Qed. - + Lemma sem_pred_expr_corr : forall A B (sem: forall G, @Abstr.ctx G -> A -> B -> Prop) a p r, (forall x y, sem _ ictx x y -> sem _ octx x y) -> @@ -870,7 +911,7 @@ Section SEM_PRED_EXEC. + apply IHp2 in H. solve [constructor; auto]. + apply IHp1 in H2. apply IHp2 in H4. solve [constructor; auto]. Qed. - + Lemma sem_pexpr_negate2 : forall p b, sem_pexpr ctx (¬ p) (negb b) -> @@ -1127,7 +1168,7 @@ Module HashExprNorm(HS: Hashable). | Some p' => equiv_check p p' | None => equiv_check p ⟂ end. - + Definition tree_equiv_check_None_el (np2: PTree.t pred_op) (n: positive) (p: pred_op): bool := match np2 ! n with | Some p' => true @@ -1230,7 +1271,7 @@ Module HashExprNorm(HS: Hashable). + rewrite PTree.gso in H2 by auto. now rewrite PTree.gempty in H2. - assert (H.wf_hash_table h1) by eauto using H.wf_hash_table_distr. destruct_match; inv H0. - + destruct (peq h0 x); subst; eauto. + + destruct (peq h0 x); subst; eauto. rewrite PTree.gso in H1 by auto. eauto. + destruct (peq h0 x); subst; eauto. * pose proof Heqp0 as X. @@ -1660,15 +1701,138 @@ Proof. specialize (H1 h br). Abort. +Local Open Scope monad_scope. +Fixpoint sem_valueF (e: expression) : option val := + match e with + | Ebase (Reg r) => Some ((ctx_rs ctx) !! r) + | Eop op args => + do lv <- sem_val_listF args; + Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op lv (ctx_mem ctx) + | Eload chunk addr args mexp => + do m' <- sem_memF mexp; + do lv <- sem_val_listF args; + do a <- Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv; + Mem.loadv chunk m' a + | _ => None + end +with sem_memF (e: expression) : option mem := + match e with + | Ebase Mem => Some (ctx_mem ctx) + | Estore vexp chunk addr args mexp => + do m' <- sem_memF mexp; + do v <- sem_valueF vexp; + do lv <- sem_val_listF args; + do a <- Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv; + Mem.storev chunk m' a v + | _ => None + end +with sem_val_listF (e: expression_list) : option (list val) := + match e with + | Enil => Some nil + | Econs e l => + do v <- sem_valueF e; + do lv <- sem_val_listF l; + Some (v :: lv) + end. + +Definition sem_predF (e: pred_expression): option bool := + match e with + | PEbase p => Some ((ctx_ps ctx) !! p) + | PEsetpred c args => + do lv <- sem_val_listF args; + Op.eval_condition c lv (ctx_mem ctx) + end. +Local Close Scope monad_scope. + +Definition sem_pexprF := TVL.eval_predicate sem_predF. + +Lemma sem_valueF_correct : + forall e v m, + (sem_valueF e = Some v -> sem_value ctx e v) + /\ (sem_memF e = Some m -> sem_mem ctx e m). +Proof. + induction e using expression_ind2 with + (P0 := fun p => forall l, sem_val_listF p = Some l -> sem_val_list ctx p l); intros. + - split; intros; destruct r; try discriminate; cbn in *; inv H; constructor. + - split; intros. + + cbn in *; unfold Option.bind in *; destruct_match; try discriminate. + econstructor; eauto. + + cbn in *. discriminate. + - split; intros; cbn in *; try discriminate; unfold Option.bind in *; + repeat (destruct_match; try discriminate; []). + econstructor; eauto. eapply IHe0; auto. + - split; intros; cbn in *; try discriminate; unfold Option.bind in *; + repeat (destruct_match; try discriminate; []). + econstructor; eauto. eapply IHe3; eauto. eapply IHe1; eauto. + - cbn in *. inv H. constructor. + - cbn in *; unfold Option.bind in *; + repeat (destruct_match; try discriminate; []). inv H. constructor; eauto. + eapply IHe; auto. apply (ctx_mem ctx). +Qed. + +Lemma sem_val_listF_correct : + forall l vl, + sem_val_listF l = Some vl -> + sem_val_list ctx l vl. +Proof. + induction l. + - intros. cbn in *. inv H. constructor. + - cbn; intros. unfold Option.bind in *; + repeat (destruct_match; try discriminate; []). inv H. constructor; eauto. + eapply sem_valueF_correct; eauto. apply (ctx_mem ctx). +Qed. + +Lemma sem_valueF_correct2 : + forall e v m, + (sem_value ctx e v -> sem_valueF e = Some v) + /\ (sem_mem ctx e m -> sem_memF e = Some m). +Proof. + induction e using expression_ind2 with + (P0 := fun p => forall l, sem_val_list ctx p l -> sem_val_listF p = Some l); intros. + - split; inversion 1; cbn; auto. + - split; inversion 1; subst; clear H. cbn; unfold Option.bind. + erewrite IHe; eauto. + - split; inversion 1; subst; clear H. cbn; unfold Option.bind. + specialize (IHe0 v m'). inv IHe0. + erewrite H0; eauto. erewrite IHe; eauto. rewrite H8; auto. + - split; inversion 1; subst; clear H. cbn; unfold Option.bind. + specialize (IHe3 v0 m'); inv IHe3. + specialize (IHe1 v0 m'); inv IHe1. + erewrite H0; eauto. + erewrite H1; eauto. + erewrite IHe2; eauto. + rewrite H10; auto. + - inv H. auto. + - inv H. cbn; unfold Option.bind. + specialize (IHe v (ctx_mem ctx)). inv IHe. + erewrite H; eauto. + erewrite IHe0; eauto. +Qed. + +Lemma sem_val_listF_correct2 : + forall l vl, + sem_val_list ctx l vl -> + sem_val_listF l = Some vl. +Proof. + induction l. + - inversion 1; subst; auto. + - inversion 1; subst; clear H. + specialize (sem_valueF_correct2 e v (ctx_mem ctx)); inversion 1; clear H. + cbn; unfold Option.bind. erewrite H0; eauto. erewrite IHl; eauto. +Qed. + +(* Definition eval_pexpr_atom {G} (ctx: @Abstr.ctx G) (p: pred_expression) := *) + Lemma sem_pexpr_beq_correct : - forall p1 p2 b, + forall p1 p2, beq_pred_pexpr p1 p2 = true -> - sem_pexpr ctx p1 b -> - sem_pexpr ctx p2 b. + sem_pexprF (transf_pred_op p1) = sem_pexprF (transf_pred_op p2). Proof. - unfold beq_pred_pexpr. - induction p1; intros; destruct_match; crush. - Admitted. + unfold beq_pred_pexpr; intros. + destruct_match; subst; auto. + repeat destruct_match. + pose proof STV.valid_check_smt_total. + unfold sem_pexprF. (*| This should only require a proof of sem_pexpr_beq_correct, the rest is diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v index b677be7..b28c0ee 100644 --- a/src/hls/RTLParFU.v +++ b/src/hls/RTLParFU.v @@ -29,8 +29,8 @@ Require Import compcert.lib.Maps. Require Import compcert.verilog.Op. Require Import vericert.hls.FunctionalUnits. -Require Import Predicate. -Require Import Vericertlib. +Require Import vericert.hls.Predicate. +Require Import vericert.common.Vericertlib. Definition node := positive. Definition predicate := positive. -- cgit