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/Compiler.v | 3 +- src/bourdoncle/BourdoncleAux.ml | 2 +- src/dune | 1 + src/extraction/Extraction.v | 10 ++- 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 +- 10 files changed, 229 insertions(+), 50 deletions(-) create mode 100644 src/dune (limited to 'src') diff --git a/src/Compiler.v b/src/Compiler.v index 5ff291e..2fb909e 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -55,6 +55,7 @@ Require Import compcert.common.Errors. Require Import compcert.common.Linking. Require Import compcert.common.Smallstep. Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Maps. Require vericert.hls.Verilog. Require vericert.hls.Veriloggen. @@ -279,7 +280,7 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := @@ print (print_GibleSeq 0) @@ total_if HLSOpts.optim_if_conversion CondElim.transf_program @@ print (print_GibleSeq 1) - @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (Maps.PTree.empty _ :: Maps.PTree.empty _ :: nil)) + @@ total_if HLSOpts.optim_if_conversion (fold_left (fun a b => IfConversion.transf_program b a) (PTree.empty _ :: PTree.empty _ :: nil)) @@ print (print_GibleSeq 2) @@@ DeadBlocks.transf_program @@ print (print_GibleSeq 3) diff --git a/src/bourdoncle/BourdoncleAux.ml b/src/bourdoncle/BourdoncleAux.ml index 1ea4de6..932bb18 100644 --- a/src/bourdoncle/BourdoncleAux.ml +++ b/src/bourdoncle/BourdoncleAux.ml @@ -20,7 +20,7 @@ let positive_of_int n = P.of_int (n+1) (* Functions copied from SliceToString to avoid mutual inclusion *) let nodeToString (p : P.t) : string = - Int.to_string (P.to_int p) + string_of_int (P.to_int p) let rec cleanListToString' (aToString: 'a -> string) (l : 'a list) = match l with | [] -> "" diff --git a/src/dune b/src/dune new file mode 100644 index 0000000..fdcb9fd --- /dev/null +++ b/src/dune @@ -0,0 +1 @@ +(dirs (:standard \ pipelining)) diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 20fc48c..b65bc41 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -55,9 +55,13 @@ From compcert Require Parser Initializers. +From cohpred_theory Require + Smtpredicate. + (* Standard lib *) Require Import ExtrOcamlBasic. Require Import ExtrOcamlString. +Require Import ExtrOCamlInt63. (* Coqlib *) Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". @@ -172,7 +176,7 @@ Extract Constant Cabs.char_code => "int64". Load extractionMachdep. (* Avoid name clashes *) -Extraction Blacklist List String Int. +Extraction Blacklist List String Int Uint63. (* Cutting the dependency to R. *) Extract Inlined Constant Defs.F2R => "fun _ -> assert false". @@ -185,6 +189,8 @@ Extract Constant GibleSeqgen.partition => "Partition.partition". Extract Constant GiblePargen.schedule => "Schedule.schedule_fn". Extract Constant Abstr.print_forest => "(PrintAbstr.print_forest stdout)". +Extract Constant Smtpredicate.pred_verit_unsat => "Cohpred.smt_certificate". + (* Loop normalization *) Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle". (*Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".*) @@ -202,6 +208,8 @@ Separate Extraction Verilog.stmnt_to_list Bourdoncle.bourdoncle + Smtpredicate.check_smt_total + Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes 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