From b5144a6f513c5c6e3344dcc935117706637ddd3f Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 3 Jul 2020 18:47:56 +0100 Subject: Add new value type to fix Iop proof --- src/translation/HTLgen.v | 4 +- src/verilog/AssocMap.v | 4 +- src/verilog/Value.v | 23 ++----- src/verilog/ValueInt.v | 160 +++++++++++++++++++++++++++++++++++++++++++++++ src/verilog/Verilog.v | 93 ++++++++++++++------------- 5 files changed, 217 insertions(+), 67 deletions(-) create mode 100644 src/verilog/ValueInt.v diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index a2b77e6..f58c9ae 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -19,7 +19,7 @@ From compcert Require Import Maps. From compcert Require Errors Globalenvs Integers. From compcert Require Import AST RTL. -From coqup Require Import Verilog HTL Coquplib AssocMap Value Statemonad. +From coqup Require Import Verilog HTL Coquplib AssocMap ValueInt Statemonad. Hint Resolve AssocMap.gempty : htlh. Hint Resolve AssocMap.gso : htlh. @@ -88,7 +88,7 @@ Import HTLMonadExtra. Export MonadNotation. Definition state_goto (st : reg) (n : node) : stmnt := - Vnonblock (Vvar st) (Vlit (posToValue 32 n)). + Vnonblock (Vvar st) (Vlit (posToValue n)). Definition state_cond (st : reg) (c : expr) (n1 n2 : node) : stmnt := Vnonblock (Vvar st) (Vternary c (posToExpr 32 n1) (posToExpr 32 n2)). diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 5d531d5..c5cfa3f 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -16,7 +16,7 @@ * along with this program. If not, see . *) -From coqup Require Import Coquplib Value. +From coqup Require Import Coquplib ValueInt. From compcert Require Import Maps. Definition reg := positive. @@ -192,7 +192,7 @@ Import AssocMapExt. Definition assocmap := AssocMap.t value. Definition find_assocmap (n : nat) : reg -> assocmap -> value := - get_default value (ZToValue n 0). + get_default value (ZToValue 0). Definition empty_assocmap : assocmap := AssocMap.empty value. diff --git a/src/verilog/Value.v b/src/verilog/Value.v index b80b614..2718a46 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -466,16 +466,9 @@ Proof. rewrite ZToWord_plus; auto. Qed. -Lemma zadd_vplus3 : - forall w1 w2, - (wordToN w1 + wordToN w2 < Npow2 32)%N -> - valueToN (vplus (mkvalue 32 w1) (mkvalue 32 w2) eq_refl) = - (valueToN (mkvalue 32 w1) + valueToN (mkvalue 32 w2))%N. -Proof. - intros. unfold vplus, map_word2. rewrite unify_word_unfold. unfold valueToN. - simplify. unfold wplus. unfold wordBin. - rewrite wordToN_NToWord_2. trivial. assumption. -Qed. +Lemma ZToValue_eq : + forall w1, + (mkvalue 32 w1) = (ZToValue 32 (wordToZ w1)). Admitted. Lemma wordsize_32 : Int.wordsize = 32%nat. @@ -490,13 +483,7 @@ Proof. rewrite Int.repr_unsigned. auto. rewrite wordsize_32. omega. Qed. -Lemma vadd_vplus : - forall v1 v2 EQ, - uvalueToZ v1 + uvalueToZ v2 = uvalueToZ (vplus v1 v2 EQ). -Proof. - Admitted. - -Lemma intadd_vplus2 : +(*Lemma intadd_vplus2 : forall v1 v2 EQ, vsize v1 = 32%nat -> Int.add (valueToInt v1) (valueToInt v2) = valueToInt (vplus v1 v2 EQ). @@ -504,7 +491,7 @@ Proof. intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr). rewrite (@vadd_vplus v1 v2 EQ). trivial. unfold uvalueToZ. Search word "bound". pose proof (@uwordToZ_bound (vsize v2) (vword v2)). - rewrite H in EQ. rewrite <- EQ in H0. + rewrite H in EQ. rewrite <- EQ in H0 at 3.*) (*rewrite zadd_vplus3. trivia*) Lemma valadd_vplus : diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v new file mode 100644 index 0000000..cc1d404 --- /dev/null +++ b/src/verilog/ValueInt.v @@ -0,0 +1,160 @@ +(* + * CoqUp: 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 coqup Require Import Coquplib. +(* 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. + +Search Ptrofs.of_int Ptrofs.to_int. +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 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 true else false. + +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' -> + (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 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 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. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0); try discriminate. + inv H1. symmetry. unfold valueToPtr, ptrToValue. apply Ptrofs.of_int_to_int. trivial. + inv H. destruct (uvalueToZ (ptrToValue i) mod 4 =? 0) eqn:?; try discriminate. + inv H1. apply Z.eqb_eq. apply Heqb0. +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. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 555ddbd..5ef4dda 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -29,11 +29,9 @@ Require Import Lia. Import ListNotations. -From coqup Require Import common.Coquplib common.Show verilog.Value AssocMap Array. -From compcert Require Integers Events. -From compcert Require Import Errors Smallstep Globalenvs. - -Import HexNotationValue. +From coqup Require Import common.Coquplib common.Show verilog.ValueInt AssocMap Array. +From compcert Require Events. +From compcert Require Import Integers Errors Smallstep Globalenvs. Local Open Scope assocmap. @@ -80,7 +78,7 @@ Definition merge_arrs (new : assocmap_arr) (old : assocmap_arr) : assocmap_arr : 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 32 0) (Option.join (array_get_error i arr))) + | 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 := @@ -164,8 +162,8 @@ Inductive expr : Type := | Vunop : unop -> expr -> expr | Vternary : expr -> expr -> expr -> expr. -Definition posToExpr (sz : nat) (p : positive) : expr := - Vlit (posToValue sz p). +Definition posToExpr (p : positive) : expr := + Vlit (posToValue p). (** ** Statements *) @@ -245,7 +243,7 @@ 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 (posToValueAuto p). + Vlit (posToValue p). Coercion Vlit : value >-> expr. Coercion Vvar : reg >-> expr. @@ -298,37 +296,43 @@ Inductive state : Type := (m : module) (args : list value), state. -Definition binop_run (op : binop) : forall v1 v2 : value, vsize v1 = vsize v2 -> value := +Definition binop_run (op : binop) (v1 v2 : value) : option value := match op with - | Vadd => vplus - | Vsub => vminus - | Vmul => vmul - | Vdiv => vdivs - | Vdivu => vdiv - | Vmod => vmods - | Vmodu => vmod - | Vlt => vlts - | Vltu => vlt - | Vgt => vgts - | Vgtu => vgt - | Vle => vles - | Vleu => vle - | Vge => vges - | Vgeu => vge - | Veq => veq - | Vne => vne - | Vand => vand - | Vor => vor - | Vxor => vxor - | Vshl => vshl - | Vshr => vshr - | Vshru => vshr (* FIXME: should not be the same operation. *) + | 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) : value -> value := +Definition unop_run (op : unop) (v1 : value) : value := match op with - | Vneg => vnot - | Vnot => vbitneg + | Vneg => Int.notbool v1 + | Vnot => Int.not v1 end. Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop := @@ -349,11 +353,10 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop fext!r = Some v -> expr_runp fext reg stack (Vinputvar r) v | erun_Vbinop : - forall fext reg stack op l r lv rv oper EQ resv, + forall fext reg stack op l r lv rv resv, expr_runp fext reg stack l lv -> expr_runp fext reg stack r rv -> - oper = binop_run op -> - resv = oper lv rv EQ -> + 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, @@ -394,7 +397,7 @@ 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 1 0) + | _ => OK (ZToValue 0) end. (* TODO FIX Vvar case without default *) @@ -652,8 +655,8 @@ 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 1) empty_assocmap) - | _ => (AssocMap.set (mod_reset m) (ZToValue 1 0) empty_assocmap) + | 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 := @@ -727,21 +730,21 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := 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 (1'h"1") -> + 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 m.(mod_st) (posToValue 32 m.(mod_entrypoint)) + (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 32 pc)) # r <- i) + (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) (empty_stack m)). Hint Constructors step : verilog. -- cgit