From 088a554043e3d4b8b8b424dbda9a136e3f4571e5 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 11 Jun 2020 22:50:01 +0100 Subject: Rough outline of stack address proof --- src/translation/HTLgen.v | 12 ++--- src/translation/HTLgenproof.v | 123 +++++++++++++++++++++++++++++++++--------- src/verilog/Verilog.v | 8 +-- 3 files changed, 109 insertions(+), 34 deletions(-) diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index d5a8af2..cba2940 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -314,21 +314,21 @@ Definition add_branch_instr (e: expr) (n n1 n2: node) : mon unit := Definition translate_arr_access (mem : AST.memory_chunk) (addr : Op.addressing) (args : list reg) (stack : reg) : mon expr := - match addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) - | Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *) - | Op.Ascaled scale offset, r1::nil => + match mem, addr, args with (* TODO: We should be more methodical here; what are the possibilities?*) + | Mint32, Op.Aindexed off, r1::nil => ret (Vvari stack (boplitz Vadd r1 off)) (* FIXME: Cannot guarantee alignment *) + | Mint32, Op.Ascaled scale offset, r1::nil => if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) then ret (Vvari stack (Vbinop Vadd (boplitz Vmul r1 (scale / 4)) (Vlit (ZToValue 32 (offset / 4))))) else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") - | Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) + | Mint32, Op.Aindexed2scaled scale offset, r1::r2::nil => (* Typical for dynamic array addressing *) if ((Z.eqb (Z.modulo scale 4) 0) && (Z.eqb (Z.modulo offset 4) 0)) then ret (Vvari stack (Vbinop Vadd (boplitz Vadd r1 (offset / 4)) (boplitz Vmul r2 (scale / 4)))) else error (Errors.msg "Veriloggen: translate_arr_access address misaligned") - | Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) + | Mint32, Op.Ainstack a, nil => (* We need to be sure that the base address is aligned *) let a := Integers.Ptrofs.unsigned a in (* FIXME: Assuming stack offsets are +ve; is this ok? *) if (Z.eq_dec (Z.modulo a 4) 0) then ret (Vvari stack (Vlit (ZToValue 32 (a / 4)))) else error (Errors.msg "Veriloggen: eff_addressing misaligned stack offset") - | _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") + | _, _, _ => error (Errors.msg "Veriloggen: translate_arr_access unsuported addressing") end. Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon unit := diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 1f9e368..34fa8ec 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -51,7 +51,7 @@ Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem 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 ptr))) - (nth (Z.to_nat ptr) stack (ZToValue 32 0))) -> + (nth (Z.to_nat ptr / 4) stack (ZToValue 32 0))) -> match_arrs m f sp mem asa. Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop := @@ -425,38 +425,113 @@ Section CORRECTNESS. | [ H: Values.Vptr _ _ = Values.Vptr _ _ |- _] => invert H end. - - destruct c, addr, args; simplify; rt; t; simplify. + Opaque Nat.div. + + - destruct c, chunk, addr, args; simplify; rt; simplify. + admit. (* FIXME: Alignment *) + + admit. + + admit. + + invert MARR. simplify. - + unfold Op.eval_addressing in *. - (* destruct (Archi.ptr64); simplify; *) - (* destruct (Registers.Regmap.get r0 rs); simplify. *) - admit. + unfold Op.eval_addressing in H0. + destruct (Archi.ptr64) eqn:ARCHI; simplify. + rewrite ARCHI in H0. simplify. - (* eexists. split. *) - (* eapply Smallstep.plus_one. *) - (* eapply HTL.step_module; eauto. *) - (* econstructor. econstructor. econstructor. simpl. *) - (* econstructor. econstructor. econstructor. econstructor. econstructor. *) - (* econstructor. econstructor. econstructor. econstructor. econstructor. *) - (* econstructor. econstructor. econstructor. simpl. *) + (* Out of bounds reads are undefined behaviour. *) + assert (forall ptr v, f.(RTL.fn_stacksize) <= ptr -> + Mem.loadv AST.Mint32 m (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr)) = Some v -> + v = Values.Vundef) as INVALID_READ by admit. - (* inversion MARR; subst; clear MARR. simpl in *. *) - (* unfold Verilog.arr_assocmap_lookup. *) - (* rewrite H3. *) + (* Case split on whether read is out of bounds. *) + destruct (RTL.fn_stacksize f <=? Integers.Ptrofs.unsigned i0) eqn:BOUND. + * assert (RTL.fn_stacksize f <= Integers.Ptrofs.unsigned i0) as OUT_OF_BOUNDS. { + apply Zle_bool_imp_le. assumption. + } + eapply INVALID_READ in OUT_OF_BOUNDS. + 2: { rewrite Integers.Ptrofs.repr_unsigned. eassumption. } - (* admit. *) + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. econstructor. simplify. - + unfold Op.eval_addressing in *. - (* destruct (Archi.ptr64); simplify; *) - (* destruct (Registers.Regmap.get r0 rs); *) - (* destruct (Registers.Regmap.get r1 rs); simplify; *) - (* destruct (Archi.ptr64); simplify. *) - admit. + unfold Verilog.arr_assocmap_lookup. rewrite H3. + reflexivity. - + admit. + simplify. unfold_merge. apply AssocMap.gss. + + simplify. rewrite assumption_32bit. + constructor. + + unfold_merge. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + + apply regs_lessdef_add_match. + rewrite OUT_OF_BOUNDS. + constructor. assumption. + + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold_merge. apply AssocMap.gss. + + assumption. + + econstructor; simplify; try reflexivity; eassumption. + + * assert (Integers.Ptrofs.unsigned i0 < f.(RTL.fn_stacksize)) as IN_BOUNDS. { + rewrite Z.leb_antisym in BOUND. + rewrite negb_false_iff in BOUND. + apply Zlt_is_lt_bool. assumption. + } + + eexists. split. + eapply Smallstep.plus_one. + eapply HTL.step_module; eauto. + econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. econstructor. simplify. + + unfold Verilog.arr_assocmap_lookup. rewrite H3. + reflexivity. + + simplify. unfold_merge. apply AssocMap.gss. + + simplify. rewrite assumption_32bit. + constructor. + + unfold_merge. + apply regs_lessdef_add_greater. + apply greater_than_max_func. + + apply regs_lessdef_add_match. + + assert (exists ptr, (Z.to_nat ptr / 4)%nat = (valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned i0 / 4)))) + by admit. + simplify. rewrite <- H5. + specialize (H4 x). + assert (0 <= x < Z.of_nat (Z.to_nat (RTL.fn_stacksize f / 4))) by admit. + apply H4 in H0. + invert H0. + assert (Integers.Ptrofs.repr x = i0) by admit. + rewrite H0 in H6. + rewrite H1 in H6. + invert H6. + assumption. + + assumption. + + assumption. + + unfold state_st_wf. inversion 1. simplify. + unfold_merge. apply AssocMap.gss. + + assumption. + + econstructor; simplify; try reflexivity; eassumption. - admit. diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v index 845d706..0e999de 100644 --- a/src/verilog/Verilog.v +++ b/src/verilog/Verilog.v @@ -56,10 +56,10 @@ Definition merge_associations {A : Type} (assoc : associations A) := mkassociations (AssocMapExt.merge A assoc.(assoc_nonblocking) assoc.(assoc_blocking)) (AssocMap.empty A). -Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : option value := +Definition arr_assocmap_lookup (a : assocmap_arr) (r : reg) (i : nat) : value := match a ! r with - | None => None - | Some arr => nth_error arr i + | None => natToValue 32 0 + | Some arr => nth i arr (natToValue 32 0) end. Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) : list A := @@ -297,7 +297,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop | 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 -> + arr_assocmap_lookup stack r (valueToNat i) = v -> expr_runp fext reg stack (Vvari r iexp) v | erun_Vinputvar : forall fext reg stack r v, -- cgit