From d0257b0a47ad998e01715e9bc6ba612b834765f1 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 11 Jun 2020 14:47:52 +0100 Subject: Working on proof. --- src/translation/HTLgenspec.v | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 4bf3843..89b79ac 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -184,14 +184,15 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk m, + forall data control fin rtrn st stk stk_len m, (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) -> + tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> + stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk fin rtrn) -> + st stk stk_len fin rtrn) -> tr_module f m. Hint Constructors tr_module : htlspec. @@ -379,6 +380,12 @@ Proof. Qed. Hint Resolve iter_expand_instr_spec : htlspec. +Lemma create_arr_inv : forall x y z a b c d, + create_arr x y z = OK (a, b) c d -> y = b. +Proof. + inversion 1. reflexivity. +Qed. + Theorem transl_module_correct : forall f m, transl_module f = Errors.OK m -> tr_module f m. @@ -392,6 +399,11 @@ Proof. unfold transf_module in *. monadInv Heqr. + + (* TODO: We should be able to fold this into the automation. *) + pose proof (create_arr_inv _ _ _ _ _ _ _ EQ0) as STK_LEN. + rewrite <- STK_LEN. + econstructor; simpl; trivial. intros. inv_incr. -- cgit From eacdec2dd13611f94fe12a41cf04cf38dc389092 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Fri, 12 Jun 2020 18:13:52 +0100 Subject: Fix broken proof. --- src/translation/HTLgenspec.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 57d2d87..57d7d62 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -433,8 +433,8 @@ Proof. Qed. Hint Resolve iter_expand_instr_spec : htlspec. -Lemma create_arr_inv : forall x y z a b c d, - create_arr x y z = OK (a, b) c d -> y = b. +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. Proof. inversion 1. reflexivity. Qed. @@ -454,14 +454,14 @@ Proof. monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) - pose proof (create_arr_inv _ _ _ _ _ _ _ EQ0) as STK_LEN. + pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. rewrite <- STK_LEN. econstructor; simpl; trivial. intros. inv_incr. assert (EQ3D := EQ3). - destruct x3. + destruct x4. apply collect_declare_datapath_trans in EQ3. apply collect_declare_controllogic_trans in EQ3D. assert (STC: st_controllogic s10 = st_controllogic s3) by congruence. -- cgit From 58f0022a8b5f9ab42e1a8515a77820a9d086ba76 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Wed, 17 Jun 2020 20:05:05 +0100 Subject: Use NBAs for loads and stores. --- src/translation/HTLgenspec.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 57d7d62..1a9144c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -163,11 +163,11 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt - | tr_instr_Iload : forall mem addr args s s' i c dst n, 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) (block dst c) (state_goto st n) + 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, 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) (Vblock c (Vvar src)) + tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src)) (state_goto st n). Hint Constructors tr_instr : htlspec. -- cgit From b59a2e2913aa7ad010c0652e909ae790c07c7281 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Thu, 18 Jun 2020 17:47:21 +0100 Subject: Enforce stack size alignment to fix proof. --- src/translation/HTLgenspec.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index 1a9144c..a916cb5 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -188,6 +188,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := (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 -> m = (mkmodule f.(RTL.fn_params) data control @@ -451,7 +452,7 @@ Proof. inversion s; subst. unfold transf_module in *. - monadInv Heqr. + destruct (Z.eq_dec (RTL.fn_stacksize f mod 4) 0); monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) pose proof (create_arr_inv _ _ _ _ _ _ _ _ EQ0) as STK_LEN. -- cgit