From ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sun, 30 Aug 2020 14:03:40 +0100 Subject: Add RTLBlock intermediate language --- src/hls/Array.v | 337 ++++++ src/hls/AssocMap.v | 217 ++++ src/hls/HTL.v | 171 +++ src/hls/HTLgen.v | 654 +++++++++++ src/hls/HTLgenproof.v | 2683 +++++++++++++++++++++++++++++++++++++++++++++ src/hls/HTLgenspec.v | 641 +++++++++++ src/hls/Partition.ml | 60 + src/hls/PrintHTL.ml | 81 ++ src/hls/PrintRTLBlock.ml | 0 src/hls/PrintVerilog.ml | 232 ++++ src/hls/PrintVerilog.mli | 25 + src/hls/RTLBlock.v | 69 ++ src/hls/RTLBlockgen.v | 39 + src/hls/Value.v | 551 ++++++++++ src/hls/ValueInt.v | 167 +++ src/hls/Verilog.v | 893 +++++++++++++++ src/hls/Veriloggen.v | 65 ++ src/hls/Veriloggenproof.v | 368 +++++++ 18 files changed, 7253 insertions(+) create mode 100644 src/hls/Array.v create mode 100644 src/hls/AssocMap.v create mode 100644 src/hls/HTL.v create mode 100644 src/hls/HTLgen.v create mode 100644 src/hls/HTLgenproof.v create mode 100644 src/hls/HTLgenspec.v create mode 100644 src/hls/Partition.ml create mode 100644 src/hls/PrintHTL.ml create mode 100644 src/hls/PrintRTLBlock.ml create mode 100644 src/hls/PrintVerilog.ml create mode 100644 src/hls/PrintVerilog.mli create mode 100644 src/hls/RTLBlock.v create mode 100644 src/hls/RTLBlockgen.v create mode 100644 src/hls/Value.v create mode 100644 src/hls/ValueInt.v create mode 100644 src/hls/Verilog.v create mode 100644 src/hls/Veriloggen.v create mode 100644 src/hls/Veriloggenproof.v (limited to 'src/hls') diff --git a/src/hls/Array.v b/src/hls/Array.v new file mode 100644 index 0000000..fe0f6b2 --- /dev/null +++ b/src/hls/Array.v @@ -0,0 +1,337 @@ +Set Implicit Arguments. + +Require Import Lia. +Require Import Vericertlib. +From Coq Require Import Lists.List Datatypes. + +Import ListNotations. + +Local Open Scope nat_scope. + +Record Array (A : Type) : Type := + mk_array + { arr_contents : list A + ; arr_length : nat + ; arr_wf : length arr_contents = arr_length + }. + +Definition make_array {A : Type} (l : list A) : Array A := + @mk_array A l (length l) eq_refl. + +Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A := + match i, l with + | _, nil => nil + | S n, h :: t => h :: list_set n x t + | O, h :: t => x :: t + end. + +Lemma list_set_spec1 {A : Type} : + forall l i (x : A), + i < length l -> nth_error (list_set i x l) i = Some x. +Proof. + induction l; intros; destruct i; crush; firstorder. +Qed. +Hint Resolve list_set_spec1 : array. + +Lemma list_set_spec2 {A : Type} : + forall l i (x : A) d, + i < length l -> nth i (list_set i x l) d = x. +Proof. + induction l; intros; destruct i; crush; firstorder. +Qed. +Hint Resolve list_set_spec2 : array. + +Lemma list_set_spec3 {A : Type} : + forall l i1 i2 (x : A), + i1 <> i2 -> + nth_error (list_set i1 x l) i2 = nth_error l i2. +Proof. + induction l; intros; destruct i1; destruct i2; crush; firstorder. +Qed. +Hint Resolve list_set_spec3 : array. + +Lemma array_set_wf {A : Type} : + forall l ln i (x : A), + length l = ln -> length (list_set i x l) = ln. +Proof. + induction l; intros; destruct i; auto. + + invert H; crush; auto. +Qed. + +Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := + let l := a.(arr_contents) in + let ln := a.(arr_length) in + let WF := a.(arr_wf) in + @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF). + +Lemma array_set_spec1 {A : Type} : + forall a i (x : A), + i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x. +Proof. + intros. + + rewrite <- a.(arr_wf) in H. + unfold array_set. crush. + eauto with array. +Qed. +Hint Resolve array_set_spec1 : array. + +Lemma array_set_spec2 {A : Type} : + forall a i (x : A) d, + i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x. +Proof. + intros. + + rewrite <- a.(arr_wf) in H. + unfold array_set. crush. + eauto with array. +Qed. +Hint Resolve array_set_spec2 : array. + +Lemma array_set_len {A : Type} : + forall a i (x : A), + a.(arr_length) = (array_set i x a).(arr_length). +Proof. + unfold array_set. crush. +Qed. + +Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A := + nth_error a.(arr_contents) i. + +Lemma array_get_error_equal {A : Type} : + forall (a b : Array A) i, + a.(arr_contents) = b.(arr_contents) -> + array_get_error i a = array_get_error i b. +Proof. + unfold array_get_error. crush. +Qed. + +Lemma array_get_error_bound {A : Type} : + forall (a : Array A) i, + i < a.(arr_length) -> exists x, array_get_error i a = Some x. +Proof. + intros. + + rewrite <- a.(arr_wf) in H. + assert (~ length (arr_contents a) <= i) by lia. + + pose proof (nth_error_None a.(arr_contents) i). + apply not_iff_compat in H1. + apply <- H1 in H0. + + destruct (nth_error (arr_contents a) i) eqn:EQ; try contradiction; eauto. +Qed. + +Lemma array_get_error_set_bound {A : Type} : + forall (a : Array A) i x, + i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x. +Proof. + intros. + + unfold array_get_error. + eauto with array. +Qed. + +Lemma array_gso {A : Type} : + forall (a : Array A) i1 i2 x, + i1 <> i2 -> + array_get_error i2 (array_set i1 x a) = array_get_error i2 a. +Proof. + intros. + + unfold array_get_error. + unfold array_set. + crush. + eauto with array. +Qed. + +Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A := + nth i a.(arr_contents) x. + +Lemma array_get_set_bound {A : Type} : + forall (a : Array A) i x d, + i < a.(arr_length) -> array_get i d (array_set i x a) = x. +Proof. + intros. + + unfold array_get. + eauto with array. +Qed. + +Lemma array_get_get_error {A : Type} : + forall (a : Array A) i x d, + array_get_error i a = Some x -> + array_get i d a = x. +Proof. + intros. + unfold array_get. + unfold array_get_error in H. + auto using nth_error_nth. +Qed. + +(** Tail recursive version of standard library function. *) +Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := + match n with + | O => acc + | S n => list_repeat' (a::acc) a n + end. + +Lemma list_repeat'_len {A : Type} : forall (a : A) n l, + length (list_repeat' l a n) = (n + Datatypes.length l)%nat. +Proof. + induction n; intros; crush; try reflexivity. + + specialize (IHn (a :: l)). + rewrite IHn. + crush. +Qed. + +Lemma list_repeat'_app {A : Type} : forall (a : A) n l, + list_repeat' l a n = list_repeat' [] a n ++ l. +Proof. + induction n; intros; crush; try reflexivity. + + pose proof IHn. + specialize (H (a :: l)). + rewrite H. clear H. + specialize (IHn (a :: nil)). + rewrite IHn. clear IHn. + remember (list_repeat' [] a n) as l0. + + rewrite <- app_assoc. + f_equal. +Qed. + +Lemma list_repeat'_head_tail {A : Type} : forall n (a : A), + a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]. +Proof. + induction n; intros; crush; try reflexivity. + rewrite list_repeat'_app. + + replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]). + 2: { rewrite app_comm_cons. rewrite IHn; auto. + rewrite app_assoc. reflexivity. } + rewrite app_assoc. reflexivity. +Qed. + +Lemma list_repeat'_cons {A : Type} : forall (a : A) n, + list_repeat' [a] a n = a :: list_repeat' [] a n. +Proof. + intros. + + rewrite list_repeat'_head_tail; auto. + apply list_repeat'_app. +Qed. + +Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil. + +Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n. +Proof. + intros. + unfold list_repeat. + rewrite list_repeat'_len. + crush. +Qed. + +Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a', + (forall x x' : A, {x' = x} + {~ x' = x}) -> + In a' (list_repeat a n) -> a' = a. +Proof. + induction n; intros; crush. + + unfold list_repeat in *. + crush. + + rewrite list_repeat'_app in H. + pose proof (X a a'). + destruct H0; auto. + + (* This is actually a degenerate case, not an unprovable goal. *) + pose proof (in_app_or (list_repeat' [] a n) ([a])). + apply H0 in H. invert H. + + - eapply IHn in X; eassumption. + - invert H1; contradiction. +Qed. + +Lemma list_repeat_head_tail {A : Type} : forall n (a : A), + a :: list_repeat a n = list_repeat a n ++ [a]. +Proof. + unfold list_repeat. apply list_repeat'_head_tail. +Qed. + +Lemma list_repeat_cons {A : Type} : forall n (a : A), + list_repeat a (S n) = a :: list_repeat a n. +Proof. + intros. + + unfold list_repeat. + apply list_repeat'_cons. +Qed. + +Lemma list_repeat_lookup {A : Type} : + forall n i (a : A), + i < n -> + nth_error (list_repeat a n) i = Some a. +Proof. + induction n; intros. + + destruct i; crush. + + rewrite list_repeat_cons. + destruct i; crush; firstorder. +Qed. + +Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). + +Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n. +Proof. + unfold list_repeat. crush. apply list_repeat_len. +Qed. + +Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := + match x, y with + | a :: t, b :: t' => f a b :: list_combine f t t' + | _, _ => nil + end. + +Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B), + length (list_combine f x y) = min (length x) (length y). +Proof. + induction x; intros; crush. + + destruct y; crush; auto. +Qed. + +Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C := + make_array (list_combine f x.(arr_contents) y.(arr_contents)). + +Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C), + x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length). +Proof. + intros. + + unfold combine. + unfold make_array. + crush. + + rewrite <- (arr_wf x) in *. + rewrite <- (arr_wf y) in *. + + destruct (arr_contents x); destruct (arr_contents y); crush. + rewrite list_combine_length. + destruct (Min.min_dec (length l) (length l0)); congruence. +Qed. + +Ltac array := + try match goal with + | [ |- context[arr_length (combine _ _ _)] ] => + rewrite combine_length + | [ |- context[length (list_repeat _ _)] ] => + rewrite list_repeat_len + | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] => + unfold array_get_error, arr_repeat + | |- context[nth_error (list_repeat ?x _) _ = Some ?x] => + apply list_repeat_lookup + end. diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v new file mode 100644 index 0000000..8d8788a --- /dev/null +++ b/src/hls/AssocMap.v @@ -0,0 +1,217 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From vericert Require Import Vericertlib ValueInt. +From compcert Require Import Maps. + +Definition reg := positive. + +Module AssocMap := Maps.PTree. + +Module AssocMapExt. + Import AssocMap. + + Hint Resolve elements_correct elements_complete + elements_keys_norepet : assocmap. + Hint Resolve gso gss : assocmap. + + Section Operations. + + Variable A : Type. + + Definition get_default (a : A) (k : reg) (m : t A) : A := + match get k m with + | None => a + | Some v => v + end. + + Fixpoint merge (m1 m2 : t A) : t A := + match m1, m2 with + | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2) + | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2) + | Leaf, _ => m2 + | _, _ => m1 + end. + + Lemma merge_base_1 : + forall am, + merge (empty A) am = am. + Proof. auto. Qed. + Hint Resolve merge_base_1 : assocmap. + + Lemma merge_base_2 : + forall am, + merge am (empty A) = am. + Proof. + unfold merge. + destruct am; trivial. + destruct o; trivial. + Qed. + Hint Resolve merge_base_2 : assocmap. + + Lemma merge_add_assoc : + forall r am am' v, + merge (set r v am) am' = set r v (merge am am'). + Proof. + induction r; intros; destruct am; destruct am'; try (destruct o); simpl; + try rewrite IHr; try reflexivity. + Qed. + Hint Resolve merge_add_assoc : assocmap. + + Lemma merge_correct_1 : + forall am bm k v, + get k am = Some v -> + get k (merge am bm) = Some v. + Proof. + induction am; intros; destruct k; destruct bm; try (destruct o); simpl; + try rewrite gempty in H; try discriminate; try assumption; auto. + Qed. + Hint Resolve merge_correct_1 : assocmap. + + Lemma merge_correct_2 : + forall am bm k v, + get k am = None -> + get k bm = Some v -> + get k (merge am bm) = Some v. + Proof. + induction am; intros; destruct k; destruct bm; try (destruct o); simpl; + try rewrite gempty in H; try discriminate; try assumption; auto. + Qed. + Hint Resolve merge_correct_2 : assocmap. + + Definition merge_fold (am bm : t A) : t A := + fold_right (fun p a => set (fst p) (snd p) a) bm (elements am). + + Lemma add_assoc : + forall (k : elt) (v : A) l bm, + List.In (k, v) l -> + list_norepet (List.map fst l) -> + @get A k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v. + Proof. + induction l; intros. + - contradiction. + - destruct a as [k' v']. + destruct (peq k k'). + + inversion H. inversion H1. inversion H0. subst. + simpl. auto with assocmap. + + inversion H0; subst. apply in_map with (f:=fst) in H1. contradiction. + + + inversion H. inversion H1. inversion H0. subst. simpl. rewrite gso; try assumption. + apply IHl. contradiction. contradiction. + simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption. + Qed. + Hint Resolve add_assoc : assocmap. + + Lemma not_in_assoc : + forall k v l bm, + ~ List.In k (List.map (@fst elt A) l) -> + @get A k bm = Some v -> + get k (fold_right (fun p a => set (fst p) (snd p) a) bm l) = Some v. + Proof. + induction l; intros. + - assumption. + - destruct a as [k' v']. + destruct (peq k k'); subst; + simpl in *; apply Decidable.not_or in H; destruct H. contradiction. + rewrite AssocMap.gso; auto. + Qed. + Hint Resolve not_in_assoc : assocmap. + + Lemma elements_iff : + forall am k, + (exists v, get k am = Some v) <-> + List.In k (List.map (@fst _ A) (elements am)). + Proof. + split; intros. + destruct H. apply elements_correct in H. apply in_map with (f := fst) in H. apply H. + apply list_in_map_inv in H. destruct H. destruct H. subst. + exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing. + rewrite H in H0; assumption. + Qed. + Hint Resolve elements_iff : assocmap. + + Lemma elements_correct' : + forall am k, + ~ (exists v, get k am = Some v) <-> + ~ List.In k (List.map (@fst _ A) (elements am)). + Proof. auto using not_iff_compat with assocmap. Qed. + Hint Resolve elements_correct' : assocmap. + + Lemma elements_correct_none : + forall am k, + get k am = None -> + ~ List.In k (List.map (@fst _ A) (elements am)). + Proof. + intros. apply elements_correct'. unfold not. intros. + destruct H0. rewrite H in H0. discriminate. + Qed. + Hint Resolve elements_correct_none : assocmap. + + Lemma merge_fold_add : + forall k v am bm, + am ! k = Some v -> + (merge_fold am bm) ! k = Some v. + Proof. unfold merge_fold; auto with assocmap. Qed. + Hint Resolve merge_fold_add : assocmap. + + Lemma merge_fold_not_in : + forall k v am bm, + get k am = None -> + get k bm = Some v -> + get k (merge_fold am bm) = Some v. + Proof. intros. apply not_in_assoc; auto with assocmap. Qed. + Hint Resolve merge_fold_not_in : assocmap. + + Lemma merge_fold_base : + forall am, + merge_fold (empty A) am = am. + Proof. auto. Qed. + Hint Resolve merge_fold_base : assocmap. + + End Operations. + +End AssocMapExt. +Import AssocMapExt. + +Definition assocmap := AssocMap.t value. + +Definition find_assocmap (n : nat) : reg -> assocmap -> value := + get_default value (ZToValue 0). + +Definition empty_assocmap : assocmap := AssocMap.empty value. + +Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. + +Ltac unfold_merge := + unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); + rewrite AssocMapExt.merge_base_1. + +Declare Scope assocmap. +Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap. +Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap. +Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap. +Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap. +Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap. + +Local Open Scope assocmap. +Lemma find_get_assocmap : + forall assoc r v, + assoc ! r = Some v -> + assoc # r = v. +Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. diff --git a/src/hls/HTL.v b/src/hls/HTL.v new file mode 100644 index 0000000..620ef14 --- /dev/null +++ b/src/hls/HTL.v @@ -0,0 +1,171 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From Coq Require Import FSets.FMapPositive. +From vericert Require Import Vericertlib ValueInt AssocMap Array. +From vericert Require Verilog. +From compcert Require Events Globalenvs Smallstep Integers Values. +From compcert Require Import Maps. + +(** The purpose of the hardware transfer language (HTL) is to create a more +hardware-like layout that is still similar to the register transfer language +(RTL) that it came from. The main change is that function calls become module +instantiations and that we now describe a state machine instead of a +control-flow graph. *) + +Local Open Scope assocmap. + +Definition reg := positive. +Definition node := positive. + +Definition datapath := PTree.t Verilog.stmnt. +Definition controllogic := PTree.t Verilog.stmnt. + +Definition map_well_formed {A : Type} (m : PTree.t A) : Prop := + forall p0 : positive, + In p0 (map fst (Maps.PTree.elements m)) -> + Z.pos p0 <= Integers.Int.max_unsigned. + +Record module: Type := + mkmodule { + mod_params : list reg; + mod_datapath : datapath; + mod_controllogic : controllogic; + mod_entrypoint : node; + mod_st : reg; + mod_stk : reg; + mod_stk_len : nat; + mod_finish : reg; + mod_return : reg; + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_scldecls : AssocMap.t (option Verilog.io * Verilog.scl_decl); + mod_arrdecls : AssocMap.t (option Verilog.io * Verilog.arr_decl); + mod_wf : (map_well_formed mod_controllogic /\ map_well_formed mod_datapath); + }. + +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + +Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_regs vl' rl') + | _, _ => empty_assocmap + end. + +Definition empty_stack (m : module) : Verilog.assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty Verilog.arr)). + +(** * Operational Semantics *) + +Definition genv := Globalenvs.Genv.t fundef unit. + +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), + stackframe. + +Inductive state : Type := +| State : + forall (stack : list stackframe) + (m : module) + (st : node) + (reg_assoc : Verilog.assocmap_reg) + (arr_assoc : Verilog.assocmap_arr), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. + +Inductive step : genv -> state -> Events.trace -> state -> Prop := +| step_module : + forall g m st sf ctrl data + asr asa + basr1 basa1 nasr1 nasa1 + basr2 basa2 nasr2 nasa2 + asr' asa' + f pstval, + asr!(mod_reset m) = Some (ZToValue 0) -> + asr!(mod_finish m) = Some (ZToValue 0) -> + asr!(m.(mod_st)) = Some (posToValue st) -> + m.(mod_controllogic)!st = Some ctrl -> + m.(mod_datapath)!st = Some data -> + Verilog.stmnt_runp f + (Verilog.mkassociations asr empty_assocmap) + (Verilog.mkassociations asa (empty_stack m)) + ctrl + (Verilog.mkassociations basr1 nasr1) + (Verilog.mkassociations basa1 nasa1) -> + basr1!(m.(mod_st)) = Some (posToValue st) -> + Verilog.stmnt_runp f + (Verilog.mkassociations basr1 nasr1) + (Verilog.mkassociations basa1 nasa1) + data + (Verilog.mkassociations basr2 nasr2) + (Verilog.mkassociations basa2 nasa2) -> + asr' = Verilog.merge_regs nasr2 basr2 -> + asa' = Verilog.merge_arrs nasa2 basa2 -> + asr'!(m.(mod_st)) = Some (posToValue pstval) -> + Z.pos pstval <= Integers.Int.max_unsigned -> + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') +| step_finish : + forall g m st asr asa retval sf, + asr!(m.(mod_finish)) = Some (ZToValue 1) -> + asr!(m.(mod_return)) = Some retval -> + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) +| step_call : + forall g m args res, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set (mod_st m) (posToValue m.(mod_entrypoint)) + (init_regs args m.(mod_params))))) + (empty_stack m)) +| step_return : + forall g m asr asa i r sf pc mst, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). +Hint Constructors step : htl. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + initial_state p (Callstate nil m nil). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + retvali = valueToInt retval -> + final_state (Returnstate nil retval) retvali. + +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v new file mode 100644 index 0000000..68e0293 --- /dev/null +++ b/src/hls/HTLgen.v @@ -0,0 +1,654 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require Import Maps. +From compcert Require Errors Globalenvs Integers. +From compcert Require Import AST RTL. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt Statemonad. + +Hint Resolve AssocMap.gempty : htlh. +Hint Resolve AssocMap.gso : htlh. +Hint Resolve AssocMap.gss : htlh. +Hint Resolve Ple_refl : htlh. +Hint Resolve Ple_succ : htlh. + +Record state: Type := mkstate { + st_st : reg; + st_freshreg: reg; + st_freshstate: node; + st_scldecls: AssocMap.t (option io * scl_decl); + st_arrdecls: AssocMap.t (option io * arr_decl); + st_datapath: datapath; + st_controllogic: controllogic; +}. + +Definition init_state (st : reg) : state := + mkstate st + 1%positive + 1%positive + (AssocMap.empty (option io * scl_decl)) + (AssocMap.empty (option io * arr_decl)) + (AssocMap.empty stmnt) + (AssocMap.empty stmnt). + +Module HTLState <: State. + + Definition st := state. + + Inductive st_incr: state -> state -> Prop := + state_incr_intro: + forall (s1 s2: state), + st_st s1 = st_st s2 -> + Ple s1.(st_freshreg) s2.(st_freshreg) -> + Ple s1.(st_freshstate) s2.(st_freshstate) -> + (forall n, + s1.(st_datapath)!n = None \/ s2.(st_datapath)!n = s1.(st_datapath)!n) -> + (forall n, + s1.(st_controllogic)!n = None + \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> + st_incr s1 s2. + Hint Constructors st_incr : htlh. + + Definition st_prop := st_incr. + Hint Unfold st_prop : htlh. + + Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. + + Lemma st_trans : + forall s1 s2 s3, st_prop s1 s2 -> st_prop s2 s3 -> st_prop s1 s3. + Proof. + intros. inv H. inv H0. apply state_incr_intro; eauto using Ple_trans; intros; try congruence. + - destruct H4 with n; destruct H8 with n; intuition congruence. + - destruct H5 with n; destruct H9 with n; intuition congruence. + Qed. + +End HTLState. +Export HTLState. + +Module HTLMonad := Statemonad(HTLState). +Export HTLMonad. + +Module HTLMonadExtra := Monad.MonadExtra(HTLMonad). +Import HTLMonadExtra. +Export MonadNotation. + +Definition state_goto (st : reg) (n : node) : stmnt := + Vnonblock (Vvar st) (Vlit (posToValue n)). + +Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := + Vnonblock (Vvar st) (Vternary c (posToExpr n1) (posToExpr n2)). + +Definition check_empty_node_datapath: + forall (s: state) (n: node), { s.(st_datapath)!n = None } + { True }. +Proof. + intros. case (s.(st_datapath)!n); tauto. +Defined. + +Definition check_empty_node_controllogic: + forall (s: state) (n: node), { s.(st_controllogic)!n = None } + { True }. +Proof. + intros. case (s.(st_controllogic)!n); tauto. +Defined. + +Lemma add_instr_state_incr : + forall s n n' st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Lemma declare_reg_state_incr : + forall i s r sz, + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)). +Proof. auto with htlh. Qed. + +Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := + fun s => OK tt (mkstate + s.(st_st) + s.(st_freshreg) + s.(st_freshstate) + (AssocMap.set r (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + s.(st_datapath) + s.(st_controllogic)) + (declare_reg_state_incr i s r sz). + +Definition add_instr (n : node) (n' : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n (state_goto s.(st_st) n') s.(st_controllogic))) + (add_instr_state_incr s n n' st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Lemma add_instr_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_instr_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n st s.(st_datapath)) + (AssocMap.set n Vskip s.(st_controllogic))) + (add_instr_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Lemma add_node_skip_state_incr : + forall s n st, + (st_datapath s)!n = None -> + (st_controllogic s)!n = None -> + st_incr s + (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))). +Proof. + constructor; intros; + try (simpl; destruct (peq n n0); subst); + auto with htlh. +Qed. + +Definition add_node_skip (n : node) (st : stmnt) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left STM, left TRANS => + OK tt (mkstate + s.(st_st) + s.(st_freshreg) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip s.(st_datapath)) + (AssocMap.set n st s.(st_controllogic))) + (add_node_skip_state_incr s n st STM TRANS) + | _, _ => Error (Errors.msg "HTL.add_instr") + end. + +Definition nonblock (dst : reg) (e : expr) := Vnonblock (Vvar dst) e. +Definition block (dst : reg) (e : expr) := Vblock (Vvar dst) e. + +Definition bop (op : binop) (r1 r2 : reg) : expr := + Vbinop op (Vvar r1) (Vvar r2). + +Definition boplit (op : binop) (r : reg) (l : Integers.int) : expr := + Vbinop op (Vvar r) (Vlit (intToValue l)). + +Definition boplitz (op: binop) (r: reg) (l: Z) : expr := + Vbinop op (Vvar r) (Vlit (ZToValue l)). + +Definition translate_comparison (c : Integers.comparison) (args : list reg) : mon expr := + match c, args with + | Integers.Ceq, r1::r2::nil => ret (bop Veq r1 r2) + | Integers.Cne, r1::r2::nil => ret (bop Vne r1 r2) + | Integers.Clt, r1::r2::nil => ret (bop Vlt r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgt r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vle r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vge r1 r2) + | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_imm (c : Integers.comparison) (args : list reg) (i: Integers.int) + : mon expr := + match c, args with + | Integers.Ceq, r1::nil => ret (boplit Veq r1 i) + | Integers.Cne, r1::nil => ret (boplit Vne r1 i) + | Integers.Clt, r1::nil => ret (boplit Vlt r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgt r1 i) + | Integers.Cle, r1::nil => ret (boplit Vle r1 i) + | Integers.Cge, r1::nil => ret (boplit Vge r1 i) + | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + end. + +Definition translate_comparisonu (c : Integers.comparison) (args : list reg) : mon expr := + match c, args with + | Integers.Clt, r1::r2::nil => ret (bop Vltu r1 r2) + | Integers.Cgt, r1::r2::nil => ret (bop Vgtu r1 r2) + | Integers.Cle, r1::r2::nil => ret (bop Vleu r1 r2) + | Integers.Cge, r1::r2::nil => ret (bop Vgeu r1 r2) + | _, _ => error (Errors.msg "Htlgen: comparison instruction not implemented: other") + end. + +Definition translate_comparison_immu (c : Integers.comparison) (args : list reg) (i: Integers.int) + : mon expr := + match c, args with + | Integers.Clt, r1::nil => ret (boplit Vltu r1 i) + | Integers.Cgt, r1::nil => ret (boplit Vgtu r1 i) + | Integers.Cle, r1::nil => ret (boplit Vleu r1 i) + | Integers.Cge, r1::nil => ret (boplit Vgeu r1 i) + | _, _ => error (Errors.msg "Htlgen: comparison_imm instruction not implemented: other") + end. + +Definition translate_condition (c : Op.condition) (args : list reg) : mon expr := + match c, args with + | Op.Ccomp c, _ => translate_comparison c args + | Op.Ccompu c, _ => translate_comparisonu c args + | Op.Ccompimm c i, _ => translate_comparison_imm c args i + | Op.Ccompuimm c i, _ => translate_comparison_immu c args i + | Op.Cmaskzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmaskzero") + | Op.Cmasknotzero n, _ => error (Errors.msg "Htlgen: condition instruction not implemented: Cmasknotzero") + | _, _ => error (Errors.msg "Htlgen: condition instruction not implemented: other") + end. + +Definition check_address_parameter_signed (p : Z) : bool := + Z.leb Integers.Ptrofs.min_signed p + && Z.leb p Integers.Ptrofs.max_signed. + +Definition check_address_parameter_unsigned (p : Z) : bool := + Z.leb p Integers.Ptrofs.max_unsigned. + +Definition translate_eff_addressing (a: Op.addressing) (args: list reg) : mon expr := + match a, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (boplitz Vadd r1 off) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed): address out of bounds") + | Op.Ascaled scale offset, r1::nil => + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (boplitz Vmul r1 scale) (Vlit (ZToValue offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ascaled): address out of bounds") + | Op.Aindexed2 offset, r1::r2::nil => + if (check_address_parameter_signed offset) + then ret (Vbinop Vadd (bop Vadd r1 r2) (Vlit (ZToValue offset))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2): address out of bounds") + | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vbinop Vadd (Vvar r1) (Vbinop Vadd (boplitz Vmul r2 scale) (Vlit (ZToValue offset)))) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Aindexed2scaled): address out of bounds") + | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vlit (ZToValue a)) + else error (Errors.msg "Veriloggen: translate_eff_addressing (Ainstack): address out of bounds") + | _, _ => error (Errors.msg "Veriloggen: translate_eff_addressing unsuported addressing") + end. + +(** Translate an instruction to a statement. FIX mulhs mulhu *) +Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := + match op, args with + | Op.Omove, r::nil => ret (Vvar r) + | Op.Ointconst n, _ => ret (Vlit (intToValue n)) + | Op.Oneg, r::nil => ret (Vunop Vneg (Vvar r)) + | Op.Osub, r1::r2::nil => ret (bop Vsub r1 r2) + | Op.Omul, r1::r2::nil => ret (bop Vmul r1 r2) + | Op.Omulimm n, r::nil => ret (boplit Vmul r n) + | Op.Omulhs, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhs") + | Op.Omulhu, r1::r2::nil => error (Errors.msg "Htlgen: Instruction not implemented: mulhu") + | Op.Odiv, r1::r2::nil => ret (bop Vdiv r1 r2) + | Op.Odivu, r1::r2::nil => ret (bop Vdivu r1 r2) + | Op.Omod, r1::r2::nil => ret (bop Vmod r1 r2) + | Op.Omodu, r1::r2::nil => ret (bop Vmodu r1 r2) + | Op.Oand, r1::r2::nil => ret (bop Vand r1 r2) + | Op.Oandimm n, r::nil => ret (boplit Vand r n) + | Op.Oor, r1::r2::nil => ret (bop Vor r1 r2) + | Op.Oorimm n, r::nil => ret (boplit Vor r n) + | Op.Oxor, r1::r2::nil => ret (bop Vxor r1 r2) + | Op.Oxorimm n, r::nil => ret (boplit Vxor r n) + | Op.Onot, r::nil => ret (Vunop Vnot (Vvar r)) + | Op.Oshl, r1::r2::nil => ret (bop Vshl r1 r2) + | Op.Oshlimm n, r::nil => ret (boplit Vshl r n) + | Op.Oshr, r1::r2::nil => ret (bop Vshr r1 r2) + | Op.Oshrimm n, r::nil => ret (boplit Vshr r n) + | Op.Oshrximm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Oshrximm") + (*ret (Vbinop Vdiv (Vvar r) + (Vbinop Vshl (Vlit (ZToValue 1)) + (Vlit (intToValue n))))*) + | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) + | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) + | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) + | Op.Ocmp c, _ => translate_condition c args + | Op.Osel c AST.Tint, r1::r2::rl => + do tc <- translate_condition c rl; + ret (Vternary tc (Vvar r1) (Vvar r2)) + | Op.Olea a, _ => translate_eff_addressing a args + | _, _ => error (Errors.msg "Htlgen: Instruction not implemented: other") + end. + +Lemma add_branch_instr_state_incr: + forall s e n n1 n2, + (st_datapath s) ! n = None -> + (st_controllogic s) ! n = None -> + st_incr s (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))). +Proof. + intros. apply state_incr_intro; simpl; + try (intros; destruct (peq n0 n); subst); + auto with htlh. +Qed. + +Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := + fun s => + match check_empty_node_datapath s n, check_empty_node_controllogic s n with + | left NSTM, left NTRANS => + OK tt (mkstate + s.(st_st) + (st_freshreg s) + (st_freshstate s) + s.(st_scldecls) + s.(st_arrdecls) + (AssocMap.set n Vskip (st_datapath s)) + (AssocMap.set n (state_cond s.(st_st) e n1 n2) (st_controllogic s))) + (add_branch_instr_state_incr s e n n1 n2 NSTM NTRANS) + | _, _ => Error (Errors.msg "Htlgen: add_branch_instr") + end. + +Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) + (args : list reg) (stack : reg) : mon expr := + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => + if (check_address_parameter_signed off) + then ret (Vvari stack (Vbinop Vdivu (boplitz Vadd r1 off) (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + if (check_address_parameter_signed scale) && (check_address_parameter_signed offset) + then ret (Vvari stack + (Vbinop Vdivu + (Vbinop Vadd (boplitz Vadd r1 offset) (boplitz Vmul r2 scale)) + (Vlit (ZToValue 4)))) + else error (Errors.msg "HTLgen: translate_arr_access address out of bounds") + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + let a := Integers.Ptrofs.unsigned a in + if (check_address_parameter_unsigned a) + then ret (Vvari stack (Vlit (ZToValue (a / 4)))) + else error (Errors.msg "HTLgen: eff_addressing out of bounds stack offset") + | _, _, _ => error (Errors.msg "HTLgen: translate_arr_access unsuported addressing") + end. + +Fixpoint enumerate (i : nat) (ns : list node) {struct ns} : list (nat * node) := + match ns with + | n :: ns' => (i, n) :: enumerate (i+1) ns' + | nil => nil + end. + +Definition tbl_to_case_expr (st : reg) (ns : list node) : list (expr * stmnt) := + List.map (fun a => match a with + (i, n) => (Vlit (natToValue i), Vnonblock (Vvar st) (Vlit (posToValue n))) + end) + (enumerate 0 ns). + +Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := + match ni with + (n, i) => + match i with + | Inop n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + add_instr n n' Vskip + else error (Errors.msg "State is larger than 2^32.") + | Iop op args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do instr <- translate_instr op args; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst instr) + else error (Errors.msg "State is larger than 2^32.") + | Iload mem addr args dst n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do src <- translate_arr_access mem addr args stack; + do _ <- declare_reg None dst 32; + add_instr n n' (nonblock dst src) + else error (Errors.msg "State is larger than 2^32.") + | Istore mem addr args src n' => + if Z.leb (Z.pos n') Integers.Int.max_unsigned then + do dst <- translate_arr_access mem addr args stack; + add_instr n n' (Vnonblock dst (Vvar src)) (* TODO: Could juse use add_instr? reg exists. *) + else error (Errors.msg "State is larger than 2^32.") + | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") + | Itailcall _ _ _ => error (Errors.msg "Tailcalls are not implemented.") + | Ibuiltin _ _ _ _ => error (Errors.msg "Builtin functions not implemented.") + | Icond cond args n1 n2 => + if Z.leb (Z.pos n1) Integers.Int.max_unsigned && Z.leb (Z.pos n2) Integers.Int.max_unsigned then + do e <- translate_condition cond args; + add_branch_instr e n n1 n2 + else error (Errors.msg "State is larger than 2^32.") + | Ijumptable r tbl => + (*do s <- get; + add_node_skip n (Vcase (Vvar r) (tbl_to_case_expr s.(st_st) tbl) (Some Vskip))*) + error (Errors.msg "Ijumptable: Case statement not supported.") + | Ireturn r => + match r with + | Some r' => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r'))) + | None => + add_instr_skip n (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vlit (ZToValue 0%Z)))) + end + end + end. + +Lemma create_reg_state_incr: + forall s sz i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + s.(st_arrdecls) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_reg (i : option io) (sz : nat) : mon reg := + fun s => let r := s.(st_freshreg) in + OK r (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + (AssocMap.set s.(st_freshreg) (i, VScalar sz) s.(st_scldecls)) + (st_arrdecls s) + (st_datapath s) + (st_controllogic s)) + (create_reg_state_incr s sz i). + +Lemma create_arr_state_incr: + forall s sz ln i, + st_incr s (mkstate + s.(st_st) + (Pos.succ (st_freshreg s)) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)). +Proof. constructor; simpl; auto with htlh. Qed. + +Definition create_arr (i : option io) (sz : nat) (ln : nat) : mon (reg * nat) := + fun s => let r := s.(st_freshreg) in + OK (r, ln) (mkstate + s.(st_st) + (Pos.succ r) + (st_freshstate s) + s.(st_scldecls) + (AssocMap.set s.(st_freshreg) (i, VArray sz ln) s.(st_arrdecls)) + (st_datapath s) + (st_controllogic s)) + (create_arr_state_incr s sz ln i). + +Definition stack_correct (sz : Z) : bool := + (0 <=? sz) && (sz Pos.max m pc) m 1%positive. + +Lemma max_pc_map_sound: + forall m pc i, m!pc = Some i -> Ple pc (max_pc_map m). +Proof. + intros until i. unfold max_pc_function. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. xomega. + apply Ple_trans with a. auto. xomega. +Qed. + +Lemma max_pc_wf : + forall m, Z.pos (max_pc_map m) <= Integers.Int.max_unsigned -> + map_well_formed m. +Proof. + unfold map_well_formed. intros. + exploit list_in_map_inv. eassumption. intros [x [A B]]. destruct x. + apply Maps.PTree.elements_complete in B. apply max_pc_map_sound in B. + unfold Ple in B. apply Pos2Z.pos_le_pos in B. subst. + simplify. transitivity (Z.pos (max_pc_map m)); eauto. +Qed. + +Definition transf_module (f: function) : mon module := + if stack_correct f.(fn_stacksize) then + do fin <- create_reg (Some Voutput) 1; + do rtrn <- create_reg (Some Voutput) 32; + do (stack, stack_len) <- create_arr None 32 (Z.to_nat (f.(fn_stacksize) / 4)); + do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code)); + do _ <- collectlist (fun r => declare_reg (Some Vinput) r 32) f.(RTL.fn_params); + do start <- create_reg (Some Vinput) 1; + do rst <- create_reg (Some Vinput) 1; + do clk <- create_reg (Some Vinput) 1; + do current_state <- get; + match zle (Z.pos (max_pc_map current_state.(st_datapath))) Integers.Int.max_unsigned, + zle (Z.pos (max_pc_map current_state.(st_controllogic))) Integers.Int.max_unsigned with + | left LEDATA, left LECTRL => + ret (mkmodule + f.(RTL.fn_params) + current_state.(st_datapath) + current_state.(st_controllogic) + f.(fn_entrypoint) + current_state.(st_st) + stack + stack_len + fin + rtrn + start + rst + clk + current_state.(st_scldecls) + current_state.(st_arrdecls) + (conj (max_pc_wf _ LECTRL) (max_pc_wf _ LEDATA))) + | _, _ => error (Errors.msg "More than 2^32 states.") + end + else error (Errors.msg "Stack size misalignment."). + +Definition max_state (f: function) : state := + let st := Pos.succ (max_reg_function f) in + mkstate st + (Pos.succ st) + (Pos.succ (max_pc_function f)) + (AssocMap.set st (None, VScalar 32) (st_scldecls (init_state st))) + (st_arrdecls (init_state st)) + (st_datapath (init_state st)) + (st_controllogic (init_state st)). + +Definition transl_module (f : function) : Errors.res module := + run_mon (max_state f) (transf_module f). + +Definition transl_fundef := transf_partial_fundef transl_module. + +(* Definition transl_program (p : RTL.program) := transform_partial_program transl_fundef p. *) + +(*Definition transl_main_fundef f : Errors.res HTL.fundef := + match f with + | Internal f => transl_fundef (Internal f) + | External f => Errors.Error (Errors.msg "Could not find internal main function") + end. + +(** Translation of a whole program. *) + +Definition transl_program (p: RTL.program) : Errors.res HTL.program := + transform_partial_program2 (fun i f => if Pos.eqb p.(AST.prog_main) i + then transl_fundef f + else transl_main_fundef f) + (fun i v => Errors.OK v) p. +*) + +Definition main_is_internal (p : RTL.program) : bool := + let ge := Globalenvs.Genv.globalenv p in + match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with + | Some b => + match Globalenvs.Genv.find_funct_ptr ge b with + | Some (AST.Internal _) => true + | _ => false + end + | _ => false + end. + +Definition transl_program (p : RTL.program) : Errors.res HTL.program := + if main_is_internal p + then transform_partial_program transl_fundef p + else Errors.Error (Errors.msg "Main function is not Internal."). diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v new file mode 100644 index 0000000..22f8f57 --- /dev/null +++ b/src/hls/HTLgenproof.v @@ -0,0 +1,2683 @@ + (* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require RTL Registers AST. +From compcert Require Import Integers Globalenvs Memory Linking. +From vericert Require Import Vericertlib HTLgenspec HTLgen ValueInt AssocMap Array IntegerExtra ZExtra. +From vericert Require HTL Verilog. + +Require Import Lia. + +Local Open Scope assocmap. + +Hint Resolve Smallstep.forward_simulation_plus : htlproof. +Hint Resolve AssocMap.gss : htlproof. +Hint Resolve AssocMap.gso : htlproof. + +Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. + +Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := + match_assocmap : forall f rs am, + (forall r, Ple r (RTL.max_reg_function f) -> + val_value_lessdef (Registers.Regmap.get r rs) am#r) -> + match_assocmaps f rs am. +Hint Constructors match_assocmaps : htlproof. + +Definition state_st_wf (m : HTL.module) (s : HTL.state) := + forall st asa asr res, + s = HTL.State res m st asa asr -> + asa!(m.(HTL.mod_st)) = Some (posToValue st). +Hint Unfold state_st_wf : htlproof. + +Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : + Verilog.assocmap_arr -> Prop := +| match_arr : forall asa stack, + asa ! (m.(HTL.mod_stk)) = Some stack /\ + stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ + (forall ptr, + 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> + opt_val_value_lessdef (Mem.loadv AST.Mint32 mem + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr)))) + (Option.default (NToValue 0) + (Option.join (array_get_error (Z.to_nat ptr) stack)))) -> + match_arrs m f sp mem asa. + +Definition stack_based (v : Values.val) (sp : Values.block) : Prop := + match v with + | Values.Vptr sp' off => sp' = sp + | _ => True + end. + +Definition reg_stack_based_pointers (sp : Values.block) (rs : Registers.Regmap.t Values.val) : Prop := + forall r, stack_based (Registers.Regmap.get r rs) sp. + +Definition arr_stack_based_pointers (spb : Values.block) (m : mem) (stack_length : Z) + (sp : Values.val) : Prop := + forall ptr, + 0 <= ptr < (stack_length / 4) -> + stack_based (Option.default + Values.Vundef + (Mem.loadv AST.Mint32 m + (Values.Val.offset_ptr sp (Integers.Ptrofs.repr (4 * ptr))))) + spb. + +Definition stack_bounds (sp : Values.val) (hi : Z) (m : mem) : Prop := + forall ptr v, + hi <= ptr <= Integers.Ptrofs.max_unsigned -> + Z.modulo ptr 4 = 0 -> + Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) = None /\ + Mem.storev AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr )) v = None. + +Inductive match_frames : list RTL.stackframe -> list HTL.stackframe -> Prop := +| match_frames_nil : + match_frames nil nil. + +Inductive match_constants : HTL.module -> assocmap -> Prop := + match_constant : + forall m asr, + asr!(HTL.mod_reset m) = Some (ZToValue 0) -> + asr!(HTL.mod_finish m) = Some (ZToValue 0) -> + match_constants m asr. + +Inductive match_states : RTL.state -> HTL.state -> Prop := +| match_state : forall asa asr sf f sp sp' rs mem m st res + (MASSOC : match_assocmaps f rs asr) + (TF : tr_module f m) + (WF : state_st_wf m (HTL.State res m st asr asa)) + (MF : match_frames sf res) + (MARR : match_arrs m f sp mem asa) + (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) + (RSBP : reg_stack_based_pointers sp' rs) + (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) + (CONST : match_constants m asr), + match_states (RTL.State sf f sp st rs mem) + (HTL.State res m st asr asa) +| match_returnstate : + forall + v v' stack mem res + (MF : match_frames stack res), + val_value_lessdef v v' -> + match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v') +| match_initial_call : + forall f m m0 + (TF : tr_module f m), + match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). +Hint Constructors match_states : htlproof. + +Definition match_prog (p: RTL.program) (tp: HTL.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\ + main_is_internal p = true. + +Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program): + TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2). +Proof. + red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2]. + apply link_prog_inv in H. + + unfold match_prog in *. + unfold main_is_internal in *. simplify. repeat (unfold_match H4). + repeat (unfold_match H3). simplify. + subst. rewrite H0 in *. specialize (H (AST.prog_main p2)). + exploit H. + apply Genv.find_def_symbol. exists b. split. + assumption. apply Genv.find_funct_ptr_iff. eassumption. + apply Genv.find_def_symbol. exists b0. split. + assumption. apply Genv.find_funct_ptr_iff. eassumption. + intros. inv H3. inv H5. destruct H6. inv H5. +Qed. + +Definition match_prog' (p: RTL.program) (tp: HTL.program) := + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. + +Lemma match_prog_matches : + forall p tp, match_prog p tp -> match_prog' p tp. +Proof. unfold match_prog. tauto. Qed. + +Lemma transf_program_match: + forall p tp, HTLgen.transl_program p = Errors.OK tp -> match_prog p tp. +Proof. + intros. unfold transl_program in H. + destruct (main_is_internal p) eqn:?; try discriminate. + unfold match_prog. split. + apply Linking.match_transform_partial_program; auto. + assumption. +Qed. + +Lemma regs_lessdef_add_greater : + forall f rs1 rs2 n v, + Plt (RTL.max_reg_function f) n -> + match_assocmaps f rs1 rs2 -> + match_assocmaps f rs1 (AssocMap.set n v rs2). +Proof. + inversion 2; subst. + intros. constructor. + intros. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso. eauto. + apply Pos.le_lt_trans with _ _ n in H2. + unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. +Qed. +Hint Resolve regs_lessdef_add_greater : htlproof. + +Lemma regs_lessdef_add_match : + forall f rs am r v v', + val_value_lessdef v v' -> + match_assocmaps f rs am -> + match_assocmaps f (Registers.Regmap.set r v rs) (AssocMap.set r v' am). +Proof. + inversion 2; subst. + constructor. intros. + destruct (peq r0 r); subst. + rewrite Registers.Regmap.gss. + unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gss. assumption. + + rewrite Registers.Regmap.gso; try assumption. + unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite AssocMap.gso; eauto. +Qed. +Hint Resolve regs_lessdef_add_match : htlproof. + +Lemma list_combine_none : + forall n l, + length l = n -> + list_combine Verilog.merge_cell (list_repeat None n) l = l. +Proof. + induction n; intros; crush. + - symmetry. apply length_zero_iff_nil. auto. + - destruct l; crush. + rewrite list_repeat_cons. + crush. f_equal. + eauto. +Qed. + +Lemma combine_none : + forall n a, + a.(arr_length) = n -> + arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. +Proof. + intros. + unfold combine. + crush. + + rewrite <- (arr_wf a) in H. + apply list_combine_none. + assumption. +Qed. + +Lemma list_combine_lookup_first : + forall l1 l2 n, + length l1 = length l2 -> + nth_error l1 n = Some None -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. +Proof. + induction l1; intros; crush. + + rewrite nth_error_nil in H0. + discriminate. + + destruct l2 eqn:EQl2. crush. + simpl in H. invert H. + destruct n; simpl in *. + invert H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_first : + forall a1 a2 n, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some None -> + array_get_error n (combine Verilog.merge_cell a1 a2) = array_get_error n a2. +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_first; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Lemma list_combine_lookup_second : + forall l1 l2 n x, + length l1 = length l2 -> + nth_error l1 n = Some (Some x) -> + nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). +Proof. + induction l1; intros; crush; auto. + + destruct l2 eqn:EQl2. crush. + simpl in H. invert H. + destruct n; simpl in *. + invert H0. simpl. reflexivity. + eauto. +Qed. + +Lemma combine_lookup_second : + forall a1 a2 n x, + a1.(arr_length) = a2.(arr_length) -> + array_get_error n a1 = Some (Some x) -> + array_get_error n (combine Verilog.merge_cell a1 a2) = Some (Some x). +Proof. + intros. + + unfold array_get_error in *. + apply list_combine_lookup_second; eauto. + rewrite a1.(arr_wf). rewrite a2.(arr_wf). + assumption. +Qed. + +Ltac inv_state := + match goal with + MSTATE : match_states _ _ |- _ => + inversion MSTATE; + match goal with + TF : tr_module _ _ |- _ => + inversion TF; + match goal with + TC : forall _ _, + Maps.PTree.get _ _ = Some _ -> tr_code _ _ _ _ _ _ _ _ _, + H : Maps.PTree.get _ _ = Some _ |- _ => + apply TC in H; inversion H; + match goal with + TI : context[tr_instr] |- _ => + inversion TI + end + end + end +end; subst. + +Ltac unfold_func H := + match type of H with + | ?f = _ => unfold f in H; repeat (unfold_match H) + | ?f _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ _ = _ => unfold f in H; repeat (unfold_match H) + | ?f _ _ _ _ = _ => unfold f in H; repeat (unfold_match H) + end. + +Lemma init_reg_assoc_empty : + forall f l, + match_assocmaps f (RTL.init_regs nil l) (HTL.init_regs nil l). +Proof. + induction l; simpl; constructor; intros. + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. + + - rewrite Registers.Regmap.gi. unfold find_assocmap. + unfold AssocMapExt.get_default. rewrite AssocMap.gempty. + constructor. +Qed. + +Lemma arr_lookup_some: + forall (z : Z) (r0 : Registers.reg) (r : Verilog.reg) (asr : assocmap) (asa : Verilog.assocmap_arr) + (stack : Array (option value)) (H5 : asa ! r = Some stack) n, + exists x, Verilog.arr_assocmap_lookup asa r n = Some x. +Proof. + intros z r0 r asr asa stack H5 n. + eexists. + unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. +Qed. +Hint Resolve arr_lookup_some : htlproof. + +Section CORRECTNESS. + + Variable prog : RTL.program. + Variable tprog : HTL.program. + + Hypothesis TRANSL : match_prog prog tprog. + + Lemma TRANSL' : + Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog. + Proof. intros; apply match_prog_matches; assumption. Qed. + + Let ge : RTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : HTL.genv := Globalenvs.Genv.globalenv tprog. + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof. intros. eapply (Genv.find_symbol_match TRANSL'). Qed. + + Lemma function_ptr_translated: + forall (b: Values.block) (f: RTL.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. + Proof. + intros. exploit (Genv.find_funct_ptr_match TRANSL'); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma functions_translated: + forall (v: Values.val) (f: RTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf. + Proof. + intros. exploit (Genv.find_funct_match TRANSL'); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof + (Genv.senv_transf_partial TRANSL'). + Hint Resolve senv_preserved : htlproof. + + Lemma ptrofs_inj : + forall a b, + Ptrofs.unsigned a = Ptrofs.unsigned b -> a = b. + Proof. + intros. rewrite <- Ptrofs.repr_unsigned. symmetry. rewrite <- Ptrofs.repr_unsigned. + rewrite H. auto. + Qed. + + Lemma op_stack_based : + forall F V sp v m args rs op ge pc' res0 pc f e fin rtrn st stk, + tr_instr fin rtrn st stk (RTL.Iop op args res0 pc') + (Verilog.Vnonblock (Verilog.Vvar res0) e) + (state_goto st pc') -> + reg_stack_based_pointers sp rs -> + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> + @Op.eval_operation F V ge (Values.Vptr sp Ptrofs.zero) op + (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> + stack_based v sp. + Proof. + Ltac solve_no_ptr := + match goal with + | H: reg_stack_based_pointers ?sp ?rs |- stack_based (Registers.Regmap.get ?r ?rs) _ => + solve [apply H] + | H1: reg_stack_based_pointers ?sp ?rs, H2: Registers.Regmap.get _ _ = Values.Vptr ?b ?i + |- context[Values.Vptr ?b _] => + let H := fresh "H" in + assert (H: stack_based (Values.Vptr b i) sp) by (rewrite <- H2; apply H1); simplify; solve [auto] + | |- context[Registers.Regmap.get ?lr ?lrs] => + destruct (Registers.Regmap.get lr lrs) eqn:?; simplify; auto + | |- stack_based (?f _) _ => unfold f + | |- stack_based (?f _ _) _ => unfold f + | |- stack_based (?f _ _ _) _ => unfold f + | |- stack_based (?f _ _ _ _) _ => unfold f + | H: ?f _ _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H); inv H + | H: ?f _ _ _ _ _ _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H); inv H + | H: map (fun r : positive => Registers.Regmap.get r _) ?args = _ |- _ => + destruct args; inv H + | |- context[if ?c then _ else _] => destruct c; try discriminate + | H: match _ with _ => _ end = Some _ |- _ => repeat (unfold_match H) + | H: match _ with _ => _ end = OK _ _ _ |- _ => repeat (unfold_match H) + | |- context[match ?g with _ => _ end] => destruct g; try discriminate + | |- _ => simplify; solve [auto] + end. + intros F V sp v m args rs op g pc' res0 pc f e fin rtrn st stk INSTR RSBP SEL EVAL. + inv INSTR. unfold translate_instr in H5. + unfold_match H5; repeat (unfold_match H5); repeat (simplify; solve_no_ptr). + Qed. + + Lemma int_inj : + forall x y, + Int.unsigned x = Int.unsigned y -> + x = y. + Proof. + intros. rewrite <- Int.repr_unsigned at 1. rewrite <- Int.repr_unsigned. + rewrite <- H. trivial. + Qed. + + Ltac eval_correct_tac := + match goal with + | |- context[valueToPtr] => unfold valueToPtr + | |- context[valueToInt] => unfold valueToInt + | |- context[bop] => unfold bop + | H : context[bop] |- _ => unfold bop in H + | |- context[boplit] => unfold boplit + | H : context[boplit] |- _ => unfold boplit in H + | |- context[boplitz] => unfold boplitz + | H : context[boplitz] |- _ => unfold boplitz in H + | |- val_value_lessdef Values.Vundef _ => solve [constructor] + | H : val_value_lessdef _ _ |- val_value_lessdef (Values.Vint _) _ => constructor; inv H + | |- val_value_lessdef (Values.Vint _) _ => constructor; auto + | H : ret _ _ = OK _ _ _ |- _ => inv H + | H : context[RTL.max_reg_function ?f] + |- context[_ (Registers.Regmap.get ?r ?rs) (Registers.Regmap.get ?r0 ?rs)] => + let HPle1 := fresh "HPle" in + let HPle2 := fresh "HPle" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle1; apply H in HPle2; eexists; split; + [econstructor; eauto; constructor; trivial | inv HPle1; inv HPle2; try (constructor; auto)] + | H : context[RTL.max_reg_function ?f] + |- context[_ (Registers.Regmap.get ?r ?rs) _] => + let HPle1 := fresh "HPle" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle1; eexists; split; + [econstructor; eauto; constructor; trivial | inv HPle1; try (constructor; auto)] + | H : _ :: _ = _ :: _ |- _ => inv H + | |- context[match ?d with _ => _ end] => destruct d eqn:?; try discriminate + | H : match ?d with _ => _ end = _ |- _ => repeat unfold_match H + | H : match ?d with _ => _ end _ = _ |- _ => repeat unfold_match H + | |- Verilog.expr_runp _ _ _ _ _ => econstructor + | |- val_value_lessdef (?f _ _) _ => unfold f + | |- val_value_lessdef (?f _) _ => unfold f + | H : ?f (Registers.Regmap.get _ _) _ = Some _ |- _ => + unfold f in H; repeat (unfold_match H) + | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, H2 : val_value_lessdef (Registers.Regmap.get ?r ?rs) _ + |- _ => rewrite H1 in H2; inv H2 + | |- _ => eexists; split; try constructor; solve [eauto] + | H : context[RTL.max_reg_function ?f] |- context[_ (Verilog.Vvar ?r) (Verilog.Vvar ?r0)] => + let HPle1 := fresh "H" in + let HPle2 := fresh "H" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + assert (HPle2 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle1; apply H in HPle2; eexists; split; try constructor; eauto + | H : context[RTL.max_reg_function ?f] |- context[Verilog.Vvar ?r] => + let HPle := fresh "H" in + assert (HPle : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H in HPle; eexists; split; try constructor; eauto + | |- context[if ?c then _ else _] => destruct c eqn:?; try discriminate + | H : ?b = _ |- _ = boolToValue ?b => rewrite H + end. + Ltac inv_lessdef := lazymatch goal with + | H2 : context[RTL.max_reg_function ?f], + H : Registers.Regmap.get ?r ?rs = _, + H1 : Registers.Regmap.get ?r0 ?rs = _ |- _ => + let HPle1 := fresh "HPle" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H2 in HPle1; inv HPle1; + let HPle2 := fresh "HPle" in + assert (HPle2 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H2 in HPle2; inv HPle2 + | H2 : context[RTL.max_reg_function ?f], H : Registers.Regmap.get ?r ?rs = _ |- _ => + let HPle1 := fresh "HPle" in + assert (HPle1 : Ple r (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto); + apply H2 in HPle1; inv HPle1 + end. + Ltac solve_cond := + match goal with + | H : context[match _ with _ => _ end] |- _ => repeat (unfold_merge H) + | H : ?f = _ |- context[boolToValue ?f] => rewrite H; solve [auto] + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vint _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ => + rewrite H2 in H; discriminate + | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vtrue |- _ => + rewrite H2 in H; discriminate + | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vfalse |- _ => + rewrite H2 in H; discriminate + | H : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _ |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vtrue |- _ => + rewrite H2 in H; discriminate + | H : Values.Vundef = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vfalse |- _ => + rewrite H2 in H; discriminate + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vundef |- _ => + rewrite H2 in H; discriminate + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vtrue |- _ => + rewrite H2 in H; discriminate + | H : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H2 : Registers.Regmap.get ?r ?rs = Values.Vfalse |- _ => + rewrite H2 in H; discriminate + | |- context[val_value_lessdef Values.Vundef _] => + econstructor; split; econstructor; econstructor; auto; solve [constructor] + | H1 : Registers.Regmap.get ?r ?rs = Values.Vint _, + H2 : Values.Vint _ = Registers.Regmap.get ?r ?rs, + H3 : Registers.Regmap.get ?r0 ?rs = Values.Vint _, + H4 : Values.Vint _ = Registers.Regmap.get ?r0 ?rs|- _ => + rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor + | H1 : Registers.Regmap.get ?r ?rs = Values.Vptr _ _, + H2 : Values.Vptr _ _ = Registers.Regmap.get ?r ?rs, + H3 : Registers.Regmap.get ?r0 ?rs = Values.Vptr _ _, + H4 : Values.Vptr _ _ = Registers.Regmap.get ?r0 ?rs|- _ => + rewrite H1 in H2; rewrite H3 in H4; inv H2; inv H4; unfold valueToInt in *; constructor; + unfold Ptrofs.ltu, Int.ltu in *; unfold Ptrofs.of_int in *; + repeat (rewrite Ptrofs.unsigned_repr in *; auto using Int.unsigned_range_2) + | H : _ :: _ = _ :: _ |- _ => inv H + | H : ret _ _ = OK _ _ _ |- _ => inv H + | |- _ => + eexists; split; [ econstructor; econstructor; auto + | simplify; inv_lessdef; repeat (unfold valueToPtr, valueToInt in *; solve_cond); + unfold valueToPtr in * + ] + end. + + Lemma eval_cond_correct : + forall stk f sp pc rs m res ml st asr asa e b f' s s' args i cond, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> + (forall v, In v args -> Ple v (RTL.max_reg_function f)) -> + Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> + translate_condition cond args s = OK e s' i -> + Verilog.expr_runp f' asr asa e (boolToValue b). + Proof. + intros stk f sp pc rs m res ml st asr asa e b f' s s' args i cond MSTATE MAX_FUN EVAL TR_INSTR. + pose proof MSTATE as MSTATE_2. inv MSTATE. + inv MASSOC. unfold translate_condition, translate_comparison, + translate_comparisonu, translate_comparison_imm, + translate_comparison_immu in TR_INSTR; + repeat unfold_match TR_INSTR; try inv TR_INSTR; simplify_val; + unfold Values.Val.cmp_bool, Values.Val.of_optbool, bop, Values.Val.cmpu_bool, + Int.cmpu in *; + repeat unfold_match EVAL. + - repeat econstructor. repeat unfold_match Heqo. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo; simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; solve_cond. + - repeat econstructor. repeat unfold_match Heqo; simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val. + rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3. + unfold Ptrofs.ltu. unfold Int.ltu. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto. + - repeat econstructor. unfold Verilog.binop_run. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; simplify_val; solve_cond. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val. + rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3. + unfold Ptrofs.ltu. unfold Int.ltu. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto. + - repeat econstructor. unfold Verilog.binop_run. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; simplify_val; solve_cond. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val. + rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3. + unfold Ptrofs.ltu. unfold Int.ltu. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto. + - repeat econstructor. unfold Verilog.binop_run. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; simplify_val; solve_cond. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + pose proof (MAX_FUN p0) as MAX_FUN_P0. apply H in MAX_FUN_P0; auto. + inv MAX_FUN_P; inv MAX_FUN_P0; try solve_cond. simplify_val. + rewrite Heqv0 in H3. rewrite Heqv in H2. inv H2. inv H3. + unfold Ptrofs.ltu. unfold Int.ltu. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr by apply Int.unsigned_range_2. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + - repeat econstructor. simplify_val. + pose proof (MAX_FUN p) as MAX_FUN_P. apply H in MAX_FUN_P; auto. + inv MAX_FUN_P; simplify_val; try solve_cond. + rewrite Heqv in H0. inv H0. auto. + Qed. + + Lemma eval_cond_correct' : + forall e stk f sp pc rs m res ml st asr asa v f' s s' args i cond, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> + (forall v, In v args -> Ple v (RTL.max_reg_function f)) -> + Values.Val.of_optbool None = v -> + translate_condition cond args s = OK e s' i -> + exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. + intros e stk f sp pc rs m res ml st asr asa v f' s s' args i cond MSTATE MAX_FUN EVAL TR_INSTR. + unfold translate_condition, translate_comparison, translate_comparisonu, + translate_comparison_imm, translate_comparison_immu, bop, boplit in *. + repeat unfold_match TR_INSTR; inv TR_INSTR; repeat econstructor. + Qed. + + Lemma eval_correct : + forall s sp op rs m v e asr asa f f' stk s' i pc res0 pc' args res ml st, + match_states (RTL.State stk f sp pc rs m) (HTL.State res ml st asr asa) -> + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> + Op.eval_operation ge sp op + (List.map (fun r : BinNums.positive => Registers.Regmap.get r rs) args) m = Some v -> + translate_instr op args s = OK e s' i -> + exists v', Verilog.expr_runp f' asr asa e v' /\ val_value_lessdef v v'. + Proof. + intros s sp op rs m v e asr asa f f' stk s' i pc pc' res0 args res ml st MSTATE INSTR EVAL TR_INSTR. + pose proof MSTATE as MSTATE_2. inv MSTATE. + inv MASSOC. unfold translate_instr in TR_INSTR; repeat (unfold_match TR_INSTR); inv TR_INSTR; + unfold Op.eval_operation in EVAL; repeat (unfold_match EVAL); inv EVAL; + repeat (simplify; eval_correct_tac; unfold valueToInt in *). + - pose proof Integers.Ptrofs.agree32_sub as H2; unfold Integers.Ptrofs.agree32 in H2. + unfold Ptrofs.of_int. simpl. + apply ptrofs_inj. assert (Archi.ptr64 = false) by auto. eapply H2 in H3. + rewrite Ptrofs.unsigned_repr. apply H3. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. + auto. rewrite Ptrofs.unsigned_repr. replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + apply Int.unsigned_range_2. + - pose proof Integers.Ptrofs.agree32_sub as AGR; unfold Integers.Ptrofs.agree32 in AGR. + assert (ARCH: Archi.ptr64 = false) by auto. eapply AGR in ARCH. + apply int_inj. unfold Ptrofs.to_int. rewrite Int.unsigned_repr. + apply ARCH. pose proof Ptrofs.unsigned_range_2. + replace Ptrofs.max_unsigned with Int.max_unsigned; auto. + pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. + eapply H2 in ARCH. apply ARCH. + pose proof Ptrofs.agree32_of_int. unfold Ptrofs.agree32 in H2. + eapply H2 in ARCH. apply ARCH. + - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. + - rewrite Heqb in Heqb0. discriminate. + - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. + - rewrite Heqb in Heqb0. discriminate. + (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, + repeat (rewrite Int.unsigned_repr). auto.*) + - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). + destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac. + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. rewrite H2 in H0. inv H0. unfold valueToPtr. unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + * inv Heqv. unfold valueToInt in *. inv H2. inv H0. unfold valueToInt in *. trivial. + * constructor. unfold valueToPtr, ZToValue in *. + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. inv Heqv. rewrite Int.add_commut. + apply AGR. auto. inv H1. inv H0. unfold valueToPtr. unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + unfold Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr. inv H0. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr. auto. replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + apply Int.unsigned_range_2. + * constructor. unfold valueToPtr, ZToValue in *. + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. inv Heqv. + apply AGR. auto. inv H0. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + inv H1. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. + rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. + apply Int.unsigned_range_2. apply Int.unsigned_range_2. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). inv Heqv. inv H3. + unfold valueToInt, ZToValue. auto. + * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). + * unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). + * constructor. unfold valueToPtr, ZToValue. unfold Values.Val.mul in Heqv. repeat (unfold_match Heqv). + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + unfold valueToPtr, ZToValue. + repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1. + inv Heqv1. inv Heqv0. unfold valueToInt in *. + assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H2. inv H2. auto. + rewrite Heqv2 in H2. inv H2. + rewrite Heqv2 in H3. discriminate. + repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1. + repeat unfold_match Heqv0. unfold Values.Val.mul in Heqv1. repeat unfold_match Heqv1. + constructor. unfold valueToPtr, ZToValue. inv Heqv0. inv Heqv1. + assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. unfold valueToInt in *. rewrite Heqv2 in H3. inv H3. + + pose proof Integers.Ptrofs.agree32_add as AGR; unfold Integers.Ptrofs.agree32 in AGR. unfold ZToValue. + apply ptrofs_inj. unfold Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. + apply AGR. auto. inv H2. unfold valueToPtr, Ptrofs.of_int. rewrite Ptrofs.unsigned_repr. auto. + replace Ptrofs.max_unsigned with Int.max_unsigned by auto. apply Int.unsigned_range_2. + apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. apply Int.unsigned_range_2. + + rewrite Heqv2 in H3. inv H3. + + rewrite Heqv2 in H4. inv H4. + + unfold translate_eff_addressing in *. repeat (unfold_match H1). inv H1. + inv Heql. unfold boplitz. repeat (simplify; eval_correct_tac). + all: repeat (unfold_match Heqv). + eexists. split. constructor. + constructor. unfold valueToPtr, ZToValue. rewrite Ptrofs.add_zero_l. unfold Ptrofs.of_int. + rewrite Int.unsigned_repr. symmetry. apply Ptrofs.repr_unsigned. + unfold check_address_parameter_unsigned in *. apply Ptrofs.unsigned_range_2. + - destruct (Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m) eqn:EQ. + + exploit eval_cond_correct; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. auto. + intros. econstructor. econstructor. eassumption. unfold boolToValue, Values.Val.of_optbool. + destruct b; constructor; auto. + + eapply eval_cond_correct'; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. auto. + - monadInv H1. + destruct (Op.eval_condition c (map (fun r1 : positive => Registers.Regmap.get r1 rs) l0) m) eqn:EQN; + simplify. destruct b eqn:B. + + exploit eval_cond_correct; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. + simplify; tauto. intros. + econstructor. econstructor. eapply Verilog.erun_Vternary_true. eassumption. econstructor. auto. + auto. unfold Values.Val.normalize. + destruct (Registers.Regmap.get r rs) eqn:EQN2; constructor. + * assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. unfold valueToInt in H1. rewrite EQN2 in H1. inv H1. auto. + rewrite EQN2 in H1. discriminate. rewrite EQN2 in H2. discriminate. + * assert (HPle1 : Ple r (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. rewrite EQN2 in H1. inv H1. rewrite EQN2 in H1. inv H1. auto. + rewrite EQN2 in H2. discriminate. + + exploit eval_cond_correct; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. + simplify; tauto. intros. + econstructor. econstructor. eapply Verilog.erun_Vternary_false. eassumption. econstructor. auto. + auto. unfold Values.Val.normalize. + destruct (Registers.Regmap.get r0 rs) eqn:EQN2; constructor. + * assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. unfold valueToInt in H1. rewrite EQN2 in H1. inv H1. auto. + rewrite EQN2 in H1. discriminate. rewrite EQN2 in H2. discriminate. + * assert (HPle1 : Ple r0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H in HPle1. inv HPle1. rewrite EQN2 in H1. inv H1. rewrite EQN2 in H1. inv H1. auto. + rewrite EQN2 in H2. discriminate. + + exploit eval_cond_correct'; eauto. intros. eapply RTL.max_reg_function_use. apply INSTR. + simplify; tauto. intros. inv H0. inv H1. destruct (Int.eq_dec x0 Int.zero). + econstructor. econstructor. eapply Verilog.erun_Vternary_false. + eassumption. econstructor. auto. subst. auto. constructor. + econstructor. econstructor. eapply Verilog.erun_Vternary_true. + eassumption. econstructor. auto. unfold valueToBool. pose proof n. apply Int.eq_false in n. + unfold uvalueToZ. unfold Int.eq in n. unfold zeq in *. + destruct (Int.unsigned x0 ==Z Int.unsigned Int.zero); try discriminate. + rewrite <- Z.eqb_neq in n0. rewrite Int.unsigned_zero in n0. rewrite n0. auto. + constructor. + Qed. + + (** The proof of semantic preservation for the translation of instructions + is a simulation argument based on diagrams of the following form: +<< + match_states + code st rs ---------------- State m st assoc + || | + || | + || | + \/ v + code st rs' --------------- State m st assoc' + match_states +>> + where [tr_code c data control fin rtrn st] is assumed to hold. + + The precondition and postcondition is that that should hold is [match_assocmaps rs assoc]. + *) + + Definition transl_instr_prop (instr : RTL.instruction) : Prop := + forall m asr asa fin rtrn st stmt trans res, + tr_instr fin rtrn st (m.(HTL.mod_stk)) instr stmt trans -> + exists asr' asa', + HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). + + Opaque combine. + + Ltac tac0 := + match goal with + | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs + | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr + | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge + | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros + | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set + + | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack + + | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss + | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso + | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty + + | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => + rewrite combine_lookup_first + + | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 + | [ |- context[match_states _ _] ] => econstructor; auto + | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto + | [ |- match_assocmaps _ _ _ # _ <- (posToValue _) ] => + apply regs_lessdef_add_greater; [> unfold Plt; lia | assumption] + + | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => + unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal + | [ |- context[(AssocMap.combine _ _ _) ! _] ] => + try (rewrite AssocMap.gcombine; [> | reflexivity]) + + | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => + rewrite Registers.Regmap.gss + | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => + let EQ := fresh "EQ" in + destruct (Pos.eq_dec s d) as [EQ|EQ]; + [> rewrite EQ | rewrite Registers.Regmap.gso; auto] + + | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H + | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] + | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H + end. + + Ltac small_tac := repeat (crush_val; try array; try ptrofs); crush_val; auto. + Ltac big_tac := repeat (crush_val; try array; try ptrofs; try tac0); crush_val; auto. + + Lemma transl_inop_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) + (rs : RTL.regset) (m : mem) (pc' : RTL.node), + (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> + forall R1 : HTL.state, + match_states (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Proof. + intros s f sp pc rs m pc' H R1 MSTATE. + inv_state. + + unfold match_prog in TRANSL. + econstructor. + split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + (* processing of state *) + econstructor. + crush. + econstructor. + econstructor. + econstructor. + + all: invert MARR; big_tac. + + inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. + + Unshelve. exact tt. + Qed. + Hint Resolve transl_inop_correct : htlproof. + + Lemma transl_iop_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) + (rs : Registers.Regmap.t Values.val) (m : mem) (op : Op.operation) (args : list Registers.reg) + (res0 : Registers.reg) (pc' : RTL.node) (v : Values.val), + (RTL.fn_code f) ! pc = Some (RTL.Iop op args res0 pc') -> + Op.eval_operation ge sp op (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some v -> + forall R1 : HTL.state, + match_states (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states (RTL.State s f sp pc' (Registers.Regmap.set res0 v rs) m) R2. + Proof. + intros s f sp pc rs m op args res0 pc' v H H0 R1 MSTATE. + inv_state. inv MARR. + exploit eval_correct; eauto. intros. inversion H1. inversion H2. + econstructor. split. + apply Smallstep.plus_one. + eapply HTL.step_module; eauto. + inv CONST. assumption. + inv CONST. assumption. + econstructor; simpl; trivial. + constructor; trivial. + econstructor; simpl; eauto. + simpl. econstructor. econstructor. + apply H5. simplify. + + all: big_tac. + + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + + unfold Ple in HPle. lia. + apply regs_lessdef_add_match. assumption. + apply regs_lessdef_add_greater. unfold Plt; lia. assumption. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle; lia. + eapply op_stack_based; eauto. + inv CONST. constructor; simplify. rewrite AssocMap.gso. rewrite AssocMap.gso. + assumption. lia. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle. lia. + rewrite AssocMap.gso. rewrite AssocMap.gso. + assumption. lia. + assert (HPle: Ple res0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_def; eauto; simpl; auto). + unfold Ple in HPle. lia. + Unshelve. exact tt. + Qed. + Hint Resolve transl_iop_correct : htlproof. + + Ltac tac := + repeat match goal with + | [ _ : error _ _ = OK _ _ _ |- _ ] => discriminate + | [ _ : context[if (?x && ?y) then _ else _] |- _ ] => + let EQ1 := fresh "EQ" in + let EQ2 := fresh "EQ" in + destruct x eqn:EQ1; destruct y eqn:EQ2; simpl in * + | [ _ : context[if ?x then _ else _] |- _ ] => + let EQ := fresh "EQ" in + destruct x eqn:EQ; simpl in * + | [ H : ret _ _ = _ |- _ ] => invert H + | [ _ : context[match ?x with | _ => _ end] |- _ ] => destruct x + end. + + Ltac inv_arr_access := + match goal with + | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => + destruct c, chunk, addr, args; crush; tac; crush + end. + + Lemma offset_expr_ok : + forall v z, (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ v)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) + (Integers.Ptrofs.repr 4))) + = valueToNat (Int.divu (Int.add v (ZToValue z)) (ZToValue 4))). + Proof. + simplify_val. unfold valueToNat. unfold Int.divu, Ptrofs.divu. + pose proof Integers.Ptrofs.agree32_add as AGR. + unfold Integers.Ptrofs.agree32 in AGR. + assert (Ptrofs.unsigned (Ptrofs.add (Ptrofs.repr (Int.unsigned v)) + (Ptrofs.repr (Int.unsigned (Int.repr z)))) = + Int.unsigned (Int.add v (ZToValue z))). + apply AGR; auto. + apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. + apply Ptrofs.unsigned_repr. apply Int.unsigned_range_2. + rewrite H. replace (Ptrofs.unsigned (Ptrofs.repr 4)) with 4. + replace (Int.unsigned (ZToValue 4)) with 4. + pose proof Ptrofs.agree32_repr. unfold Ptrofs.agree32 in *. + rewrite H0. trivial. auto. + unfold ZToValue. symmetry. apply Int.unsigned_repr. + unfold_constants. lia. + unfold ZToValue. symmetry. apply Int.unsigned_repr. + unfold_constants. lia. + Qed. + + Lemma offset_expr_ok_2 : + forall v0 v1 z0 z1, + (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ v0)) + (Integers.Ptrofs.of_int + (Integers.Int.add + (Integers.Int.mul (valueToInt v1) (Integers.Int.repr z1)) + (Integers.Int.repr z0)))) (Ptrofs.repr 4)))) + = valueToNat (Int.divu (Int.add (Int.add v0 (ZToValue z0)) + (Int.mul v1 (ZToValue z1))) (ZToValue 4)). + intros. unfold ZToValue, valueToNat, valueToInt, Ptrofs.divu, Int.divu, Ptrofs.of_int. + + assert (H : (Ptrofs.unsigned + (Ptrofs.add (Ptrofs.repr (uvalueToZ v0)) + (Ptrofs.of_int (Int.add (Int.mul (valueToInt v1) (Int.repr z1)) (Int.repr z0)))) / + Ptrofs.unsigned (Ptrofs.repr 4)) + = (Int.unsigned (Int.add (Int.add v0 (Int.repr z0)) (Int.mul v1 (Int.repr z1))) / + Int.unsigned (Int.repr 4))). + { unfold ZToValue, valueToNat, valueToInt, Ptrofs.divu, Int.divu, Ptrofs.of_int. + rewrite Ptrofs.unsigned_repr by (unfold_constants; lia). + rewrite Int.unsigned_repr by (unfold_constants; lia). + + unfold Ptrofs.of_int. rewrite Int.add_commut. + pose proof Integers.Ptrofs.agree32_add as AGR. unfold Ptrofs.agree32 in *. + erewrite AGR. + 3: { unfold uvalueToZ. rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. } + 3: { rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. } + rewrite Int.add_assoc. trivial. auto. + } + + rewrite <- H. auto. + + Qed. + + Lemma offset_expr_ok_3 : + forall OFFSET, + Z.to_nat (Ptrofs.unsigned (Ptrofs.divu OFFSET (Ptrofs.repr 4))) + = valueToNat (ZToValue (Ptrofs.unsigned OFFSET / 4)). + Proof. auto. Qed. + + Lemma transl_iload_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) + (rs : Registers.Regmap.t Values.val) (m : mem) (chunk : AST.memory_chunk) + (addr : Op.addressing) (args : list Registers.reg) (dst : Registers.reg) + (pc' : RTL.node) (a v : Values.val), + (RTL.fn_code f) ! pc = Some (RTL.Iload chunk addr args dst pc') -> + Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> + Mem.loadv chunk m a = Some v -> + forall R1 : HTL.state, + match_states (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states (RTL.State s f sp pc' (Registers.Regmap.set dst v rs) m) R2. + Proof. + intros s f sp pc rs m chunk addr args dst pc' a v H H0 H1 R1 MSTATE. + inv_state. inv_arr_access. + + + (** Preamble *) + invert MARR. inv CONST. crush. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; crush. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. + + rewrite ARCHI in H1. crush. + subst. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). + apply H0 in HPler0. + invert HPler0; try congruence. + rewrite EQr0 in H11. + invert H11. + + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; crush. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { apply Mem.load_valid_access in H1. unfold Mem.valid_access in *. simplify. + apply Zdivide_mod. assumption. } + + (** Read bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET + Op.eval_addressing ge sp addr (map (fun r : positive => Registers.Regmap.get r rs) args) = Some a -> + Mem.storev chunk m a (Registers.Regmap.get src rs) = Some m' -> + forall R1 : HTL.state, + match_states (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m') R2. + Proof. + intros s f sp pc rs m chunk addr args src pc' a m' H H0 H1 R1 MSTATES. + inv_state. inv_arr_access. + + + (** Preamble *) + invert MARR. inv CONST. crush. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; crush. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. + + rewrite ARCHI in H1. crush. + subst. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). + apply H8 in HPler0. + invert HPler0; try congruence. + rewrite EQr0 in H11. + invert H11. + clear H0. clear H8. + + unfold check_address_parameter_unsigned in *; + unfold check_address_parameter_signed in *; crush. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. + apply Zdivide_mod. assumption. } + + (** Write bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. + assert (Mem.valid_access m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) Writable). + { pose proof H1. eapply Mem.store_valid_access_2 in H11. + exact H11. eapply Mem.store_valid_access_3. eassumption. } + pose proof (Mem.valid_access_store m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) v). + apply X in H11. invert H11. congruence. + + constructor; simplify. unfold Verilog.merge_regs. unfold_merge. + rewrite AssocMap.gso. + assumption. lia. + unfold Verilog.merge_regs. unfold_merge. + rewrite AssocMap.gso. + assumption. lia. + + + (** Preamble *) + invert MARR. inv CONST. crush. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; crush. + + unfold reg_stack_based_pointers in RSBP. + pose proof (RSBP r0) as RSBPr0. + pose proof (RSBP r1) as RSBPr1. + + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. + + rewrite ARCHI in H1. crush. + subst. + clear RSBPr1. + + pose proof MASSOC as MASSOC'. + invert MASSOC'. + pose proof (H0 r0). + pose proof (H0 r1). + assert (HPler0 : Ple r0 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). + assert (HPler1 : Ple r1 (RTL.max_reg_function f)) + by (eapply RTL.max_reg_function_use; eauto; simpl; auto). + apply H8 in HPler0. + apply H11 in HPler1. + invert HPler0; invert HPler1; try congruence. + rewrite EQr0 in H13. + rewrite EQr1 in H14. + invert H13. invert H14. + clear H0. clear H8. clear H11. + + unfold check_address_parameter_signed in *; + unfold check_address_parameter_unsigned in *; crush. + + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (uvalueToZ asr # r0)) + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) + (Integers.Int.repr z0)))) as OFFSET. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. + apply Zdivide_mod. assumption. } + + (** Write bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:EQ end; try reflexivity. + assert (Mem.valid_access m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) Writable). + { pose proof H1. eapply Mem.store_valid_access_2 in H14. + exact H14. eapply Mem.store_valid_access_3. eassumption. } + pose proof (Mem.valid_access_store m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) v). + apply X in H14. invert H14. congruence. + + constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. + assumption. lia. + unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. + assumption. lia. + + + invert MARR. inv CONST. crush. + + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; crush. + rewrite ARCHI in H0. crush. + + unfold check_address_parameter_unsigned in *; + unfold check_address_parameter_signed in *; crush. + + assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. + rewrite ZERO in H1. clear ZERO. + rewrite Integers.Ptrofs.add_zero_l in H1. + + remember i0 as OFFSET. + + (** Modular preservation proof *) + assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. + { apply Mem.store_valid_access_3 in H1. unfold Mem.valid_access in *. simplify. + apply Zdivide_mod. assumption. } + + (** Write bounds proof *) + assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. + { destruct (Integers.Ptrofs.unsigned OFFSET destruct x eqn:?EQ end; try reflexivity. + assert (Mem.valid_access m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) Writable). + { pose proof H1. eapply Mem.store_valid_access_2 in H0. + exact H0. eapply Mem.store_valid_access_3. eassumption. } + pose proof (Mem.valid_access_store m AST.Mint32 sp' + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.add (Integers.Ptrofs.repr 0) + (Integers.Ptrofs.repr ptr))) v). + apply X in H0. invert H0. congruence. + + constructor; simplify. unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. + assumption. lia. + unfold Verilog.merge_regs. unfold_merge. rewrite AssocMap.gso. + assumption. lia. + + Unshelve. + exact tt. + exact (Values.Vint (Int.repr 0)). + exact tt. + exact (Values.Vint (Int.repr 0)). + exact tt. + exact (Values.Vint (Int.repr 0)). + Qed. + Hint Resolve transl_istore_correct : htlproof. + + Lemma transl_icond_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) + (rs : Registers.Regmap.t Values.val) (m : mem) (cond : Op.condition) (args : list Registers.reg) + (ifso ifnot : RTL.node) (b : bool) (pc' : RTL.node), + (RTL.fn_code f) ! pc = Some (RTL.Icond cond args ifso ifnot) -> + Op.eval_condition cond (map (fun r : positive => Registers.Regmap.get r rs) args) m = Some b -> + pc' = (if b then ifso else ifnot) -> + forall R1 : HTL.state, + match_states (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Proof. + intros s f sp pc rs m cond args ifso ifnot b pc' H H0 H1 R1 MSTATE. + inv_state. + destruct b. + - eexists. split. apply Smallstep.plus_one. + clear H33. + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + econstructor; simpl; trivial. + constructor; trivial. + eapply Verilog.erun_Vternary_true; simpl; eauto. + eapply eval_cond_correct; eauto. intros. + intros. eapply RTL.max_reg_function_use. apply H22. auto. + econstructor. auto. + simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + apply AssocMap.gss. + + inv MARR. inv CONST. + big_tac. + constructor; rewrite AssocMap.gso; simplify; try assumption; lia. + - eexists. split. apply Smallstep.plus_one. + clear H32. + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + econstructor; simpl; trivial. + constructor; trivial. + eapply Verilog.erun_Vternary_false; simpl; eauto. + eapply eval_cond_correct; eauto. intros. + intros. eapply RTL.max_reg_function_use. apply H22. auto. + econstructor. auto. + simpl. econstructor. unfold Verilog.merge_regs. unfold_merge. simpl. + apply AssocMap.gss. + + inv MARR. inv CONST. + big_tac. + constructor; rewrite AssocMap.gso; simplify; try assumption; lia. + + Unshelve. all: exact tt. + Qed. + Hint Resolve transl_icond_correct : htlproof. + + (*Lemma transl_ijumptable_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) + (rs : Registers.Regmap.t Values.val) (m : mem) (arg : Registers.reg) (tbl : list RTL.node) + (n : Integers.Int.int) (pc' : RTL.node), + (RTL.fn_code f) ! pc = Some (RTL.Ijumptable arg tbl) -> + Registers.Regmap.get arg rs = Values.Vint n -> + list_nth_z tbl (Integers.Int.unsigned n) = Some pc' -> + forall R1 : HTL.state, + match_states (RTL.State s f sp pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2. + Proof. + intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. + + Hint Resolve transl_ijumptable_correct : htlproof.*) + + Lemma transl_ireturn_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (stk : Values.block) + (pc : positive) (rs : RTL.regset) (m : mem) (or : option Registers.reg) + (m' : mem), + (RTL.fn_code f) ! pc = Some (RTL.Ireturn or) -> + Mem.free m stk 0 (RTL.fn_stacksize f) = Some m' -> + forall R1 : HTL.state, + match_states (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) pc rs m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states (RTL.Returnstate s (Registers.regmap_optget or Values.Vundef rs) m') R2. + Proof. + intros s f stk pc rs m or m' H H0 R1 MSTATE. + inv_state. + + - econstructor. split. + eapply Smallstep.plus_two. + + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + constructor. + econstructor; simpl; trivial. + econstructor; simpl; trivial. + constructor. + econstructor; simpl; trivial. + constructor. + + constructor. constructor. + + unfold state_st_wf in WF; big_tac; eauto. + destruct wf as [HCTRL HDATA]. apply HCTRL. + apply AssocMapExt.elements_iff. eexists. + match goal with H: control ! pc = Some _ |- _ => apply H end. + + apply HTL.step_finish. + unfold Verilog.merge_regs. + unfold_merge; simpl. + rewrite AssocMap.gso. + apply AssocMap.gss. lia. + apply AssocMap.gss. + rewrite Events.E0_left. reflexivity. + + constructor; auto. + constructor. + + (* FIXME: Duplication *) + - econstructor. split. + eapply Smallstep.plus_two. + eapply HTL.step_module; eauto. + inv CONST; assumption. + inv CONST; assumption. + constructor. + econstructor; simpl; trivial. + econstructor; simpl; trivial. + constructor. constructor. constructor. + constructor. constructor. constructor. + + unfold state_st_wf in WF; big_tac; eauto. + + destruct wf as [HCTRL HDATA]. apply HCTRL. + apply AssocMapExt.elements_iff. eexists. + match goal with H: control ! pc = Some _ |- _ => apply H end. + + apply HTL.step_finish. + unfold Verilog.merge_regs. + unfold_merge. + rewrite AssocMap.gso. + apply AssocMap.gss. simpl; lia. + apply AssocMap.gss. + rewrite Events.E0_left. trivial. + + constructor; auto. + + simpl. inversion MASSOC. subst. + unfold find_assocmap, AssocMapExt.get_default. rewrite AssocMap.gso. + apply H1. eapply RTL.max_reg_function_use. eauto. simpl; tauto. + assert (HPle : Ple r (RTL.max_reg_function f)). + eapply RTL.max_reg_function_use. eassumption. simpl; auto. + apply ZExtra.Ple_not_eq. apply ZExtra.Ple_Plt_Succ. assumption. + + Unshelve. + all: constructor. + Qed. + Hint Resolve transl_ireturn_correct : htlproof. + + Lemma transl_callstate_correct: + forall (s : list RTL.stackframe) (f : RTL.function) (args : list Values.val) + (m : mem) (m' : Mem.mem') (stk : Values.block), + Mem.alloc m 0 (RTL.fn_stacksize f) = (m', stk) -> + forall R1 : HTL.state, + match_states (RTL.Callstate s (AST.Internal f) args m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states + (RTL.State s f (Values.Vptr stk Integers.Ptrofs.zero) (RTL.fn_entrypoint f) + (RTL.init_regs args (RTL.fn_params f)) m') R2. + Proof. + intros s f args m m' stk H R1 MSTATE. + + inversion MSTATE; subst. inversion TF; subst. + econstructor. split. apply Smallstep.plus_one. + eapply HTL.step_call. crush. + + apply match_state with (sp' := stk); eauto. + + all: big_tac. + + apply regs_lessdef_add_greater. unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. + apply regs_lessdef_add_greater. unfold Plt; lia. + apply init_reg_assoc_empty. + + constructor. + + destruct (Mem.load AST.Mint32 m' stk + (Integers.Ptrofs.unsigned (Integers.Ptrofs.add + Integers.Ptrofs.zero + (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. + pose proof Mem.load_alloc_same as LOAD_ALLOC. + pose proof H as ALLOC. + eapply LOAD_ALLOC in ALLOC. + 2: { exact LOAD. } + ptrofs. rewrite LOAD. + rewrite ALLOC. + repeat constructor. + + ptrofs. rewrite LOAD. + repeat constructor. + + unfold reg_stack_based_pointers. intros. + unfold RTL.init_regs; crush. + destruct (RTL.fn_params f); + rewrite Registers.Regmap.gi; constructor. + + unfold arr_stack_based_pointers. intros. + crush. + destruct (Mem.load AST.Mint32 m' stk + (Integers.Ptrofs.unsigned (Integers.Ptrofs.add + Integers.Ptrofs.zero + (Integers.Ptrofs.repr (4 * ptr))))) eqn:LOAD. + pose proof Mem.load_alloc_same as LOAD_ALLOC. + pose proof H as ALLOC. + eapply LOAD_ALLOC in ALLOC. + 2: { exact LOAD. } + rewrite ALLOC. + repeat constructor. + constructor. + + Transparent Mem.alloc. (* TODO: Since there are opaque there's probably a lemma. *) + Transparent Mem.load. + Transparent Mem.store. + unfold stack_bounds. + split. + + unfold Mem.alloc in H. + invert H. + crush. + unfold Mem.load. + intros. + match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. + invert v0. unfold Mem.range_perm in H4. + unfold Mem.perm in H4. crush. + unfold Mem.perm_order' in H4. + small_tac. + exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. + rewrite Maps.PMap.gss in H8. + match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. + crush. + apply proj_sumbool_true in H10. lia. + + unfold Mem.alloc in H. + invert H. + crush. + unfold Mem.store. + intros. + match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. + invert v0. unfold Mem.range_perm in H4. + unfold Mem.perm in H4. crush. + unfold Mem.perm_order' in H4. + small_tac. + exploit (H4 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. + rewrite Maps.PMap.gss in H8. + match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. + crush. + apply proj_sumbool_true in H10. lia. + constructor. simplify. rewrite AssocMap.gss. + simplify. rewrite AssocMap.gso. apply AssocMap.gss. simplify. lia. + Opaque Mem.alloc. + Opaque Mem.load. + Opaque Mem.store. + Qed. + Hint Resolve transl_callstate_correct : htlproof. + + Lemma transl_returnstate_correct: + forall (res0 : Registers.reg) (f : RTL.function) (sp : Values.val) (pc : RTL.node) + (rs : RTL.regset) (s : list RTL.stackframe) (vres : Values.val) (m : mem) + (R1 : HTL.state), + match_states (RTL.Returnstate (RTL.Stackframe res0 f sp pc rs :: s) vres m) R1 -> + exists R2 : HTL.state, + Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ + match_states (RTL.State s f sp pc (Registers.Regmap.set res0 vres rs) m) R2. + Proof. + intros res0 f sp pc rs s vres m R1 MSTATE. + inversion MSTATE. inversion MF. + Qed. + Hint Resolve transl_returnstate_correct : htlproof. + + Lemma option_inv : + forall A x y, + @Some A x = Some y -> x = y. + Proof. intros. inversion H. trivial. Qed. + + Lemma main_tprog_internal : + forall b, + Globalenvs.Genv.find_symbol tge tprog.(AST.prog_main) = Some b -> + exists f, Genv.find_funct_ptr (Genv.globalenv tprog) b = Some (AST.Internal f). + Proof. + intros. + destruct TRANSL. unfold main_is_internal in H1. + repeat (unfold_match H1). replace b with b0. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + unfold transl_fundef, AST.transf_partial_fundef, Errors.bind in B. + unfold_match B. inv B. econstructor. apply A. + + apply option_inv. rewrite <- Heqo. rewrite <- H. + rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). + trivial. symmetry; eapply Linking.match_program_main; eauto. + Qed. + + Lemma transl_initial_states : + forall s1 : Smallstep.state (RTL.semantics prog), + Smallstep.initial_state (RTL.semantics prog) s1 -> + exists s2 : Smallstep.state (HTL.semantics tprog), + Smallstep.initial_state (HTL.semantics tprog) s2 /\ match_states s1 s2. + Proof. + induction 1. + destruct TRANSL. unfold main_is_internal in H4. + repeat (unfold_match H4). + assert (f = AST.Internal f1). apply option_inv. + rewrite <- Heqo0. rewrite <- H1. replace b with b0. + auto. apply option_inv. rewrite <- H0. rewrite <- Heqo. + trivial. + exploit function_ptr_translated; eauto. + intros [tf [A B]]. + unfold transl_fundef, Errors.bind in B. + unfold AST.transf_partial_fundef, Errors.bind in B. + repeat (unfold_match B). inversion B. subst. + exploit main_tprog_internal; eauto; intros. + rewrite symbols_preserved. replace (AST.prog_main tprog) with (AST.prog_main prog). + apply Heqo. symmetry; eapply Linking.match_program_main; eauto. + inversion H5. + econstructor; split. econstructor. + apply (Genv.init_mem_transf_partial TRANSL'); eauto. + replace (AST.prog_main tprog) with (AST.prog_main prog). + rewrite symbols_preserved; eauto. + symmetry; eapply Linking.match_program_main; eauto. + apply H6. + + constructor. + apply transl_module_correct. + assert (Some (AST.Internal x) = Some (AST.Internal m)). + replace (AST.fundef HTL.module) with (HTL.fundef). + rewrite <- H6. setoid_rewrite <- A. trivial. + trivial. inv H7. assumption. + Qed. + Hint Resolve transl_initial_states : htlproof. + + Lemma transl_final_states : + forall (s1 : Smallstep.state (RTL.semantics prog)) + (s2 : Smallstep.state (HTL.semantics tprog)) + (r : Integers.Int.int), + match_states s1 s2 -> + Smallstep.final_state (RTL.semantics prog) s1 r -> + Smallstep.final_state (HTL.semantics tprog) s2 r. + Proof. + intros. inv H0. inv H. inv H4. invert MF. constructor. reflexivity. + Qed. + Hint Resolve transl_final_states : htlproof. + + Theorem transl_step_correct: + forall (S1 : RTL.state) t S2, + RTL.step ge S1 t S2 -> + forall (R1 : HTL.state), + match_states S1 R1 -> + exists R2, Smallstep.plus HTL.step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; eauto with htlproof; (intros; inv_state). + Qed. + Hint Resolve transl_step_correct : htlproof. + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus; eauto with htlproof. + apply senv_preserved. + Qed. + +End CORRECTNESS. diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v new file mode 100644 index 0000000..541f9fa --- /dev/null +++ b/src/hls/HTLgenspec.v @@ -0,0 +1,641 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require RTL Op Maps Errors. +From compcert Require Import Maps Integers. +From vericert Require Import Vericertlib Verilog ValueInt HTL HTLgen AssocMap. +Require Import Lia. + +Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. +Hint Resolve Maps.PTree.elements_correct : htlspec. + +Remark bind_inversion: + forall (A B: Type) (f: mon A) (g: A -> mon B) + (y: B) (s1 s3: st) (i: st_incr s1 s3), + bind f g s1 = OK y s3 i -> + exists x, exists s2, exists i1, exists i2, + f s1 = OK x s2 i1 /\ g x s2 = OK y s3 i2. +Proof. + intros until i. unfold bind. destruct (f s1); intros. + discriminate. + exists a; exists s'; exists s. + destruct (g a s'); inv H. + exists s0; auto. +Qed. + +Remark bind2_inversion: + forall (A B C: Type) (f: mon (A*B)) (g: A -> B -> mon C) + (z: C) (s1 s3: st) (i: st_incr s1 s3), + bind2 f g s1 = OK z s3 i -> + exists x, exists y, exists s2, exists i1, exists i2, + f s1 = OK (x, y) s2 i1 /\ g x y s2 = OK z s3 i2. +Proof. + unfold bind2; intros. + exploit bind_inversion; eauto. + intros [[x y] [s2 [i1 [i2 [P Q]]]]]. simpl in Q. + exists x; exists y; exists s2; exists i1; exists i2; auto. +Qed. + +Ltac monadInv1 H := + match type of H with + | (OK _ _ _ = OK _ _ _) => + inversion H; clear H; try subst + | (Error _ _ = OK _ _ _) => + discriminate + | (ret _ _ = OK _ _ _) => + inversion H; clear H; try subst + | (error _ _ = OK _ _ _) => + discriminate + | (bind ?F ?G ?S = OK ?X ?S' ?I) => + let x := fresh "x" in ( + let s := fresh "s" in ( + let i1 := fresh "INCR" in ( + let i2 := fresh "INCR" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind_inversion _ _ F G X S S' I H) as [x [s [i1 [i2 [EQ1 EQ2]]]]]; + clear H; + try (monadInv1 EQ2))))))) + | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => + let x1 := fresh "x" in ( + let x2 := fresh "x" in ( + let s := fresh "s" in ( + let i1 := fresh "INCR" in ( + let i2 := fresh "INCR" in ( + let EQ1 := fresh "EQ" in ( + let EQ2 := fresh "EQ" in ( + destruct (bind2_inversion _ _ _ F G X S S' I H) as [x1 [x2 [s [i1 [i2 [EQ1 EQ2]]]]]]; + clear H; + try (monadInv1 EQ2)))))))) + end. + +Ltac monadInv H := + match type of H with + | (ret _ _ = OK _ _ _) => monadInv1 H + | (error _ _ = OK _ _ _) => monadInv1 H + | (bind ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H + | (bind2 ?F ?G ?S = OK ?X ?S' ?I) => monadInv1 H + | (?F _ _ _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + | (?F _ = OK _ _ _) => + ((progress simpl in H) || unfold F in H); monadInv1 H + end. + +(** * Relational specification of the translation *) + +(** We now define inductive predicates that characterise the fact that the +statemachine that is created by the translation contains the correct +translations for each of the elements *) + +Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop := +| tr_instr_Inop : + forall n, + Z.pos n <= Int.max_unsigned -> + tr_instr fin rtrn st stk (RTL.Inop n) Vskip (state_goto st n) +| tr_instr_Iop : + forall n op args dst s s' e i, + Z.pos n <= Int.max_unsigned -> + translate_instr op args s = OK e s' i -> + tr_instr fin rtrn st stk (RTL.Iop op args dst n) (Vnonblock (Vvar dst) e) (state_goto st n) +| tr_instr_Icond : + forall n1 n2 cond args s s' i c, + Z.pos n1 <= Int.max_unsigned -> + Z.pos n2 <= Int.max_unsigned -> + translate_condition cond args s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Icond cond args n1 n2) Vskip (state_cond st c n1 n2) +| tr_instr_Ireturn_None : + tr_instr fin rtrn st stk (RTL.Ireturn None) (Vseq (block fin (Vlit (ZToValue 1%Z))) + (block rtrn (Vlit (ZToValue 0%Z)))) Vskip +| tr_instr_Ireturn_Some : + forall r, + tr_instr fin rtrn st stk (RTL.Ireturn (Some r)) + (Vseq (block fin (Vlit (ZToValue 1%Z))) (block rtrn (Vvar r))) Vskip +| tr_instr_Iload : + forall mem addr args s s' i c dst n, + Z.pos n <= Int.max_unsigned -> + translate_arr_access mem addr args stk s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Iload mem addr args dst n) (nonblock dst c) (state_goto st n) +| tr_instr_Istore : + forall mem addr args s s' i c src n, + Z.pos n <= Int.max_unsigned -> + translate_arr_access mem addr args stk s = OK c s' i -> + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) + (state_goto st n). +(*| tr_instr_Ijumptable : + forall cexpr tbl r, + cexpr = tbl_to_case_expr st tbl -> + tr_instr fin rtrn st stk (RTL.Ijumptable r tbl) (Vskip) (Vcase (Vvar r) cexpr (Some Vskip)).*) +Hint Constructors tr_instr : htlspec. + +Inductive tr_code (c : RTL.code) (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) + (fin rtrn st stk : reg) : Prop := + tr_code_intro : + forall s t, + c!pc = Some i -> + stmnts!pc = Some s -> + trans!pc = Some t -> + tr_instr fin rtrn st stk i s t -> + tr_code c pc i stmnts trans fin rtrn st stk. +Hint Constructors tr_code : htlspec. + +Inductive tr_module (f : RTL.function) : module -> Prop := + tr_module_intro : + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf, + m = (mkmodule f.(RTL.fn_params) + data + control + f.(RTL.fn_entrypoint) + st stk stk_len fin rtrn start rst clk scldecls arrdecls wf) -> + (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> + Z.modulo (f.(RTL.fn_stacksize)) 4 = 0 -> + 0 <= f.(RTL.fn_stacksize) < Integers.Ptrofs.modulus -> + st = ((RTL.max_reg_function f) + 1)%positive -> + fin = ((RTL.max_reg_function f) + 2)%positive -> + rtrn = ((RTL.max_reg_function f) + 3)%positive -> + stk = ((RTL.max_reg_function f) + 4)%positive -> + start = ((RTL.max_reg_function f) + 5)%positive -> + rst = ((RTL.max_reg_function f) + 6)%positive -> + clk = ((RTL.max_reg_function f) + 7)%positive -> + tr_module f m. +Hint Constructors tr_module : htlspec. + +Lemma create_reg_datapath_trans : + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma create_reg_controllogic_trans : + forall sz s s' x i iop, + create_reg iop sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_datapath_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_datapath_trans : htlspec. + +Lemma declare_reg_controllogic_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_reg_controllogic_trans : htlspec. + +Lemma declare_reg_freshreg_trans : + forall sz s s' x i iop r, + declare_reg iop r sz s = OK x s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. inversion 1; auto. Qed. +Hint Resolve declare_reg_freshreg_trans : htlspec. + +Lemma create_arr_datapath_trans : + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_arr_datapath_trans : htlspec. + +Lemma create_arr_controllogic_trans : + forall sz ln s s' x i iop, + create_arr iop sz ln s = OK x s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. intros. monadInv H. trivial. Qed. +Hint Resolve create_arr_controllogic_trans : htlspec. + +Lemma get_refl_x : + forall s s' x i, + get s = OK x s' i -> + s = x. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_x : htlspec. + +Lemma get_refl_s : + forall s s' x i, + get s = OK x s' i -> + s = s'. +Proof. inversion 1. trivial. Qed. +Hint Resolve get_refl_s : htlspec. + +Ltac inv_incr := + repeat match goal with + | [ H: create_reg _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_reg_datapath_trans in H; + eapply create_reg_controllogic_trans in H1 + | [ H: create_arr _ _ _ ?s = OK _ ?s' _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); eapply create_arr_datapath_trans in H; + eapply create_arr_controllogic_trans in H1 + | [ H: get ?s = OK _ _ _ |- _ ] => + let H1 := fresh "H" in + assert (H1 := H); apply get_refl_x in H; apply get_refl_s in H1; + subst + | [ H: st_prop _ _ |- _ ] => unfold st_prop in H; destruct H + | [ H: st_incr _ _ |- _ ] => destruct st_incr + end. + +Lemma collect_controllogic_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_controllogic) = s'.(st_controllogic)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_controllogic) = cs'.(st_controllogic). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_datapath_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_datapath) = s'.(st_datapath)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_datapath) = cs'.(st_datapath). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_freshreg_trans : + forall A f l cs cs' ci, + (forall s s' x i y, f y s = OK x s' i -> s.(st_freshreg) = s'.(st_freshreg)) -> + @HTLMonadExtra.collectlist A f l cs = OK tt cs' ci -> cs.(st_freshreg) = cs'.(st_freshreg). +Proof. + induction l; intros; monadInv H0. + - trivial. + - apply H in EQ. rewrite EQ. eauto. +Qed. + +Lemma collect_declare_controllogic_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_controllogic) = s'.(st_controllogic). +Proof. + intros. eapply collect_controllogic_trans; try eassumption. + intros. eapply declare_reg_controllogic_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_datapath_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_datapath) = s'.(st_datapath). +Proof. + intros. eapply collect_datapath_trans; try eassumption. + intros. eapply declare_reg_datapath_trans. simpl in H0. eassumption. +Qed. + +Lemma collect_declare_freshreg_trans : + forall io n l s s' i, + HTLMonadExtra.collectlist (fun r : reg => declare_reg io r n) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + inversion 1. auto. +Qed. + +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + +Lemma translate_eff_addressing_freshreg_trans : + forall op args s r s' i, + translate_eff_addressing op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_eff_addressing_freshreg_trans : htlspec. + +Lemma translate_comparison_freshreg_trans : + forall op args s r s' i, + translate_comparison op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_freshreg_trans : htlspec. + +Lemma translate_comparisonu_freshreg_trans : + forall op args s r s' i, + translate_comparisonu op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparisonu_freshreg_trans : htlspec. + +Lemma translate_comparison_imm_freshreg_trans : + forall op args s r s' i n, + translate_comparison_imm op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_imm_freshreg_trans : htlspec. + +Lemma translate_comparison_immu_freshreg_trans : + forall op args s r s' i n, + translate_comparison_immu op args n s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; auto. +Qed. +Hint Resolve translate_comparison_immu_freshreg_trans : htlspec. + +Lemma translate_condition_freshreg_trans : + forall op args s r s' i, + translate_condition op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_condition_freshreg_trans : htlspec. + +Lemma translate_instr_freshreg_trans : + forall op args s r s' i, + translate_instr op args s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + destruct op; intros; simpl in *; repeat (unfold_match H); inv H; eauto with htlspec. + monadInv H1. eauto with htlspec. +Qed. +Hint Resolve translate_instr_freshreg_trans : htlspec. + +Lemma translate_arr_access_freshreg_trans : + forall mem addr args st s r s' i, + translate_arr_access mem addr args st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. unfold translate_arr_access in H. repeat (unfold_match H); inv H; eauto with htlspec. +Qed. +Hint Resolve translate_arr_access_freshreg_trans : htlspec. + +Lemma add_instr_freshreg_trans : + forall n n' st s r s' i, + add_instr n n' st s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_freshreg_trans : htlspec. + +Lemma add_branch_instr_freshreg_trans : + forall n n0 n1 e s r s' i, + add_branch_instr e n n0 n1 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_branch_instr in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_branch_instr_freshreg_trans : htlspec. + +Lemma add_node_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_node_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_node_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_node_skip_freshreg_trans : htlspec. + +Lemma add_instr_skip_freshreg_trans : + forall n1 n2 s r s' i, + add_instr_skip n1 n2 s = OK r s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. intros. unfold add_instr_skip in H. repeat (unfold_match H). inv H. auto. Qed. +Hint Resolve add_instr_skip_freshreg_trans : htlspec. + +Lemma transf_instr_freshreg_trans : + forall fin ret st instr s v s' i, + transf_instr fin ret st instr s = OK v s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. destruct instr eqn:?. subst. unfold transf_instr in H. + destruct i0; try (monadInv H); try (unfold_match H); eauto with htlspec. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_instr_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - monadInv H. apply add_instr_freshreg_trans in EQ2. apply translate_arr_access_freshreg_trans in EQ. + apply declare_reg_freshreg_trans in EQ1. congruence. + - monadInv H. apply add_instr_freshreg_trans in EQ0. apply translate_arr_access_freshreg_trans in EQ. congruence. + - monadInv H. apply translate_condition_freshreg_trans in EQ. apply add_branch_instr_freshreg_trans in EQ0. + congruence. + (*- inv EQ. apply add_node_skip_freshreg_trans in EQ0. congruence.*) +Qed. +Hint Resolve transf_instr_freshreg_trans : htlspec. + +Lemma collect_trans_instr_freshreg_trans : + forall fin ret st l s s' i, + HTLMonadExtra.collectlist (transf_instr fin ret st) l s = OK tt s' i -> + s.(st_freshreg) = s'.(st_freshreg). +Proof. + intros. eapply collect_freshreg_trans; try eassumption. + eauto with htlspec. +Qed. + +Ltac rewrite_states := + match goal with + | [ H: ?x ?s = ?x ?s' |- _ ] => + let c1 := fresh "c" in + let c2 := fresh "c" in + remember (?x ?s) as c1; remember (?x ?s') as c2; try subst + end. + +Ltac inv_add_instr' H := + match type of H with + | ?f _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ = OK _ _ _ => unfold f in H + | ?f _ _ _ _ _ _ = OK _ _ _ => unfold f in H + end; repeat unfold_match H; inversion H. + +Ltac inv_add_instr := + match goal with + | H: (if ?c then _ else _) _ = OK _ _ _ |- _ => destruct c eqn:EQN; try discriminate; inv_add_instr + | H: context[add_instr_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_instr _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_instr _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_branch_instr _ _ _ _ _] |- _ => + inv_add_instr' H + | H: context[add_branch_instr _ _ _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + | H: context[add_node_skip _ _ _] |- _ => + inv_add_instr' H + | H: context[add_node_skip _ _] |- _ => + monadInv H; inv_incr; inv_add_instr + end. + +Ltac destruct_optional := + match goal with H: option ?r |- _ => destruct H end. + +Lemma iter_expand_instr_spec : + forall l fin rtrn stack s s' i x c, + HTLMonadExtra.collectlist (transf_instr fin rtrn stack) l s = OK x s' i -> + list_norepet (List.map fst l) -> + (forall pc instr, In (pc, instr) l -> c!pc = Some instr) -> + (forall pc instr, In (pc, instr) l -> + c!pc = Some instr -> + tr_code c pc instr s'.(st_datapath) s'.(st_controllogic) fin rtrn s'.(st_st) stack). +Proof. + induction l; simpl; intros; try contradiction. + destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr. + destruct (peq pc pc1). + - subst. + destruct instr1 eqn:?; try discriminate; + try destruct_optional; inv_add_instr; econstructor; try assumption. + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. inversion H9. rewrite H. apply tr_instr_Inop. + apply Z.leb_le. assumption. + eapply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. unfold nonblock. replace (st_st s4) with (st_st s2) by congruence. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. inversion H14. rewrite <- e2. replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply Z.leb_le; assumption. + apply EQ1. eapply in_map with (f := fst) in H14. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + econstructor. apply Z.leb_le; assumption. + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct H2. + * inversion H2. + replace (st_st s2) with (st_st s0) by congruence. + econstructor; try (apply Z.leb_le; apply andb_prop in EQN; apply EQN). + eauto with htlspec. + * apply in_map with (f := fst) in H2. contradiction. + + (*+ destruct o with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + destruct o0 with pc1; destruct H16; simpl in *; rewrite AssocMap.gss in H14; eauto; congruence. + + inversion H2. + * inversion H14. constructor. congruence. + * apply in_map with (f := fst) in H14. contradiction. + *) + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + + destruct o with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + destruct o0 with pc1; destruct H11; simpl in *; rewrite AssocMap.gss in H9; eauto; congruence. + + inversion H2. + * inversion H9. + replace (st_st s2) with (st_st s0) by congruence. + eauto with htlspec. + * apply in_map with (f := fst) in H9. contradiction. + + - eapply IHl. apply EQ0. assumption. + destruct H2. inversion H2. subst. contradiction. + intros. specialize H1 with pc0 instr0. destruct H1. tauto. trivial. + destruct H2. inv H2. contradiction. assumption. assumption. +Qed. +Hint Resolve iter_expand_instr_spec : htlspec. + +Lemma create_arr_inv : forall w x y z a b c d, + create_arr w x y z = OK (a, b) c d -> + y = b /\ a = z.(st_freshreg) /\ c.(st_freshreg) = Pos.succ (z.(st_freshreg)). +Proof. + inversion 1; split; auto. +Qed. + +Lemma create_reg_inv : forall a b s r s' i, + create_reg a b s = OK r s' i -> + r = s.(st_freshreg) /\ s'.(st_freshreg) = Pos.succ (s.(st_freshreg)). +Proof. + inversion 1; auto. +Qed. + +Theorem transl_module_correct : + forall f m, + transl_module f = Errors.OK m -> tr_module f m. +Proof. + intros until m. + unfold transl_module. + unfold run_mon. + destruct (transf_module f (max_state f)) eqn:?; try discriminate. + intros. inv H. + inversion s; subst. + + unfold transf_module in *. + unfold stack_correct in *. + destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; + destruct (RTL.fn_stacksize f + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlock + +(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass + [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) +let find_backedge i n = + let succ = RTL.successors_instr i in + List.filter (fun s -> P.lt n s) succ + +let find_backedges c = + +let prepend_instr i = function + | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} + +let rec bblock_from_RTL (c : RTL.code) i = + let succ = List.map (fun i -> PTree.get i c) (RTL.successors_instr i) in + match i, succ with + | RTL.Inop _, Some i::[] -> begin + match bblock_from_RTL c i with + | Errors.OK bb -> Errors.OK (prepend_instr RBnop bb) + | Errors.Error msg -> Errors.Error msg + end + | RTL.Iop (op, rs, dst, _), Some i::[] -> begin + match bblock_from_RTL c i with + | Errors.OK bb + end + +(* Partition a function and transform it into RTLBlock. *) +let function_from_RTL f = + { fn_sig = f.RTL.fn_entrypoint; + fn_stacksize = f.RTL.fn_stacksize; + fn_entrypoint = f.RTL.fn_entrypoint; + fn_code = f.RTL.fn_code + } diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml new file mode 100644 index 0000000..44f8b01 --- /dev/null +++ b/src/hls/PrintHTL.ml @@ -0,0 +1,81 @@ +(* -*- mode: tuareg -*- + * Vericert: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Value +open Datatypes +open Camlcoq +open AST +open Clflags +open Printf +open Maps +open AST +open HTL +open PrintAST +open PrintVerilog +open VericertClflags + +let pstr pp = fprintf pp "%s" + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let print_instruction pp (pc, i) = + fprintf pp "%5d:\t%s" pc (pprint_stmnt 0 i) + +let print_module pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.mod_params; + let datapath = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.mod_datapath)) in + let controllogic = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.mod_controllogic)) in + fprintf pp " datapath {\n"; + List.iter (print_instruction pp) datapath; + fprintf pp " }\n\n controllogic {\n"; + List.iter (print_instruction pp) controllogic; + fprintf pp " }\n}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_module pp id f + | _ -> () + +let print_program pp prog = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + print_program oc prog; + close_out oc diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml new file mode 100644 index 0000000..e69de29 diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml new file mode 100644 index 0000000..0f64066 --- /dev/null +++ b/src/hls/PrintVerilog.ml @@ -0,0 +1,232 @@ +(* -*- mode: tuareg -*- + * Vericert: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +open Verilog +open ValueInt +open Datatypes + +open Camlcoq +open AST +open Clflags + +open Printf + +open VericertClflags + +let concat = String.concat "" + +let indent i = String.make (2 * i) ' ' + +let fold_map f s = List.map f s |> concat + +let pstr pp = fprintf pp "%s" + +let pprint_binop l r = + let unsigned op = sprintf "{%s %s %s}" l op r in + let signed op = sprintf "{$signed(%s) %s $signed(%s)}" l op r in + function + | Vadd -> unsigned "+" + | Vsub -> unsigned "-" + | Vmul -> unsigned "*" + | Vdiv -> signed "/" + | Vdivu -> unsigned "/" + | Vmod -> signed "%" + | Vmodu -> unsigned "%" + | Vlt -> signed "<" + | Vltu -> unsigned "<" + | Vgt -> signed ">" + | Vgtu -> unsigned ">" + | Vle -> signed "<=" + | Vleu -> unsigned "<=" + | Vge -> signed ">=" + | Vgeu -> unsigned ">=" + | Veq -> unsigned "==" + | Vne -> unsigned "!=" + | Vand -> unsigned "&" + | Vor -> unsigned "|" + | Vxor -> unsigned "^" + | Vshl -> unsigned "<<" + | Vshr -> signed ">>>" + | Vshru -> unsigned ">>" + +let unop = function + | Vneg -> " ~ " + | Vnot -> " ! " + +let register a = sprintf "reg_%d" (P.to_int a) + +(*let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (uvalueToZ l))*) + +let literal l = sprintf "32'd%ld" (camlint_of_coqint l) + +let rec pprint_expr = function + | Vlit l -> literal l + | Vvar s -> register s + | Vvari (s, i) -> concat [register s; "["; pprint_expr i; "]"] + | Vinputvar s -> register s + | Vunop (u, e) -> concat ["("; unop u; pprint_expr e; ")"] + | Vbinop (op, a, b) -> concat [pprint_binop (pprint_expr a) (pprint_expr b) op] + | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] + +let rec pprint_stmnt i = + let pprint_case (e, s) = concat [ indent (i + 1); pprint_expr e; ": begin\n"; pprint_stmnt (i + 2) s; + indent (i + 1); "end\n" + ] + in function + | Vskip -> concat [indent i; ";\n"] + | Vseq (s1, s2) -> concat [ pprint_stmnt i s1; pprint_stmnt i s2] + | Vcond (e, st, sf) -> concat [ indent i; "if ("; pprint_expr e; ") begin\n"; + pprint_stmnt (i + 1) st; indent i; "end else begin\n"; + pprint_stmnt (i + 1) sf; + indent i; "end\n" + ] + | Vcase (e, es, d) -> concat [ indent i; "case ("; pprint_expr e; ")\n"; + fold_map pprint_case es; indent (i+1); "default:;\n"; + indent i; "endcase\n" + ] + | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"] + | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"] + +let rec pprint_edge = function + | Vposedge r -> concat ["posedge "; register r] + | Vnegedge r -> concat ["negedge "; register r] + | Valledge -> "*" + | Voredge (e1, e2) -> concat [pprint_edge e1; " or "; pprint_edge e2] + +let pprint_edge_top i = function + | Vposedge r -> concat ["@(posedge "; register r; ")"] + | Vnegedge r -> concat ["@(negedge "; register r; ")"] + | Valledge -> "@*" + | Voredge (e1, e2) -> concat ["@("; pprint_edge e1; " or "; pprint_edge e2; ")"] + +let declare t = + function (r, sz) -> + concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + register r; ";\n" ] + +let declarearr t = + function (r, sz, ln) -> + concat [ t; " ["; sprintf "%d" (Nat.to_int sz - 1); ":0] "; + register r; + " ["; sprintf "%d" (Nat.to_int ln - 1); ":0];\n" ] + +let print_io = function + | Some Vinput -> "input" + | Some Voutput -> "output reg" + | Some Vinout -> "inout" + | None -> "reg" + +let decl i = function + | Vdecl (io, r, sz) -> concat [indent i; declare (print_io io) (r, sz)] + | Vdeclarr (io, r, sz, ln) -> concat [indent i; declarearr (print_io io) (r, sz, ln)] + +(* TODO Fix always blocks, as they currently always print the same. *) +let pprint_module_item i = function + | Vdeclaration d -> decl i d + | Valways (e, s) -> + concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + | Valways_ff (e, s) -> + concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + | Valways_comb (e, s) -> + concat [indent i; "always "; pprint_edge_top i e; "\n"; pprint_stmnt (i+1) s] + +let rec intersperse c = function + | [] -> [] + | [x] -> [x] + | x :: xs -> x :: c :: intersperse c xs + +let make_io i io r = concat [indent i; io; " "; register r; ";\n"] + +let compose f g x = g x |> f + +let testbench = "module testbench; + reg start, reset, clk; + wire finish; + wire [31:0] return_val; + + main m(start, reset, clk, finish, return_val); + + initial begin + clk = 0; + start = 0; + reset = 0; + @(posedge clk) reset = 1; + @(posedge clk) reset = 0; + end + + always #5 clk = ~clk; + + always @(posedge clk) begin + if (finish == 1) begin + $display(\"finished: %d\", return_val); + $finish; + end + end +endmodule +" + +let debug_always i clk state = concat [ + indent i; "reg [31:0] count;\n"; + indent i; "initial count = 0;\n"; + indent i; "always @(posedge " ^ register clk ^ ") begin\n"; + indent (i+1); "if(count[0:0] == 10'd0) begin\n"; + indent (i+2); "$display(\"Cycle count %d\", count);\n"; + indent (i+2); "$display(\"State %d\\n\", " ^ register state ^ ");\n"; + indent (i+1); "end\n"; + indent (i+1); "count <= count + 1;\n"; + indent i; "end\n" + ] + +let print_initial i n stk = concat [ + indent i; "integer i;\n"; + indent i; "initial for(i = 0; i < "; sprintf "%d" n; "; i++)\n"; + indent (i+1); register stk; "[i] = 0;\n" + ] + +let pprint_module debug i n m = + if (extern_atom n) = "main" then + let inputs = m.mod_start :: m.mod_reset :: m.mod_clk :: m.mod_args in + let outputs = [m.mod_finish; m.mod_return] in + concat [ indent i; "module "; (extern_atom n); + "("; concat (intersperse ", " (List.map register (inputs @ outputs))); ");\n"; + fold_map (pprint_module_item (i+1)) m.mod_body; + if !option_initial then print_initial i (Nat.to_int m.mod_stk_len) m.mod_stk else ""; + if debug then debug_always i m.mod_clk m.mod_st else ""; + indent i; "endmodule\n\n" + ] + else "" + +let print_result pp lst = + let rec print_result_in pp = function + | [] -> fprintf pp "]\n" + | (r, v) :: ls -> + fprintf pp "%s -> %s; " (register r) (literal v); + print_result_in pp ls in + fprintf pp "[ "; + print_result_in pp lst + +let print_value pp v = fprintf pp "%s" (literal v) + +let print_globdef debug pp (id, gd) = + match gd with + | Gfun(Internal f) -> pstr pp (pprint_module debug 0 id f) + | _ -> () + +let print_program debug pp prog = + List.iter (print_globdef debug pp) prog.prog_defs; + pstr pp testbench diff --git a/src/hls/PrintVerilog.mli b/src/hls/PrintVerilog.mli new file mode 100644 index 0000000..6a15ee9 --- /dev/null +++ b/src/hls/PrintVerilog.mli @@ -0,0 +1,25 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +val pprint_stmnt : int -> Verilog.stmnt -> string + +val print_value : out_channel -> ValueInt.value -> unit + +val print_program : bool -> out_channel -> Verilog.program -> unit + +val print_result : out_channel -> (BinNums.positive * ValueInt.value) list -> unit diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v new file mode 100644 index 0000000..7169d4a --- /dev/null +++ b/src/hls/RTLBlock.v @@ -0,0 +1,69 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require Import + Coqlib + AST + Maps + Op + RTL + Registers. + +Definition node := positive. + +Inductive instruction : Type := +| RBnop : instruction +| RBop : operation -> list reg -> reg -> instruction +| RBload : memory_chunk -> addressing -> list reg -> reg -> instruction +| RBstore : memory_chunk -> addressing -> list reg -> reg -> instruction. + +Definition bblock_body : Type := list instruction. + +Inductive control_flow_inst : Type := +| RBcall : signature -> ident -> list reg -> reg -> node -> control_flow_inst +| RBtailcall : signature -> ident -> list reg -> control_flow_inst +| RBbuiltin : external_function -> list (builtin_arg reg) -> + builtin_res reg -> node -> control_flow_inst +| RBcond : condition -> list reg -> node -> node -> control_flow_inst +| RBjumptable : reg -> list node -> control_flow_inst +| RBredurn : option reg -> control_flow_inst. + +Record bblock : Type := mk_bblock { + bb_body: bblock_body; + bb_exit: option control_flow_inst + }. + +Definition code : Type := PTree.t bblock. + +Record function: Type := mkfunction { + fn_sig: signature; + fn_params: list reg; + fn_stacksize: Z; + fn_code: code; + fn_entrypoint: node +}. + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => fn_sig f + | External ef => ef_sig ef + end. diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v new file mode 100644 index 0000000..05f9a32 --- /dev/null +++ b/src/hls/RTLBlockgen.v @@ -0,0 +1,39 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require + RTL. +From compcert Require Import + AST + Maps. +From vericert Require Import + RTLBlock. + +Parameter partition : RTL.code -> code. + +Definition transl_function (f : RTL.function) : function := + mkfunction f.(RTL.fn_sig) + f.(RTL.fn_params) + f.(RTL.fn_stacksize) + (partition f.(RTL.fn_code)) + f.(RTL.fn_entrypoint). + +Definition transl_fundef := transf_fundef transl_function. + +Definition transl_program : RTL.program -> program := + transform_program transl_fundef. diff --git a/src/hls/Value.v b/src/hls/Value.v new file mode 100644 index 0000000..d6a3d8b --- /dev/null +++ b/src/hls/Value.v @@ -0,0 +1,551 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +(* begin hide *) +From bbv Require Import Word. +From bbv Require HexNotation WordScope. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. +From compcert Require Import lib.Integers common.Values. +From vericert Require Import Vericertlib. +(* end hide *) + +(** * Value + +A [value] is a bitvector with a specific size. We are using the implementation +of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. +However, we need to wrap it with an [Inductive] so that we can specify and match +on the size of the [value]. This is necessary so that we can easily store +[value]s of different sizes in a list or in a map. + +Using the default [word], this would not be possible, as the size is part of the type. *) + +Record value : Type := + mkvalue { + vsize: nat; + vword: word vsize + }. + +(** ** Value conversions + +Various conversions to different number types such as [N], [Z], [positive] and +[int], where the last one is a theory of integers of powers of 2 in CompCert. *) + +Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. + +Definition valueToWord : forall v : value, word (vsize v) := vword. + +Definition valueToNat (v :value) : nat := + wordToNat (vword v). + +Definition natToValue sz (n : nat) : value := + mkvalue sz (natToWord sz n). + +Definition valueToN (v : value) : N := + wordToN (vword v). + +Definition NToValue sz (n : N) : value := + mkvalue sz (NToWord sz n). + +Definition ZToValue (s : nat) (z : Z) : value := + mkvalue s (ZToWord s z). + +Definition valueToZ (v : value) : Z := + wordToZ (vword v). + +Definition uvalueToZ (v : value) : Z := + uwordToZ (vword v). + +Definition posToValue sz (p : positive) : value := + ZToValue sz (Zpos p). + +Definition posToValueAuto (p : positive) : value := + let size := Pos.to_nat (Pos.size p) in + ZToValue size (Zpos p). + +Definition valueToPos (v : value) : positive := + Z.to_pos (uvalueToZ v). + +Definition intToValue (i : Integers.int) : value := + ZToValue Int.wordsize (Int.unsigned i). + +Definition valueToInt (i : value) : Integers.int := + Int.repr (uvalueToZ i). + +Definition ptrToValue (i : Integers.ptrofs) : value := + ZToValue Ptrofs.wordsize (Ptrofs.unsigned i). + +Definition valueToPtr (i : value) : Integers.ptrofs := + Ptrofs.repr (uvalueToZ i). + +Definition valToValue (v : Values.val) : option value := + match v with + | Values.Vint i => Some (intToValue i) + | Values.Vptr b off => if Z.eqb (Z.modulo (uvalueToZ (ptrToValue off)) 4) 0%Z + then Some (ptrToValue off) + else None + | Values.Vundef => Some (ZToValue 32 0%Z) + | _ => None + end. + +(** Convert a [value] to a [bool], so that choices can be made based on the +result. This is also because comparison operators will give back [value] instead +of [bool], so if they are in a condition, they will have to be converted before +they can be used. *) + +Definition valueToBool (v : value) : bool := + negb (weqb (@wzero (vsize v)) (vword v)). + +Definition boolToValue (sz : nat) (b : bool) : value := + natToValue sz (if b then 1 else 0). + +(** ** Arithmetic operations *) + +Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +intros; subst; assumption. Defined. + +Lemma unify_word_unfold : + forall sz w, + unify_word sz sz w eq_refl = w. +Proof. auto. Qed. + +Definition value_eq_size: + forall v1 v2 : value, { vsize v1 = vsize v2 } + { True }. +Proof. + intros; destruct (Nat.eqb (vsize v1) (vsize v2)) eqn:?. + left; apply Nat.eqb_eq in Heqb; assumption. + right; trivial. +Defined. + +Definition map_any {A : Type} (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) + (EQ : vsize v1 = vsize v2) : A := + let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in + f (vword v1) w2. + +Definition map_any_opt {A : Type} (sz : nat) (v1 v2 : value) (f : word (vsize v1) -> word (vsize v1) -> A) + : option A := + match value_eq_size v1 v2 with + | left EQ => + Some (map_any v1 v2 f EQ) + | _ => None + end. + +Definition map_word (f : forall sz : nat, word sz -> word sz) (v : value) : value := + mkvalue (vsize v) (f (vsize v) (vword v)). + +Definition map_word2 (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) + (EQ : (vsize v1 = vsize v2)) : value := + let w2 := unify_word (vsize v1) (vsize v2) (vword v2) EQ in + mkvalue (vsize v1) (f (vsize v1) (vword v1) w2). + +Definition map_word2_opt (f : forall sz : nat, word sz -> word sz -> word sz) (v1 v2 : value) + : option value := + match value_eq_size v1 v2 with + | left EQ => Some (map_word2 f v1 v2 EQ) + | _ => None + end. + +Definition eq_to_opt (v1 v2 : value) (f : vsize v1 = vsize v2 -> value) + : option value := + match value_eq_size v1 v2 with + | left EQ => Some (f EQ) + | _ => None + end. + +Lemma eqvalue {sz : nat} (x y : word sz) : x = y <-> mkvalue sz x = mkvalue sz y. +Proof. + split; intros. + subst. reflexivity. inversion H. apply existT_wordToZ in H1. + apply wordToZ_inj. assumption. +Qed. + +Lemma eqvaluef {sz : nat} (x y : word sz) : x = y -> mkvalue sz x = mkvalue sz y. +Proof. apply eqvalue. Qed. + +Lemma nevalue {sz : nat} (x y : word sz) : x <> y <-> mkvalue sz x <> mkvalue sz y. +Proof. split; intros; intuition. apply H. apply eqvalue. assumption. + apply H. rewrite H0. trivial. +Qed. + +Lemma nevaluef {sz : nat} (x y : word sz) : x <> y -> mkvalue sz x <> mkvalue sz y. +Proof. apply nevalue. Qed. + +(*Definition rewrite_word_size (initsz finalsz : nat) (w : word initsz) + : option (word finalsz) := + match Nat.eqb initsz finalsz return option (word finalsz) with + | true => Some _ + | false => None + end.*) + +Definition valueeq (sz : nat) (x y : word sz) : + {mkvalue sz x = mkvalue sz y} + {mkvalue sz x <> mkvalue sz y} := + match weq x y with + | left eq => left (eqvaluef x y eq) + | right ne => right (nevaluef x y ne) + end. + +Definition valueeqb (x y : value) : bool := + match value_eq_size x y with + | left EQ => + weqb (vword x) (unify_word (vsize x) (vsize y) (vword y) EQ) + | right _ => false + end. + +Definition value_projZ_eqb (v1 v2 : value) : bool := Z.eqb (valueToZ v1) (valueToZ v2). + +Theorem value_projZ_eqb_true : + forall v1 v2, + v1 = v2 -> value_projZ_eqb v1 v2 = true. +Proof. intros. subst. unfold value_projZ_eqb. apply Z.eqb_eq. trivial. Qed. + +Theorem valueeqb_true_iff : + forall v1 v2, + valueeqb v1 v2 = true <-> v1 = v2. +Proof. + split; intros. + unfold valueeqb in H. destruct (value_eq_size v1 v2) eqn:?. + - destruct v1, v2. simpl in H. +Abort. + +Definition value_int_eqb (v : value) (i : int) : bool := + Z.eqb (valueToZ v) (Int.unsigned i). + +(** Arithmetic operations over [value], interpreting them as signed or unsigned +depending on the operation. + +The arithmetic operations over [word] are over [N] by default, however, can also +be called over [Z] explicitly, which is where the bits are interpreted in a +signed manner. *) + +Definition vplus v1 v2 := map_word2 wplus v1 v2. +Definition vplus_opt v1 v2 := map_word2_opt wplus v1 v2. +Definition vminus v1 v2 := map_word2 wminus v1 v2. +Definition vmul v1 v2 := map_word2 wmult v1 v2. +Definition vdiv v1 v2 := map_word2 wdiv v1 v2. +Definition vmod v1 v2 := map_word2 wmod v1 v2. + +Definition vmuls v1 v2 := map_word2 wmultZ v1 v2. +Definition vdivs v1 v2 := map_word2 wdivZ v1 v2. +Definition vmods v1 v2 := map_word2 wremZ v1 v2. + +(** ** Bitwise operations + +Bitwise operations over [value], which is independent of whether the number is +signed or unsigned. *) + +Definition vnot v := map_word wnot v. +Definition vneg v := map_word wneg v. +Definition vbitneg v := boolToValue (vsize v) (negb (valueToBool v)). +Definition vor v1 v2 := map_word2 wor v1 v2. +Definition vand v1 v2 := map_word2 wand v1 v2. +Definition vxor v1 v2 := map_word2 wxor v1 v2. + +(** ** Comparison operators + +Comparison operators that return a bool, there should probably be an equivalent +which returns another number, however I might just add that as an explicit +conversion. *) + +Definition veqb v1 v2 := map_any v1 v2 (@weqb (vsize v1)). +Definition vneb v1 v2 EQ := negb (veqb v1 v2 EQ). + +Definition veq v1 v2 EQ := boolToValue (vsize v1) (veqb v1 v2 EQ). +Definition vne v1 v2 EQ := boolToValue (vsize v1) (vneb v1 v2 EQ). + +Definition vltb v1 v2 := map_any v1 v2 wltb. +Definition vleb v1 v2 EQ := negb (map_any v2 v1 wltb (eq_sym EQ)). +Definition vgtb v1 v2 EQ := map_any v2 v1 wltb (eq_sym EQ). +Definition vgeb v1 v2 EQ := negb (map_any v1 v2 wltb EQ). + +Definition vltsb v1 v2 := map_any v1 v2 wsltb. +Definition vlesb v1 v2 EQ := negb (map_any v2 v1 wsltb (eq_sym EQ)). +Definition vgtsb v1 v2 EQ := map_any v2 v1 wsltb (eq_sym EQ). +Definition vgesb v1 v2 EQ := negb (map_any v1 v2 wsltb EQ). + +Definition vlt v1 v2 EQ := boolToValue (vsize v1) (vltb v1 v2 EQ). +Definition vle v1 v2 EQ := boolToValue (vsize v1) (vleb v1 v2 EQ). +Definition vgt v1 v2 EQ := boolToValue (vsize v1) (vgtb v1 v2 EQ). +Definition vge v1 v2 EQ := boolToValue (vsize v1) (vgeb v1 v2 EQ). + +Definition vlts v1 v2 EQ := boolToValue (vsize v1) (vltsb v1 v2 EQ). +Definition vles v1 v2 EQ := boolToValue (vsize v1) (vlesb v1 v2 EQ). +Definition vgts v1 v2 EQ := boolToValue (vsize v1) (vgtsb v1 v2 EQ). +Definition vges v1 v2 EQ := boolToValue (vsize v1) (vgesb v1 v2 EQ). + +(** ** Shift operators + +Shift operators on values. *) + +Definition shift_map (sz : nat) (f : word sz -> nat -> word sz) (w1 w2 : word sz) := + f w1 (wordToNat w2). + +Definition vshl v1 v2 := map_word2 (fun sz => shift_map sz (@wlshift sz)) v1 v2. +Definition vshr v1 v2 := map_word2 (fun sz => shift_map sz (@wrshift sz)) v1 v2. + +Module HexNotationValue. + Export HexNotation. + Import WordScope. + + Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). + +End HexNotationValue. + +Inductive val_value_lessdef: val -> value -> Prop := +| val_value_lessdef_int: + forall i v', + i = valueToInt v' -> + val_value_lessdef (Vint i) v' +| val_value_lessdef_ptr: + forall b off v', + off = valueToPtr v' -> + (Z.modulo (uvalueToZ v') 4) = 0%Z -> + val_value_lessdef (Vptr b off) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. + +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + +Lemma valueToZ_ZToValue : + forall n z, + (- Z.of_nat (2 ^ n) <= z < Z.of_nat (2 ^ n))%Z -> + valueToZ (ZToValue (S n) z) = z. +Proof. + unfold valueToZ, ZToValue. simpl. + auto using wordToZ_ZToWord. +Qed. + +Lemma uvalueToZ_ZToValue : + forall n z, + (0 <= z < 2 ^ Z.of_nat n)%Z -> + uvalueToZ (ZToValue n z) = z. +Proof. + unfold uvalueToZ, ZToValue. simpl. + auto using uwordToZ_ZToWord. +Qed. + +Lemma uvalueToZ_ZToValue_full : + forall sz : nat, + (0 < sz)%nat -> + forall z : Z, uvalueToZ (ZToValue sz z) = (z mod 2 ^ Z.of_nat sz)%Z. +Proof. unfold uvalueToZ, ZToValue. simpl. auto using uwordToZ_ZToWord_full. Qed. + +Lemma ZToValue_uvalueToZ : + forall v, + ZToValue (vsize v) (uvalueToZ v) = v. +Proof. + intros. + unfold ZToValue, uvalueToZ. + rewrite ZToWord_uwordToZ. destruct v; auto. +Qed. + +Lemma valueToPos_posToValueAuto : + forall p, valueToPos (posToValueAuto p) = p. +Proof. + intros. unfold valueToPos, posToValueAuto. + rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. + split. apply Zle_0_pos. + + assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. + inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. + simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. +Qed. + +Lemma valueToPos_posToValue : + forall p, valueToPos (posToValueAuto p) = p. +Proof. + intros. unfold valueToPos, posToValueAuto. + rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. + split. apply Zle_0_pos. + + assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. + inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. + simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. +Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. + intros. + unfold valueToInt, intToValue. rewrite uvalueToZ_ZToValue. auto using Int.repr_unsigned. + split. apply Int.unsigned_range_2. + assert ((Int.unsigned v <= Int.max_unsigned)%Z) by apply Int.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma valueToPtr_ptrToValue : + forall v, + valueToPtr (ptrToValue v) = v. +Proof. + intros. + unfold valueToPtr, ptrToValue. rewrite uvalueToZ_ZToValue. auto using Ptrofs.repr_unsigned. + split. apply Ptrofs.unsigned_range_2. + assert ((Ptrofs.unsigned v <= Ptrofs.max_unsigned)%Z) by apply Ptrofs.unsigned_range_2. + apply Z.lt_le_pred in H. apply H. +Qed. + +Lemma intToValue_valueToInt : + forall v, + vsize v = 32%nat -> + intToValue (valueToInt v) = v. +Proof. + intros. unfold valueToInt, intToValue. rewrite Int.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Int.modulus. unfold Int.wordsize. unfold Wordsize_32.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + +Lemma ptrToValue_valueToPtr : + forall v, + vsize v = 32%nat -> + ptrToValue (valueToPtr v) = v. +Proof. + intros. unfold valueToPtr, ptrToValue. rewrite Ptrofs.unsigned_repr_eq. + unfold ZToValue, uvalueToZ. unfold Ptrofs.modulus. unfold Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. + pose proof (uwordToZ_bound (vword v)). + rewrite Z.mod_small. rewrite <- H. rewrite ZToWord_uwordToZ. destruct v; auto. + rewrite <- H. rewrite two_power_nat_equiv. apply H0. +Qed. + +Lemma valToValue_lessdef : + forall v v', + valToValue v = Some v' -> + val_value_lessdef v v'. +Proof. + intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. + symmetry. apply valueToInt_intToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. + inv H1. symmetry. apply valueToPtr_ptrToValue. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. + inv H1. apply Z.eqb_eq. apply Heqb0. +Qed. + +Lemma boolToValue_ValueToBool : + forall b, + valueToBool (boolToValue 32 b) = b. +Proof. destruct b; auto. Qed. + +Local Open Scope Z. + +Ltac word_op_value H := + intros; unfold uvalueToZ, ZToValue; simpl; rewrite unify_word_unfold; + rewrite <- H; rewrite uwordToZ_ZToWord_full; auto; omega. + +Lemma zadd_vplus : + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vplus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 + z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_plus. Qed. + +Lemma zadd_vplus2 : + forall z1 z2, + vplus (ZToValue 32 z1) (ZToValue 32 z2) eq_refl = ZToValue 32 (z1 + z2). +Proof. + intros. unfold vplus, ZToValue, map_word2. rewrite unify_word_unfold. simpl. + rewrite ZToWord_plus; auto. +Qed. + +Lemma ZToValue_eq : + forall w1, + (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Abort. + +Lemma wordsize_32 : + Int.wordsize = 32%nat. +Proof. auto. Qed. + +Lemma intadd_vplus : + forall i1 i2, + valueToInt (vplus (intToValue i1) (intToValue i2) eq_refl) = Int.add i1 i2. +Proof. + intros. unfold Int.add, valueToInt, intToValue. rewrite zadd_vplus. + rewrite <- Int.unsigned_repr_eq. + rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. +Qed. + +(*Lemma intadd_vplus2 : + forall v1 v2 EQ, + vsize v1 = 32%nat -> + Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). +Proof. + intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). + rewrite (@vadd_vplus v1 v2 EQ). trivial. + unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)). + rewrite H in EQ. rewrite <- EQ in H0 at 3.*) + (*rewrite zadd_vplus3. trivia*) + +Lemma valadd_vplus : + forall v1 v2 v1' v2' v v' EQ, + val_value_lessdef v1 v1' -> + val_value_lessdef v2 v2' -> + Val.add v1 v2 = v -> + vplus v1' v2' EQ = v' -> + val_value_lessdef v v'. +Proof. + intros. inv H; inv H0; constructor; simplify. + Abort. + +Lemma zsub_vminus : + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vminus (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 - z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_minus. Qed. + +Lemma zmul_vmul : + forall sz z1 z2, + (sz > 0)%nat -> + uvalueToZ (vmul (ZToValue sz z1) (ZToValue sz z2) eq_refl) = (z1 * z2) mod 2 ^ Z.of_nat sz. +Proof. word_op_value ZToWord_mult. Qed. + +Local Open Scope N. +Lemma zdiv_vdiv : + forall n1 n2, + n1 < 2 ^ 32 -> + n2 < 2 ^ 32 -> + n1 / n2 < 2 ^ 32 -> + valueToN (vdiv (NToValue 32 n1) (NToValue 32 n2) eq_refl) = n1 / n2. +Proof. + intros; unfold valueToN, NToValue; simpl; rewrite unify_word_unfold. unfold wdiv. + unfold wordBin. repeat (rewrite wordToN_NToWord_2); auto. +Qed. + +Lemma ZToValue_valueToNat : + forall x sz, + (sz > 0)%nat -> + (0 <= x < 2^(Z.of_nat sz))%Z -> + valueToNat (ZToValue sz x) = Z.to_nat x. +Proof. + destruct x; intros; unfold ZToValue, valueToNat; crush. + - rewrite wzero'_def. apply wordToNat_wzero. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. + clear H1. + lazymatch goal with + | [ H : context[(_ < ?x)%Z] |- _ ] => replace x with (Z.of_nat (Z.to_nat x)) in H + end. + 2: { apply Z2Nat.id; apply Z.pow_nonneg; lia. } + + rewrite Z2Nat.inj_pow in H2; crush. + replace (Pos.to_nat 2) with 2%nat in H2 by reflexivity. + rewrite Nat2Z.id in H2. + rewrite <- positive_nat_Z in H2. + apply Nat2Z.inj_lt in H2. + assumption. +Qed. diff --git a/src/hls/ValueInt.v b/src/hls/ValueInt.v new file mode 100644 index 0000000..f1fd056 --- /dev/null +++ b/src/hls/ValueInt.v @@ -0,0 +1,167 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +(* begin hide *) +From bbv Require Import Word. +From bbv Require HexNotation WordScope. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. +From compcert Require Import lib.Integers common.Values. +From vericert Require Import Vericertlib. +(* end hide *) + +(** * Value + +A [value] is a bitvector with a specific size. We are using the implementation +of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse. +However, we need to wrap it with an [Inductive] so that we can specify and match +on the size of the [value]. This is necessary so that we can easily store +[value]s of different sizes in a list or in a map. + +Using the default [word], this would not be possible, as the size is part of the type. *) + +Definition value : Type := int. + +(** ** Value conversions + +Various conversions to different number types such as [N], [Z], [positive] and +[int], where the last one is a theory of integers of powers of 2 in CompCert. *) + +Definition valueToNat (v : value) : nat := + Z.to_nat (Int.unsigned v). + +Definition natToValue (n : nat) : value := + Int.repr (Z.of_nat n). + +Definition valueToN (v : value) : N := + Z.to_N (Int.unsigned v). + +Definition NToValue (n : N) : value := + Int.repr (Z.of_N n). + +Definition ZToValue (z : Z) : value := + Int.repr z. + +Definition valueToZ (v : value) : Z := + Int.signed v. + +Definition uvalueToZ (v : value) : Z := + Int.unsigned v. + +Definition posToValue (p : positive) : value := + Int.repr (Z.pos p). + +Definition valueToPos (v : value) : positive := + Z.to_pos (Int.unsigned v). + +Definition intToValue (i : Integers.int) : value := i. + +Definition valueToInt (i : value) : Integers.int := i. + +Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i. + +Definition valueToPtr (i : value) : Integers.ptrofs := + Ptrofs.of_int i. + +Definition valToValue (v : Values.val) : option value := + match v with + | Values.Vint i => Some (intToValue i) + | Values.Vptr b off => Some (ptrToValue off) + | Values.Vundef => Some (ZToValue 0%Z) + | _ => None + end. + +(** Convert a [value] to a [bool], so that choices can be made based on the +result. This is also because comparison operators will give back [value] instead +of [bool], so if they are in a condition, they will have to be converted before +they can be used. *) + +Definition valueToBool (v : value) : bool := + if Z.eqb (uvalueToZ v) 0 then false else true. + +Definition boolToValue (b : bool) : value := + natToValue (if b then 1 else 0). + +(** ** Arithmetic operations *) + +Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. +intros; subst; assumption. Defined. + +Lemma unify_word_unfold : + forall sz w, + unify_word sz sz w eq_refl = w. +Proof. auto. Qed. + +Inductive val_value_lessdef: val -> value -> Prop := +| val_value_lessdef_int: + forall i v', + i = valueToInt v' -> + val_value_lessdef (Vint i) v' +| val_value_lessdef_ptr: + forall b off v', + off = valueToPtr v' -> + val_value_lessdef (Vptr b off) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. + +Inductive opt_val_value_lessdef: option val -> value -> Prop := +| opt_lessdef_some: + forall v v', val_value_lessdef v v' -> opt_val_value_lessdef (Some v) v' +| opt_lessdef_none: forall v, opt_val_value_lessdef None v. + +Lemma valueToZ_ZToValue : + forall z, + (Int.min_signed <= z <= Int.max_signed)%Z -> + valueToZ (ZToValue z) = z. +Proof. auto using Int.signed_repr. Qed. + +Lemma uvalueToZ_ZToValue : + forall z, + (0 <= z <= Int.max_unsigned)%Z -> + uvalueToZ (ZToValue z) = z. +Proof. auto using Int.unsigned_repr. Qed. + +Lemma valueToPos_posToValue : + forall v, + 0 <= Z.pos v <= Int.max_unsigned -> + valueToPos (posToValue v) = v. +Proof. + unfold valueToPos, posToValue. + intros. rewrite Int.unsigned_repr. + apply Pos2Z.id. assumption. +Qed. + +Lemma valueToInt_intToValue : + forall v, + valueToInt (intToValue v) = v. +Proof. auto. Qed. + +Lemma valToValue_lessdef : + forall v v', + valToValue v = Some v' -> + val_value_lessdef v v'. +Proof. + intros. + destruct v; try discriminate; constructor. + unfold valToValue in H. inversion H. + unfold valueToInt. unfold intToValue in H1. auto. + inv H. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. +Qed. + +Ltac simplify_val := repeat (simplify; unfold uvalueToZ, valueToPtr, Ptrofs.of_int, valueToInt, intToValue, + ptrToValue in *). + +Ltac crush_val := simplify_val; try discriminate; try congruence; try lia; liapp; try assumption. diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v new file mode 100644 index 0000000..c5dab9e --- /dev/null +++ b/src/hls/Verilog.v @@ -0,0 +1,893 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From Coq Require Import + Structures.OrderedTypeEx + FSets.FMapPositive + Program.Basics + PeanoNat + ZArith + Lists.List + Program. + +Require Import Lia. + +Import ListNotations. + +From vericert Require Import Vericertlib Show ValueInt AssocMap Array. +From compcert Require Events. +From compcert Require Import Integers Errors Smallstep Globalenvs. + +Local Open Scope assocmap. + +Set Implicit Arguments. + +Definition reg : Type := positive. +Definition node : Type := positive. +Definition szreg : Type := reg * nat. + +Record associations (A : Type) : Type := + mkassociations { + assoc_blocking : AssocMap.t A; + assoc_nonblocking : AssocMap.t A + }. + +Definition arr := (Array (option value)). + +Definition reg_associations := associations value. +Definition arr_associations := associations arr. + +Definition assocmap_reg := AssocMap.t value. +Definition assocmap_arr := AssocMap.t arr. + +Definition merge_regs (new : assocmap_reg) (old : assocmap_reg) : assocmap_reg := + AssocMapExt.merge value new old. + +Definition merge_cell (new : option value) (old : option value) : option value := + match new, old with + | Some _, _ => new + | _, _ => old + end. + +Definition merge_arr (new : option arr) (old : option arr) : option arr := + match new, old with + | Some new', Some old' => Some (combine merge_cell new' old') + | Some new', None => Some new' + | None, Some old' => Some old' + | None, None => None + end. + +Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr := + AssocMap.combine merge_arr new old. + +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := + match a ! r with + | None => None + | Some arr => Some (Option.default (NToValue 0) (Option.join (array_get_error i arr))) + end. + +Definition arr_assocmap_set (r : reg) (i : nat) (v : value) (a : assocmap_arr) : assocmap_arr := + match a ! r with + | None => a + | Some arr => a # r <- (array_set i (Some v) arr) + end. + +Definition block_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := + mkassociations (arr_assocmap_set r i v asa.(assoc_blocking)) asa.(assoc_nonblocking). + +Definition nonblock_arr (r : reg) (i : nat) (asa : arr_associations) (v : value) : arr_associations := + mkassociations asa.(assoc_blocking) (arr_assocmap_set r i v asa.(assoc_nonblocking)). + +Definition block_reg (r : reg) (asr : reg_associations) (v : value) := + mkassociations (AssocMap.set r v asr.(assoc_blocking)) asr.(assoc_nonblocking). + +Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) := + mkassociations asr.(assoc_blocking) (AssocMap.set r v asr.(assoc_nonblocking)). + +Inductive scl_decl : Type := VScalar (sz : nat). +Inductive arr_decl : Type := VArray (sz : nat) (ln : nat). + +(** * Verilog AST + +The Verilog AST is defined here, which is the target language of the +compilation. + +** Value + +The Verilog [value] is a bitvector containg a size and the actual bitvector. In +this case, the [Word.word] type is used as many theorems about that bitvector +have already been proven. *) + +(** ** Binary Operators + +These are the binary operations that can be represented in Verilog. Ideally, +multiplication and division would be done by custom modules which could al so be +scheduled properly. However, for now every Verilog operator is assumed to take +one clock cycle. *) + +Inductive binop : Type := +| Vadd : binop (** addition (binary [+]) *) +| Vsub : binop (** subtraction (binary [-]) *) +| Vmul : binop (** multiplication (binary [*]) *) +| Vdiv : binop (** division (binary [/]) *) +| Vdivu : binop (** division unsigned (binary [/]) *) +| Vmod : binop (** remainder ([%]) *) +| Vmodu : binop (** remainder unsigned ([%]) *) +| Vlt : binop (** less than ([<]) *) +| Vltu : binop (** less than unsigned ([<]) *) +| Vgt : binop (** greater than ([>]) *) +| Vgtu : binop (** greater than unsigned ([>]) *) +| Vle : binop (** less than or equal ([<=]) *) +| Vleu : binop (** less than or equal unsigned ([<=]) *) +| Vge : binop (** greater than or equal ([>=]) *) +| Vgeu : binop (** greater than or equal unsigned ([>=]) *) +| Veq : binop (** equal to ([==]) *) +| Vne : binop (** not equal to ([!=]) *) +| Vand : binop (** and (binary [&]) *) +| Vor : binop (** or (binary [|]) *) +| Vxor : binop (** xor (binary [^|]) *) +| Vshl : binop (** shift left ([<<]) *) +| Vshr : binop (** shift right ([>>>]) *) +| Vshru : binop. (** shift right unsigned ([>>]) *) +(*| Vror : binop (** shift right unsigned ([>>]) *)*) + +(** ** Unary Operators *) + +Inductive unop : Type := +| Vneg (** negation ([~]) *) +| Vnot. (** not operation [!] *) + +(** ** Expressions *) + +Inductive expr : Type := +| Vlit : value -> expr +| Vvar : reg -> expr +| Vvari : reg -> expr -> expr +| Vinputvar : reg -> expr +| Vbinop : binop -> expr -> expr -> expr +| Vunop : unop -> expr -> expr +| Vternary : expr -> expr -> expr -> expr. + +Definition posToExpr (p : positive) : expr := + Vlit (posToValue p). + +(** ** Statements *) + +Inductive stmnt : Type := +| Vskip : stmnt +| Vseq : stmnt -> stmnt -> stmnt +| Vcond : expr -> stmnt -> stmnt -> stmnt +| Vcase : expr -> list (expr * stmnt) -> option stmnt -> stmnt +| Vblock : expr -> expr -> stmnt +| Vnonblock : expr -> expr -> stmnt. + +(** ** Edges + +These define when an always block should be triggered, for example if the always +block should be triggered synchronously at the clock edge, or asynchronously for +combinational logic. + +[edge] is not part of [stmnt] in this formalisation because is closer to the +semantics that are used. *) + +Inductive edge : Type := +| Vposedge : reg -> edge +| Vnegedge : reg -> edge +| Valledge : edge +| Voredge : edge -> edge -> edge. + +(** ** Module Items + +Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). +The declarations are always register declarations as combinational logic can be +done using combinational always block instead of continuous assignments. *) + +Inductive io : Type := +| Vinput : io +| Voutput : io +| Vinout : io. + +Inductive declaration : Type := +| Vdecl : option io -> reg -> nat -> declaration +| Vdeclarr : option io -> reg -> nat -> nat -> declaration. + +Inductive module_item : Type := +| Vdeclaration : declaration -> module_item +| Valways : edge -> stmnt -> module_item +| Valways_ff : edge -> stmnt -> module_item +| Valways_comb : edge -> stmnt -> module_item. + +(** The main module type containing all the important control signals + +- [mod_start] If set, starts the computations in the module. +- [mod_reset] If set, reset the state in the module. +- [mod_clk] The clock that controls the computation in the module. +- [mod_args] The arguments to the module. +- [mod_finish] Bit that is set if the result is ready. +- [mod_return] The return value that was computed. +- [mod_body] The body of the module, including the state machine. +*) + +Record module : Type := mkmodule { + mod_start : reg; + mod_reset : reg; + mod_clk : reg; + mod_finish : reg; + mod_return : reg; + mod_st : reg; (**r Variable that defines the current state, it should be internal. *) + mod_stk : reg; + mod_stk_len : nat; + mod_args : list reg; + mod_body : list module_item; + mod_entrypoint : node; +}. + +Definition fundef := AST.fundef module. + +Definition program := AST.program fundef unit. + +(** Convert a [positive] to an expression directly, setting it to the right + size. *) +Definition posToLit (p : positive) : expr := + Vlit (posToValue p). + +Definition fext := unit. +Definition fextclk := nat -> fext. + +(** ** State + +The [state] contains the following items: +n +- Current [module] that is being worked on, so that the state variable can be +retrieved and set appropriately. +- Current [module_item] which is being worked on. +- A contiunation ([cont]) which defines what to do next. The option is to + either evaluate another module item or go to the next clock cycle. Finally + it could also end if the finish flag of the module goes high. +- Association list containing the blocking assignments made, or assignments made + in previous clock cycles. +- Nonblocking association list containing all the nonblocking assignments made + in the current module. +- The environment containing values for the input. +- The program counter which determines the value for the state in this version of + Verilog, as the Verilog was generated by the RTL, which means that we have to + make an assumption about how it looks. In this case, that it contains state + which determines which part of the Verilog is executed. This is then the part + of the Verilog that should match with the RTL. *) + +Inductive stackframe : Type := + Stackframe : + forall (res : reg) + (m : module) + (pc : node) + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), + stackframe. + +Inductive state : Type := +| State : + forall (stack : list stackframe) + (m : module) + (st : node) + (reg_assoc : assocmap_reg) + (arr_assoc : assocmap_arr), state +| Returnstate : + forall (res : list stackframe) + (v : value), state +| Callstate : + forall (stack : list stackframe) + (m : module) + (args : list value), state. + +Definition binop_run (op : binop) (v1 v2 : value) : option value := + match op with + | Vadd => Some (Int.add v1 v2) + | Vsub => Some (Int.sub v1 v2) + | Vmul => Some (Int.mul v1 v2) + | Vdiv => if Int.eq v2 Int.zero + || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone + then None + else Some (Int.divs v1 v2) + | Vdivu => if Int.eq v2 Int.zero then None else Some (Int.divu v1 v2) + | Vmod => if Int.eq v2 Int.zero + || Int.eq v1 (Int.repr Int.min_signed) && Int.eq v2 Int.mone + then None + else Some (Int.mods v1 v2) + | Vmodu => if Int.eq v2 Int.zero then None else Some (Int.modu v1 v2) + | Vlt => Some (boolToValue (Int.lt v1 v2)) + | Vltu => Some (boolToValue (Int.ltu v1 v2)) + | Vgt => Some (boolToValue (Int.lt v2 v1)) + | Vgtu => Some (boolToValue (Int.ltu v2 v1)) + | Vle => Some (boolToValue (negb (Int.lt v2 v1))) + | Vleu => Some (boolToValue (negb (Int.ltu v2 v1))) + | Vge => Some (boolToValue (negb (Int.lt v1 v2))) + | Vgeu => Some (boolToValue (negb (Int.ltu v1 v2))) + | Veq => Some (boolToValue (Int.eq v1 v2)) + | Vne => Some (boolToValue (negb (Int.eq v1 v2))) + | Vand => Some (Int.and v1 v2) + | Vor => Some (Int.or v1 v2) + | Vxor => Some (Int.xor v1 v2) + | Vshl => Some (Int.shl v1 v2) + | Vshr => Some (Int.shr v1 v2) + | Vshru => Some (Int.shru v1 v2) + end. + +Definition unop_run (op : unop) (v1 : value) : value := + match op with + | Vneg => Int.neg v1 + | Vnot => Int.not v1 + end. + +Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop := + | erun_Vlit : + forall fext reg stack v, + expr_runp fext reg stack (Vlit v) v + | erun_Vvar : + forall fext reg stack v r, + reg#r = v -> + expr_runp fext reg stack (Vvar r) v + | erun_Vvari : + forall fext reg stack v iexp i r, + expr_runp fext reg stack iexp i -> + arr_assocmap_lookup stack r (valueToNat i) = Some v -> + expr_runp fext reg stack (Vvari r iexp) v + | erun_Vbinop : + forall fext reg stack op l r lv rv resv, + expr_runp fext reg stack l lv -> + expr_runp fext reg stack r rv -> + Some resv = binop_run op lv rv -> + expr_runp fext reg stack (Vbinop op l r) resv + | erun_Vunop : + forall fext reg stack u vu op oper resv, + expr_runp fext reg stack u vu -> + oper = unop_run op -> + resv = oper vu -> + expr_runp fext reg stack (Vunop op u) resv + | erun_Vternary_true : + forall fext reg stack c ts fs vc vt, + expr_runp fext reg stack c vc -> + expr_runp fext reg stack ts vt -> + valueToBool vc = true -> + expr_runp fext reg stack (Vternary c ts fs) vt + | erun_Vternary_false : + forall fext reg stack c ts fs vc vf, + expr_runp fext reg stack c vc -> + expr_runp fext reg stack fs vf -> + valueToBool vc = false -> + expr_runp fext reg stack (Vternary c ts fs) vf. +Hint Constructors expr_runp : verilog. + +Definition handle_opt {A : Type} (err : errmsg) (val : option A) + : res A := + match val with + | Some a => OK a + | None => Error err + end. + +Definition handle_def {A : Type} (a : A) (val : option A) + : res A := + match val with + | Some a' => OK a' + | None => OK a + end. + +Local Open Scope error_monad_scope. + +(*Definition access_fext (f : fext) (r : reg) : res value := + match AssocMap.get r f with + | Some v => OK v + | _ => OK (ZToValue 0) + end.*) + +(* TODO FIX Vvar case without default *) +(*Fixpoint expr_run (assoc : assocmap) (e : expr) + {struct e} : res value := + match e with + | Vlit v => OK v + | Vvar r => match s with + | State _ assoc _ _ _ => handle_def (ZToValue 32 0) assoc!r + | _ => Error (msg "Verilog: Wrong state") + end + | Vvari _ _ => Error (msg "Verilog: variable indexing not modelled") + | Vinputvar r => access_fext s r + | Vbinop op l r => + let lv := expr_run s l in + let rv := expr_run s r in + let oper := binop_run op in + do lv' <- lv; + do rv' <- rv; + handle_opt (msg "Verilog: sizes are not equal") + (eq_to_opt lv' rv' (oper lv' rv')) + | Vunop op e => + let oper := unop_run op in + do ev <- expr_run s e; + OK (oper ev) + | Vternary c te fe => + do cv <- expr_run s c; + if valueToBool cv then expr_run s te else expr_run s fe + end.*) + +(** Return the location of the lhs of an assignment. *) + +Inductive location : Type := +| LocReg (_ : reg) +| LocArray (_ : reg) (_ : nat). + +Inductive location_is : fext -> assocmap -> assocmap_arr -> expr -> location -> Prop := +| Base : forall f asr asa r, location_is f asr asa (Vvar r) (LocReg r) +| Indexed : forall f asr asa r iexp iv, + expr_runp f asr asa iexp iv -> + location_is f asr asa (Vvari r iexp) (LocArray r (valueToNat iv)). + +(* Definition assign_name (f : fext) (asr: assocmap) (asa : assocmap_l) (e : expr) : res reg := *) +(* match e with *) +(* | Vvar r => OK r *) +(* | _ => Error (msg "Verilog: expression not supported on lhs of assignment") *) +(* end. *) + +(*Fixpoint stmnt_height (st : stmnt) {struct st} : nat := + match st with + | Vseq s1 s2 => S (stmnt_height s1 + stmnt_height s2) + | Vcond _ s1 s2 => S (Nat.max (stmnt_height s1) (stmnt_height s2)) + | Vcase _ ls (Some st) => + S (fold_right (fun t acc => Nat.max acc (stmnt_height (snd t))) 0%nat ls) + | _ => 1 + end. + +Fixpoint find_case_stmnt (s : state) (v : value) (cl : list (expr * stmnt)) + {struct cl} : option (res stmnt) := + match cl with + | (e, st)::xs => + match expr_run s e with + | OK v' => + match eq_to_opt v v' (veq v v') with + | Some eq => if valueToBool eq then Some (OK st) else find_case_stmnt s v xs + | None => Some (Error (msg "Verilog: equality check sizes not equal")) + end + | Error msg => Some (Error msg) + end + | _ => None + end. + +Fixpoint stmnt_run' (n : nat) (s : state) (st : stmnt) {struct n} : res state := + match n with + | S n' => + match st with + | Vskip => OK s + | Vseq s1 s2 => + do s' <- stmnt_run' n' s s1; + stmnt_run' n' s' s2 + | Vcond c st sf => + do cv <- expr_run s c; + if valueToBool cv + then stmnt_run' n' s st + else stmnt_run' n' s sf + | Vcase e cl defst => + do v <- expr_run s e; + match find_case_stmnt s v cl with + | Some (OK st') => stmnt_run' n' s st' + | Some (Error msg) => Error msg + | None => do s' <- handle_opt (msg "Verilog: no case was matched") + (option_map (stmnt_run' n' s) defst); s' + end + | Vblock lhs rhs => + match s with + | State m assoc nbassoc f c => + do name <- assign_name lhs; + do rhse <- expr_run s rhs; + OK (State m (PositiveMap.add name rhse assoc) nbassoc f c) + | _ => Error (msg "Verilog: Wrong state") + end + | Vnonblock lhs rhs => + match s with + | State m assoc nbassoc f c => + do name <- assign_name lhs; + do rhse <- expr_run s rhs; + OK (State m assoc (PositiveMap.add name rhse nbassoc) f c) + | _ => Error (msg "Verilog: Wrong state") + end + end + | _ => OK s + end. + +Definition stmnt_run (s : state) (st : stmnt) : res state := + stmnt_run' (stmnt_height st) s st. *) + +Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> + stmnt -> reg_associations -> arr_associations -> Prop := +| stmnt_runp_Vskip: + forall f ar al, stmnt_runp f ar al Vskip ar al +| stmnt_runp_Vseq: + forall f st1 st2 asr0 asa0 asr1 asa1 asr2 asa2, + stmnt_runp f asr0 asa0 st1 asr1 asa1 -> + stmnt_runp f asr1 asa1 st2 asr2 asa2 -> + stmnt_runp f asr0 asa0 (Vseq st1 st2) asr2 asa2 +| stmnt_runp_Vcond_true: + forall asr0 asa0 asr1 asa1 f c vc stt stf, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> + valueToBool vc = true -> + stmnt_runp f asr0 asa0 stt asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 +| stmnt_runp_Vcond_false: + forall asr0 asa0 asr1 asa1 f c vc stt stf, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) c vc -> + valueToBool vc = false -> + stmnt_runp f asr0 asa0 stf asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcond c stt stf) asr1 asa1 +| stmnt_runp_Vcase_nomatch: + forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> + mve <> ve -> + stmnt_runp f asr0 asa0 (Vcase e cs def) asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 +| stmnt_runp_Vcase_match: + forall e ve asr0 asa0 f asr1 asa1 me mve sc cs def, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) me mve -> + mve = ve -> + stmnt_runp f asr0 asa0 sc asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcase e ((me, sc)::cs) def) asr1 asa1 +| stmnt_runp_Vcase_default: + forall asr0 asa0 asr1 asa1 f st e ve, + expr_runp f asr0.(assoc_blocking) asa0.(assoc_blocking) e ve -> + stmnt_runp f asr0 asa0 st asr1 asa1 -> + stmnt_runp f asr0 asa0 (Vcase e nil (Some st)) asr1 asa1 +| stmnt_runp_Vblock_reg: + forall lhs r rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vblock lhs rhs) + (block_reg r asr rhsval) asa +| stmnt_runp_Vnonblock_reg: + forall lhs r rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocReg r) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vnonblock lhs rhs) + (nonblock_reg r asr rhsval) asa +| stmnt_runp_Vblock_arr: + forall lhs r i rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vblock lhs rhs) + asr (block_arr r i asa rhsval) +| stmnt_runp_Vnonblock_arr: + forall lhs r i rhs rhsval asr asa f, + location_is f asr.(assoc_blocking) asa.(assoc_blocking) lhs (LocArray r i) -> + expr_runp f asr.(assoc_blocking) asa.(assoc_blocking) rhs rhsval -> + stmnt_runp f asr asa + (Vnonblock lhs rhs) + asr (nonblock_arr r i asa rhsval). +Hint Constructors stmnt_runp : verilog. + +(*Fixpoint mi_step (s : state) (m : list module_item) {struct m} : res state := + let run := fun st ls => + do s' <- stmnt_run s st; + mi_step s' ls + in + match m with + | (Valways _ st)::ls => run st ls + | (Valways_ff _ st)::ls => run st ls + | (Valways_comb _ st)::ls => run st ls + | (Vdecl _ _)::ls => mi_step s ls + | (Vdeclarr _ _ _)::ls => mi_step s ls + | nil => OK s + end.*) + +Inductive mi_stepp : fext -> reg_associations -> arr_associations -> + module_item -> reg_associations -> arr_associations -> Prop := +| mi_stepp_Valways : + forall f sr0 sa0 st sr1 sa1 c, + stmnt_runp f sr0 sa0 st sr1 sa1 -> + mi_stepp f sr0 sa0 (Valways c st) sr1 sa1 +| mi_stepp_Valways_ff : + forall f sr0 sa0 st sr1 sa1 c, + stmnt_runp f sr0 sa0 st sr1 sa1 -> + mi_stepp f sr0 sa0 (Valways_ff c st) sr1 sa1 +| mi_stepp_Valways_comb : + forall f sr0 sa0 st sr1 sa1 c, + stmnt_runp f sr0 sa0 st sr1 sa1 -> + mi_stepp f sr0 sa0 (Valways_comb c st) sr1 sa1 +| mi_stepp_Vdecl : + forall f sr sa d, + mi_stepp f sr sa (Vdeclaration d) sr sa. +Hint Constructors mi_stepp : verilog. + +Inductive mis_stepp : fext -> reg_associations -> arr_associations -> + list module_item -> reg_associations -> arr_associations -> Prop := +| mis_stepp_Cons : + forall f mi mis sr0 sa0 sr1 sa1 sr2 sa2, + mi_stepp f sr0 sa0 mi sr1 sa1 -> + mis_stepp f sr1 sa1 mis sr2 sa2 -> + mis_stepp f sr0 sa0 (mi :: mis) sr2 sa2 +| mis_stepp_Nil : + forall f sr sa, + mis_stepp f sr sa nil sr sa. +Hint Constructors mis_stepp : verilog. + +(*Definition mi_step_commit (s : state) (m : list module_item) : res state := + match mi_step s m with + | OK (State m assoc nbassoc f c) => + OK (State m (merge_assocmap nbassoc assoc) empty_assocmap f c) + | Error msg => Error msg + | _ => Error (msg "Verilog: Wrong state") + end. + +Fixpoint mi_run (f : fextclk) (assoc : assocmap) (m : list module_item) (n : nat) + {struct n} : res assocmap := + match n with + | S n' => + do assoc' <- mi_run f assoc m n'; + match mi_step_commit (State assoc' empty_assocmap f (Pos.of_nat n')) m with + | OK (State assoc _ _ _) => OK assoc + | Error m => Error m + end + | O => OK assoc + end.*) + +(** Resets the module into a known state, so that it can be executed. This is +assumed to be the starting state of the module, and may have to be changed if +other arguments to the module are also to be supported. *) + +(*Definition initial_fextclk (m : module) : fextclk := + fun x => match x with + | S O => (AssocMap.set (mod_reset m) (ZToValue 1) empty_assocmap) + | _ => (AssocMap.set (mod_reset m) (ZToValue 0) empty_assocmap) + end.*) + +(*Definition module_run (n : nat) (m : module) : res assocmap := + mi_run (initial_fextclk m) empty_assocmap (mod_body m) n.*) + +Local Close Scope error_monad_scope. + +(*Theorem value_eq_size_if_eq: + forall lv rv EQ, + vsize lv = vsize rv -> value_eq_size lv rv = left EQ. +Proof. intros. unfold value_eq_size. + +Theorem expr_run_same: + forall assoc e v, expr_run assoc e = OK v <-> expr_runp assoc e v. +Proof. + split; generalize dependent v; generalize dependent assoc. + - induction e. + + intros. inversion H. constructor. + + intros. inversion H. constructor. assumption. + + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (expr_run assoc e2) eqn:?. + unfold eq_to_opt in H1. destruct (value_eq_size v0 v1) eqn:?. inversion H1. + constructor. apply IHe1. assumption. apply IHe2. assumption. reflexivity. discriminate. discriminate. + discriminate. + + intros. inversion H. destruct (expr_run assoc e) eqn:?. unfold option_map in H1. + inversion H1. constructor. apply IHe. assumption. reflexivity. discriminate. + + intros. inversion H. destruct (expr_run assoc e1) eqn:?. destruct (valueToBool v0) eqn:?. + eapply erun_Vternary_true. apply IHe1. eassumption. apply IHe2. eassumption. assumption. + eapply erun_Vternary_false. apply IHe1. eassumption. apply IHe3. eassumption. assumption. + discriminate. + - induction e. + + intros. inversion H. reflexivity. + + intros. inversion H. subst. simpl. assumption. + + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. + apply IHe2 in H6. rewrite H6. unfold eq_to_opt. assert (vsize lv = vsize rv). + apply EQ. apply (value_eq_size_if_eq lv rv EQ) in H0. rewrite H0. reflexivity. + + intros. inversion H. subst. simpl. destruct (expr_run assoc e) eqn:?. simpl. + apply IHe in H3. rewrite Heqo in H3. + inversion H3. subst. reflexivity. apply IHe in H3. rewrite Heqo in H3. discriminate. + + intros. inversion H. subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. + apply IHe2 in H6. rewrite H6. reflexivity. + subst. simpl. apply IHe1 in H4. rewrite H4. rewrite H7. apply IHe3. + assumption. +Qed. + + *) + +Fixpoint init_params (vl : list value) (rl : list reg) {struct rl} := + match rl, vl with + | r :: rl', v :: vl' => AssocMap.set r v (init_params vl' rl') + | _, _ => empty_assocmap + end. + +Definition genv := Globalenvs.Genv.t fundef unit. +Definition empty_stack (m : module) : assocmap_arr := + (AssocMap.set m.(mod_stk) (Array.arr_repeat None m.(mod_stk_len)) (AssocMap.empty arr)). + +Inductive step : genv -> state -> Events.trace -> state -> Prop := + | step_module : + forall asr asa asr' asa' basr1 nasr1 basa1 nasa1 f stval pstval m sf st g ist, + asr!(m.(mod_reset)) = Some (ZToValue 0) -> + asr!(m.(mod_finish)) = Some (ZToValue 0) -> + asr!(m.(mod_st)) = Some ist -> + valueToPos ist = st -> + mis_stepp f (mkassociations asr empty_assocmap) + (mkassociations asa (empty_stack m)) + m.(mod_body) + (mkassociations basr1 nasr1) + (mkassociations basa1 nasa1)-> + asr' = merge_regs nasr1 basr1 -> + asa' = merge_arrs nasa1 basa1 -> + asr'!(m.(mod_st)) = Some stval -> + valueToPos stval = pstval -> + step g (State sf m st asr asa) Events.E0 (State sf m pstval asr' asa') +| step_finish : + forall asr asa sf retval m st g, + asr!(m.(mod_finish)) = Some (ZToValue 1) -> + asr!(m.(mod_return)) = Some retval -> + step g (State sf m st asr asa) Events.E0 (Returnstate sf retval) +| step_call : + forall g res m args, + step g (Callstate res m args) Events.E0 + (State res m m.(mod_entrypoint) + (AssocMap.set (mod_reset m) (ZToValue 0) + (AssocMap.set (mod_finish m) (ZToValue 0) + (AssocMap.set m.(mod_st) (posToValue m.(mod_entrypoint)) + (init_params args m.(mod_args))))) + (empty_stack m)) +| step_return : + forall g m asr i r sf pc mst asa, + mst = mod_st m -> + step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). +Hint Constructors step : verilog. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b m0 m, + let ge := Globalenvs.Genv.globalenv p in + Globalenvs.Genv.init_mem p = Some m0 -> + Globalenvs.Genv.find_symbol ge p.(AST.prog_main) = Some b -> + Globalenvs.Genv.find_funct_ptr ge b = Some (AST.Internal m) -> + initial_state p (Callstate nil m nil). + +Inductive final_state : state -> Integers.int -> Prop := +| final_state_intro : forall retval retvali, + retvali = valueToInt retval -> + final_state (Returnstate nil retval) retvali. + +Definition semantics (m : program) := + Smallstep.Semantics step (initial_state m) final_state + (Globalenvs.Genv.globalenv m). + +Lemma expr_runp_determinate : + forall f e asr asa v, + expr_runp f asr asa e v -> + forall v', + expr_runp f asr asa e v' -> + v' = v. +Proof. + induction e; intros; + + repeat (try match goal with + | [ H : expr_runp _ _ _ (Vlit _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vvari _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vinputvar _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vbinop _ _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vunop _ _) _ |- _ ] => invert H + | [ H : expr_runp _ _ _ (Vternary _ _ _) _ |- _ ] => invert H + + | [ H1 : forall asr asa v, expr_runp _ asr asa ?e v -> _, + H2 : expr_runp _ _ _ ?e _ |- _ ] => + learn (H1 _ _ _ H2) + | [ H1 : forall v, expr_runp _ ?asr ?asa ?e v -> _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (H1 _ H2) + end; crush). +Qed. +Hint Resolve expr_runp_determinate : verilog. + +Lemma location_is_determinate : + forall f asr asa e l, + location_is f asr asa e l -> + forall l', + location_is f asr asa e l' -> + l' = l. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : location_is _ _ _ _ _ |- _ ] => invert H + | [ H1 : expr_runp _ ?asr ?asa ?e _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (expr_runp_determinate H1 H2) + end; crush). +Qed. + +Lemma stmnt_runp_determinate : + forall f s asr0 asa0 asr1 asa1, + stmnt_runp f asr0 asa0 s asr1 asa1 -> + forall asr1' asa1', + stmnt_runp f asr0 asa0 s asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. + induction 1; intros; + + repeat (try match goal with + | [ H : stmnt_runp _ _ _ (Vseq _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vnonblock _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vblock _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ Vskip _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcond _ _ _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ (_ :: _) _) _ _ |- _ ] => invert H + | [ H : stmnt_runp _ _ _ (Vcase _ [] _) _ _ |- _ ] => invert H + + | [ H1 : expr_runp _ ?asr ?asa ?e _, + H2 : expr_runp _ ?asr ?asa ?e _ |- _ ] => + learn (expr_runp_determinate H1 H2) + + | [ H1 : location_is _ ?asr ?asa ?e _, + H2 : location_is _ ?asr ?asa ?e _ |- _ ] => + learn (location_is_determinate H1 H2) + + | [ H1 : forall asr1 asa1, stmnt_runp _ ?asr0 ?asa0 ?s asr1 asa1 -> _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. +Hint Resolve stmnt_runp_determinate : verilog. + +Lemma mi_stepp_determinate : + forall f asr0 asa0 m asr1 asa1, + mi_stepp f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mi_stepp f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + intros. destruct m; invert H; invert H0; + + repeat (try match goal with + | [ H1 : stmnt_runp _ ?asr0 ?asa0 ?s _ _, + H2 : stmnt_runp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (stmnt_runp_determinate H1 H2) + end; crush). +Qed. + +Lemma mis_stepp_determinate : + forall f asr0 asa0 m asr1 asa1, + mis_stepp f asr0 asa0 m asr1 asa1 -> + forall asr1' asa1', + mis_stepp f asr0 asa0 m asr1' asa1' -> + asr1' = asr1 /\ asa1' = asa1. +Proof. + induction 1; intros; + + repeat (try match goal with + | [ H : mis_stepp _ _ _ [] _ _ |- _ ] => invert H + | [ H : mis_stepp _ _ _ ( _ :: _ ) _ _ |- _ ] => invert H + + | [ H1 : mi_stepp _ ?asr0 ?asa0 ?s _ _, + H2 : mi_stepp _ ?asr0 ?asa0 ?s _ _ |- _ ] => + learn (mi_stepp_determinate H1 H2) + + | [ H1 : forall asr1 asa1, mis_stepp _ ?asr0 ?asa0 ?m asr1 asa1 -> _, + H2 : mis_stepp _ ?asr0 ?asa0 ?m _ _ |- _ ] => + learn (H1 _ _ H2) + end; crush). +Qed. + +Lemma semantics_determinate : + forall (p: program), Smallstep.determinate (semantics p). +Proof. + intros. constructor; set (ge := Globalenvs.Genv.globalenv p); simplify. + - invert H; invert H0; constructor. (* Traces are always empty *) + - invert H; invert H0; crush. assert (f = f0) by (destruct f; destruct f0; auto); subst. + pose proof (mis_stepp_determinate H5 H15). + crush. + - constructor. invert H; crush. + - invert H; invert H0; unfold ge0, ge1 in *; crush. + - red; simplify; intro; invert H0; invert H; crush. + - invert H; invert H0; crush. +Qed. diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v new file mode 100644 index 0000000..a0be0fa --- /dev/null +++ b/src/hls/Veriloggen.v @@ -0,0 +1,65 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require Import Maps. +From compcert Require Errors. +From compcert Require Import AST. +From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt. + +Definition transl_list_fun (a : node * Verilog.stmnt) := + let (n, stmnt) := a in + (Vlit (posToValue n), stmnt). + +Definition transl_list st := map transl_list_fun st. + +Definition scl_to_Vdecl_fun (a : reg * (option io * scl_decl)) := + match a with (r, (io, VScalar sz)) => (Vdecl io r sz) end. + +Definition scl_to_Vdecl scldecl := map scl_to_Vdecl_fun scldecl. + +Definition arr_to_Vdeclarr_fun (a : reg * (option io * arr_decl)) := + match a with (r, (io, VArray sz l)) => (Vdeclarr io r sz l) end. + +Definition arr_to_Vdeclarr arrdecl := map arr_to_Vdeclarr_fun arrdecl. + +Definition transl_module (m : HTL.module) : Verilog.module := + let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in + let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in + let body := + Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1))) + (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint)))) + (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip))) + :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip)) + :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls)) + ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in + Verilog.mkmodule m.(mod_start) + m.(mod_reset) + m.(mod_clk) + m.(mod_finish) + m.(mod_return) + m.(mod_st) + m.(mod_stk) + m.(mod_stk_len) + m.(mod_params) + body + m.(mod_entrypoint). + +Definition transl_fundef := transf_fundef transl_module. + +Definition transl_program (p: HTL.program) : Verilog.program := + transform_program transl_fundef p. diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v new file mode 100644 index 0000000..9abbd4b --- /dev/null +++ b/src/hls/Veriloggenproof.v @@ -0,0 +1,368 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see . + *) + +From compcert Require Import Smallstep Linking Integers Globalenvs. +From vericert Require HTL. +From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. +Require Import Lia. + +Local Open Scope assocmap. + +Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := + match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + +Lemma transf_program_match: + forall prog, match_prog prog (transl_program prog). +Proof. + intros. eapply match_transform_program_contextual. auto. +Qed. + +Inductive match_stacks : list HTL.stackframe -> list stackframe -> Prop := +| match_stack : + forall res m pc reg_assoc arr_assoc hstk vstk, + match_stacks hstk vstk -> + match_stacks (HTL.Stackframe res m pc reg_assoc arr_assoc :: hstk) + (Stackframe res (transl_module m) pc + reg_assoc arr_assoc :: vstk) +| match_stack_nil : match_stacks nil nil. + +Inductive match_states : HTL.state -> state -> Prop := +| match_state : + forall m st reg_assoc arr_assoc hstk vstk, + match_stacks hstk vstk -> + match_states (HTL.State hstk m st reg_assoc arr_assoc) + (State vstk (transl_module m) st reg_assoc arr_assoc) +| match_returnstate : + forall v hstk vstk, + match_stacks hstk vstk -> + match_states (HTL.Returnstate hstk v) (Returnstate vstk v) +| match_initial_call : + forall m, + match_states (HTL.Callstate nil m nil) (Callstate nil (transl_module m) nil). + +Lemma Vlit_inj : + forall a b, Vlit a = Vlit b -> a = b. +Proof. inversion 1. trivial. Qed. + +Lemma posToValue_inj : + forall a b, + 0 <= Z.pos a <= Int.max_unsigned -> + 0 <= Z.pos b <= Int.max_unsigned -> + posToValue a = posToValue b -> + a = b. +Proof. + intros. rewrite <- Pos2Z.id at 1. rewrite <- Pos2Z.id. + rewrite <- Int.unsigned_repr at 1; try assumption. + symmetry. + rewrite <- Int.unsigned_repr at 1; try assumption. + unfold posToValue in *. rewrite H1; auto. +Qed. + +Lemma valueToPos_inj : + forall a b, + 0 < Int.unsigned a -> + 0 < Int.unsigned b -> + valueToPos a = valueToPos b -> + a = b. +Proof. + intros. unfold valueToPos in *. + rewrite <- Int.repr_unsigned at 1. + rewrite <- Int.repr_unsigned. + apply Pos2Z.inj_iff in H1. + rewrite Z2Pos.id in H1; auto. + rewrite Z2Pos.id in H1; auto. + rewrite H1. auto. +Qed. + +Lemma unsigned_posToValue_le : + forall p, + Z.pos p <= Int.max_unsigned -> + 0 < Int.unsigned (posToValue p). +Proof. + intros. unfold posToValue. rewrite Int.unsigned_repr; lia. +Qed. + +Lemma transl_list_fun_fst : + forall p1 p2 a b, + 0 <= Z.pos p1 <= Int.max_unsigned -> + 0 <= Z.pos p2 <= Int.max_unsigned -> + transl_list_fun (p1, a) = transl_list_fun (p2, b) -> + (p1, a) = (p2, b). +Proof. + intros. unfold transl_list_fun in H1. apply pair_equal_spec in H1. + destruct H1. rewrite H2. apply Vlit_inj in H1. + apply posToValue_inj in H1; try assumption. + rewrite H1; auto. +Qed. + +Lemma Zle_relax : + forall p q r, + p < q <= r -> + p <= q <= r. +Proof. lia. Qed. +Hint Resolve Zle_relax : verilogproof. + +Lemma transl_in : + forall l p, + 0 <= Z.pos p <= Int.max_unsigned -> + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + In (Vlit (posToValue p)) (map fst (map transl_list_fun l)) -> + In p (map fst l). +Proof. + induction l. + - simplify. auto. + - intros. destruct a. simplify. destruct (peq p0 p); auto. + right. inv H1. apply Vlit_inj in H. apply posToValue_inj in H; auto. contradiction. + auto with verilogproof. + apply IHl; auto. +Qed. + +Lemma transl_notin : + forall l p, + 0 <= Z.pos p <= Int.max_unsigned -> + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + ~ In p (List.map fst l) -> ~ In (Vlit (posToValue p)) (List.map fst (transl_list l)). +Proof. + induction l; auto. intros. destruct a. unfold not in *. intros. + simplify. + destruct (peq p0 p). apply H1. auto. apply H1. + unfold transl_list in *. inv H2. apply Vlit_inj in H. apply posToValue_inj in H. + contradiction. + auto with verilogproof. auto. + right. apply transl_in; auto. +Qed. + +Lemma transl_norepet : + forall l, + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + list_norepet (List.map fst l) -> list_norepet (List.map fst (transl_list l)). +Proof. + induction l. + - intros. simpl. apply list_norepet_nil. + - destruct a. intros. simpl. apply list_norepet_cons. + inv H0. apply transl_notin. apply Zle_relax. apply H. simplify; auto. + intros. apply H. destruct (peq p0 p); subst; simplify; auto. + assumption. apply IHl. intros. apply H. destruct (peq p0 p); subst; simplify; auto. + simplify. inv H0. assumption. +Qed. + +Lemma transl_list_correct : + forall l v ev f asr asa asrn asan asr' asa' asrn' asan', + (forall p0, In p0 (List.map fst l) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + list_norepet (List.map fst l) -> + asr!ev = Some v -> + (forall p s, + In (p, s) l -> + v = posToValue p -> + stmnt_runp f + {| assoc_blocking := asr; assoc_nonblocking := asrn |} + {| assoc_blocking := asa; assoc_nonblocking := asan |} + s + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |} -> + stmnt_runp f + {| assoc_blocking := asr; assoc_nonblocking := asrn |} + {| assoc_blocking := asa; assoc_nonblocking := asan |} + (Vcase (Vvar ev) (transl_list l) (Some Vskip)) + {| assoc_blocking := asr'; assoc_nonblocking := asrn' |} + {| assoc_blocking := asa'; assoc_nonblocking := asan' |}). +Proof. + induction l as [| a l IHl]. + - contradiction. + - intros v ev f asr asa asrn asan asr' asa' asrn' asan' BOUND NOREP ASSOC p s IN EQ SRUN. + destruct a as [p' s']. simplify. + destruct (peq p p'); subst. eapply stmnt_runp_Vcase_match. + constructor. simplify. unfold AssocMap.find_assocmap, AssocMapExt.get_default. + rewrite ASSOC. trivial. constructor. auto. + inversion IN as [INV | INV]. inversion INV as [INV2]; subst. assumption. + inv NOREP. eapply in_map with (f := fst) in INV. contradiction. + + eapply stmnt_runp_Vcase_nomatch. constructor. simplify. + unfold AssocMap.find_assocmap, AssocMapExt.get_default. rewrite ASSOC. + trivial. constructor. unfold not. intros. apply n. apply posToValue_inj. + apply Zle_relax. apply BOUND. right. inv IN. inv H0; contradiction. + eapply in_map with (f := fst) in H0. auto. + apply Zle_relax. apply BOUND; auto. auto. + + eapply IHl. auto. inv NOREP. auto. eassumption. inv IN. inv H. contradiction. apply H. + trivial. assumption. +Qed. +Hint Resolve transl_list_correct : verilogproof. + +Lemma pc_wf : + forall A m p v, + (forall p0, In p0 (List.map fst (@AssocMap.elements A m)) -> 0 < Z.pos p0 <= Int.max_unsigned) -> + m!p = Some v -> + 0 <= Z.pos p <= Int.max_unsigned. +Proof. + intros A m p v LT S. apply Zle_relax. apply LT. + apply AssocMap.elements_correct in S. remember (p, v) as x. + exploit in_map. apply S. instantiate (1 := fst). subst. simplify. auto. +Qed. + +Lemma mis_stepp_decl : + forall l asr asa f, + mis_stepp f asr asa (map Vdeclaration l) asr asa. +Proof. + induction l. + - intros. constructor. + - intros. simplify. econstructor. constructor. auto. +Qed. +Hint Resolve mis_stepp_decl : verilogproof. + +Section CORRECTNESS. + + Variable prog: HTL.program. + Variable tprog: program. + + Hypothesis TRANSL : match_prog prog tprog. + + Let ge : HTL.genv := Globalenvs.Genv.globalenv prog. + Let tge : genv := Globalenvs.Genv.globalenv tprog. + + Lemma symbols_preserved: + forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. + Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. + Hint Resolve symbols_preserved : verilogproof. + + Lemma function_ptr_translated: + forall (b: Values.block) (f: HTL.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = tf. + Proof. + intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + Hint Resolve function_ptr_translated : verilogproof. + + Lemma functions_translated: + forall (v: Values.val) (f: HTL.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef f = tf. + Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & P & Q & R); exists tf; auto. + Qed. + Hint Resolve functions_translated : verilogproof. + + Lemma senv_preserved: + Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). + Proof. + intros. eapply (Genv.senv_match TRANSL). + Qed. + Hint Resolve senv_preserved : verilogproof. + + Theorem transl_step_correct : + forall (S1 : HTL.state) t S2, + HTL.step ge S1 t S2 -> + forall (R1 : state), + match_states S1 R1 -> + exists R2, Smallstep.plus step tge R1 t R2 /\ match_states S2 R2. + Proof. + induction 1; intros R1 MSTATE; inv MSTATE. + - econstructor; split. apply Smallstep.plus_one. econstructor. + assumption. assumption. eassumption. apply valueToPos_posToValue. + split. lia. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + econstructor. econstructor. eapply stmnt_runp_Vcond_false. econstructor. econstructor. + simpl. unfold find_assocmap. unfold AssocMapExt.get_default. + rewrite H. trivial. + + econstructor. simpl. auto. auto. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + econstructor. econstructor. + + eapply transl_list_correct. + intros. split. lia. pose proof (HTL.mod_wf m) as HP. destruct HP as [_ HP]. auto. + apply Maps.PTree.elements_keys_norepet. eassumption. + 2: { apply valueToPos_inj. apply unsigned_posToValue_le. + eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. + apply unsigned_posToValue_le. eapply pc_wf. intros. pose proof (HTL.mod_wf m) as HP. + destruct HP as [HP _]. + split. lia. apply HP. eassumption. eassumption. trivial. + } + apply Maps.PTree.elements_correct. eassumption. eassumption. + + apply mis_stepp_decl. trivial. trivial. simpl. eassumption. auto. + rewrite valueToPos_posToValue. constructor; assumption. lia. + + - econstructor; split. apply Smallstep.plus_one. apply step_finish. assumption. eassumption. + constructor; assumption. + - econstructor; split. apply Smallstep.plus_one. constructor. + + constructor. constructor. + - inv H3. econstructor; split. apply Smallstep.plus_one. constructor. trivial. + + apply match_state. assumption. + Qed. + Hint Resolve transl_step_correct : verilogproof. + + Lemma transl_initial_states : + forall s1 : Smallstep.state (HTL.semantics prog), + Smallstep.initial_state (HTL.semantics prog) s1 -> + exists s2 : Smallstep.state (Verilog.semantics tprog), + Smallstep.initial_state (Verilog.semantics tprog) s2 /\ match_states s1 s2. + Proof. + induction 1. + econstructor; split. econstructor. + apply (Genv.init_mem_transf TRANSL); eauto. + rewrite symbols_preserved. + replace (AST.prog_main tprog) with (AST.prog_main prog); eauto. + symmetry; eapply Linking.match_program_main; eauto. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + inv B. eauto. + constructor. + Qed. + Hint Resolve transl_initial_states : verilogproof. + + Lemma transl_final_states : + forall (s1 : Smallstep.state (HTL.semantics prog)) + (s2 : Smallstep.state (Verilog.semantics tprog)) + (r : Integers.Int.int), + match_states s1 s2 -> + Smallstep.final_state (HTL.semantics prog) s1 r -> + Smallstep.final_state (Verilog.semantics tprog) s2 r. + Proof. + intros. inv H0. inv H. inv H3. constructor. reflexivity. + Qed. + Hint Resolve transl_final_states : verilogproof. + + Theorem transf_program_correct: + forward_simulation (HTL.semantics prog) (Verilog.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus; eauto with verilogproof. + apply senv_preserved. + Qed. + +End CORRECTNESS. -- cgit