From 26775b65ba98ad798fc72c92ae73bd28609aaeb8 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Jun 2019 08:48:20 +0200 Subject: ARM: select is not supported at type Tlong --- arm/SelectOp.vp | 9 ++++++++- arm/SelectOpproof.v | 4 +++- 2 files changed, 11 insertions(+), 2 deletions(-) (limited to 'arm') diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 61ea6283..d04832d6 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -383,7 +383,14 @@ Definition compfs (c: comparison) (e1: expr) (e2: expr) := Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil). Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := - Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)). + if match ty with + | Tint => true + | Tfloat => true + | Tsingle => true + | _ => false + end + then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)) + else None. (** ** Integer conversions *) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index f281f7ce..8b546971 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -746,7 +746,9 @@ Theorem eval_select: eval_expr ge sp e m le a v /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v. Proof. - unfold select; intros; inv H. rewrite <- H3; TrivialExists. + unfold select; intros. + destruct (match ty with Tint | Tfloat | Tsingle => true | _ => false end); inv H. + rewrite <- H3; TrivialExists. Qed. Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). -- cgit From ddb2c968e6c57d2117434f169471d87f643d831a Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 6 Jun 2019 17:56:10 +0200 Subject: Added Pfmovite to list of known mnemonic names. --- arm/AsmToJSON.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'arm') diff --git a/arm/AsmToJSON.ml b/arm/AsmToJSON.ml index dfad6972..6ba3f1bc 100644 --- a/arm/AsmToJSON.ml +++ b/arm/AsmToJSON.ml @@ -29,7 +29,7 @@ let mnemonic_names = [ "Padc"; "Padd"; "Padds"; "Pand";"Pannot"; "Pasr"; "Pb"; " "Pfsts"; "Pfsubd"; "Pfsubs"; "Pftosizd"; "Pftosizs"; "Pftouizd"; "Pftouizs"; "Pfuitod"; "Pfuitos"; "Pinlineasm"; "Pisb"; "Plabel"; "Pldr"; "Ploadsymbol_lbl"; "Pldr_p"; "Pldrb"; "Pldrb_p"; "Pldrh"; "Pldrh_p"; "Pldrsb"; - "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; + "Pldrsh"; "Plsl"; "Plsr"; "Pmla"; "Pmov"; "Pmovite"; "Pfmovite"; "Pmovt"; "Pmovw"; "Pmul"; "Pmvn"; "Ploadsymbol_imm"; "Pnop"; "Porr"; "Ppush"; "Prev"; "Prev16"; "Prsb"; "Prsbs"; "Prsc"; "Psbc"; "Psbfx"; "Psdiv"; "Psmull"; "Pstr"; "Pstr_p"; "Pstrb"; "Pstrb_p"; "Pstrh"; "Pstrh_p"; "Psub"; "Psubs"; "Pudiv"; -- cgit