From 10da6dfa77f155d9d1e36e28c8bb8552601355f9 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 18:21:55 +0100 Subject: update kvx --- kvx/Asmblockdeps.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kvx/Asmblockdeps.v') diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index 67430b54..b6d18c3e 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -398,8 +398,8 @@ Definition control_eval (o: control_op) (l: list value) := end | Ocbu bt l, [Val v; Val vpc] => match cmpu_for_btest bt with - | (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0))) - | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0))) + | (Some c, Int) => eval_branch_deps fn l vpc (Val.mxcmpu_bool c v (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch_deps fn l vpc (Val.mxcmplu_bool c v (Vlong (Int64.repr 0))) | (None, _) => None end | Odiv, [Val v1; Val v2] => @@ -1232,12 +1232,12 @@ Proof. (* Pcbu *) + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. - ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. + ++ destruct (Val.mxcmpu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b. + ++ destruct (Val.mxcmplu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. -- cgit