From 9c684ec45620edff6deb57ace7d38d80304f682d Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Wed, 15 Sep 2021 03:54:30 +0300 Subject: Progress with callstate proof --- src/hls/HTLgenproof.v | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 4fda550..c8becf5 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -1514,19 +1514,22 @@ Section CORRECTNESS. - repeat apply regs_lessdef_add_greater; try not_control_reg. eauto using match_args. - edestruct no_stack_calls; eauto. - + replace (RTL.fn_stacksize f) with 0 in * - by assumption. - replace m' with m - by (destruct (mem_alloc_zero m); crush). - assumption. + + replace (RTL.fn_stacksize f) in *. + eauto using mem_alloc_zero_match_frames. + subst. inv MF. constructor. - big_tac. - admit. + destruct (Mem.load AST.Mint32 m' stk (Ptrofs.unsigned (Ptrofs.repr (4 * ptr)))) eqn:eq_load; repeat constructor. + erewrite (Mem.load_alloc_same m _ _ m' _ _ _ _ v); eauto; repeat econstructor. - eauto using stack_based_non_pointers. - (* Stack based stack pointer *) unfold arr_stack_based_pointers; intros. - admit. - - (* Stack bounds *) + destruct (Mem.loadv AST.Mint32 m' + (Values.Val.offset_ptr (Values.Vptr stk Ptrofs.zero) (Ptrofs.repr (4 * ptr)))) eqn:eq_load. + + simpl. + unfold Mem.loadv in *; simplify. + erewrite (Mem.load_alloc_same m _ _ m' _ _ _ _ v); eauto; repeat econstructor. + + crush. + - constructor; unfold Mem.loadv, Mem.storev; big_tac. admit. - constructor; simplify. + rewrite AssocMap.gss; crush. -- cgit