From 58b59cce492f53ebd9aa960306f07f816c2e279d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 13 Apr 2019 15:58:38 +0200 Subject: Add a built-in function for "select" (strict conditional) The built-in is called `EF_select` and has type `(int, T, T) -> T` for a given Cminor type T. During instruction selection, it is turned into an `Osel` operation if available, otherwise into an if/then/else. --- cfrontend/Cexec.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 7f5fe355..fba00b35 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -501,6 +501,14 @@ Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := Some(w, E0, Vundef, m). +Definition do_ef_select (ty: typ) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match vargs with + | Vint n :: v1 :: v2 :: nil => + Some(w, E0, Val.normalize (if negb (Int.eq n Int.zero) then v1 else v2) ty, m) + | _ => None + end. + Definition do_external (ef: external_function): world -> list val -> mem -> option (world * trace * val * mem) := match ef with @@ -516,6 +524,7 @@ Definition do_external (ef: external_function): | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs + | EF_select ty => do_ef_select ty end. Lemma do_ef_external_sound: @@ -568,6 +577,10 @@ Proof with try congruence. eapply do_inline_assembly_sound; eauto. (* EF_debug *) unfold do_ef_debug. mydestr. split; constructor. +(* EF_select *) + unfold do_ef_select. destruct vargs... destruct v... destruct vargs... destruct vargs... destruct vargs... mydestr. + split. constructor. constructor. + constructor. Qed. Lemma do_ef_external_complete: @@ -612,6 +625,8 @@ Proof. eapply do_inline_assembly_complete; eauto. (* EF_debug *) inv H. inv H0. reflexivity. +(* EF_select *) + inv H. inv H0. inv H1. reflexivity. Qed. (** * Reduction of expressions *) -- cgit