diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-15 03:54:30 +0300 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-09-15 03:54:30 +0300 |
| commit | 9c684ec45620edff6deb57ace7d38d80304f682d (patch) | |
| tree | 4bfe3a30ffbadd8d904b00196e0f5fdfc462acf3 | |
| parent | bf4197f480a7af3c52fe038a3483ba1857b0c13d (diff) | |
| download | vericert-9c684ec45620edff6deb57ace7d38d80304f682d.tar.gz vericert-9c684ec45620edff6deb57ace7d38d80304f682d.zip | |
Progress with callstate proof
| -rw-r--r-- | src/hls/HTLgenproof.v | 19 |
1 files 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. |