From eaae75e487a82021cc615856b31f86bd05853b1e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 16 Feb 2022 09:32:24 +0100 Subject: builtins pour signed div/mod --- kvx/Builtins1.v | 32 +++++++++++++++++++ kvx/CBuiltins.ml | 8 +++++ kvx/SelectOp.vp | 16 ++++++++++ kvx/SelectOpproof.v | 88 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 144 insertions(+) diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index e3e4f95d..5536e58c 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -32,6 +32,10 @@ Inductive platform_builtin : Type := | BI_fp_udiv64 | BI_fp_umod32 | BI_fp_umod64 +| BI_fp_sdiv32 +| BI_fp_sdiv64 +| BI_fp_smod32 +| BI_fp_smod64 | BI_abs | BI_absl. @@ -50,6 +54,10 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fp_udiv64", BI_fp_udiv64) :: ("__builtin_fp_umod32", BI_fp_umod32) :: ("__builtin_fp_umod64", BI_fp_umod64) + :: ("__builtin_fp_sdiv32", BI_fp_sdiv32) + :: ("__builtin_fp_sdiv64", BI_fp_sdiv64) + :: ("__builtin_fp_smod32", BI_fp_smod32) + :: ("__builtin_fp_smod64", BI_fp_smod64) :: ("__builtin_abs", BI_abs) :: ("__builtin_absl", BI_absl) :: nil. @@ -74,6 +82,14 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tint :: Tint :: nil) Tint cc_default | BI_fp_umod64 => mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_fp_sdiv32 => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_fp_sdiv64 => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default + | BI_fp_smod32 => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_fp_smod64 => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default | BI_abs => mksignature (Tint :: nil) Tint cc_default | BI_absl => @@ -106,6 +122,22 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl (fun n1 n2 => if Int64.eq n2 Int64.zero then None else Some (Int64.modu n1 n2)) + | BI_fp_sdiv32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.divs n1 n2)) + | BI_fp_sdiv64 => mkbuiltin_n2p Tlong Tlong Tlong + (fun n1 n2 => if Int64.eq n2 Int64.zero + then None + else Some (Int64.divs n1 n2)) + | BI_fp_smod32 => mkbuiltin_n2p Tint Tint Tint + (fun n1 n2 => if Int.eq n2 Int.zero + then None + else Some (Int.mods n1 n2)) + | BI_fp_smod64 => mkbuiltin_n2p Tlong Tlong Tlong + (fun n1 n2 => if Int64.eq n2 Int64.zero + then None + else Some (Int64.mods n1 n2)) | BI_abs => mkbuiltin_n1t Tint Tint ExtValues.int_abs | BI_absl => mkbuiltin_n1t Tlong Tlong ExtValues.long_abs end. diff --git a/kvx/CBuiltins.ml b/kvx/CBuiltins.ml index d712eecd..c0b69adf 100644 --- a/kvx/CBuiltins.ml +++ b/kvx/CBuiltins.ml @@ -145,6 +145,14 @@ let builtins = { (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); "__builtin_fp_umod64", (TInt(IULong, []), [TInt(IULong, []); TInt(IULong, [])], false); + "__builtin_fp_sdiv32", + (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); + "__builtin_fp_sdiv64", + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); + "__builtin_fp_smod32", + (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); + "__builtin_fp_smod64", + (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); "__builtin_abs", (TInt(IInt, []), [TInt(IInt, [])], false); "__builtin_absl", diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index 63c7d73b..5225a71c 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -788,6 +788,22 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr | a:::b:::Enil => Some (FPDivision64.fp_modu64 a b) | _ => None end) + | BI_fp_sdiv32 => (match args with + | a:::b:::Enil => Some (FPDivision32.fp_divs32 a b) + | _ => None + end) + | BI_fp_sdiv64 => (match args with + | a:::b:::Enil => Some (FPDivision64.fp_divs64 a b) + | _ => None + end) + | BI_fp_smod32 => (match args with + | a:::b:::Enil => Some (FPDivision32.fp_mods32 a b) + | _ => None + end) + | BI_fp_smod64 => (match args with + | a:::b:::Enil => Some (FPDivision64.fp_mods64 a b) + | _ => None + end) | BI_abs => gen_abs args | BI_absl => gen_absl args end. diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index a45d367f..19393091 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -2046,6 +2046,94 @@ Proof. } inv EVAL. constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int.eq in EVAL. + change (Int.unsigned Int.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vint (Int.divs i i0)). split. + { + apply FPDivision32.fp_divs32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.divs i i0)). split. + { + apply FPDivision64.fp_divs64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int.eq in EVAL. + change (Int.unsigned Int.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vint (Int.mods i i0)). split. + { + apply FPDivision32.fp_mods32_correct; auto. + pose proof (Int.unsigned_range i0). + lia. + } + inv EVAL. + constructor. + - cbn in *. + intro EVAL. + inv EVAL. discriminate. + inv H0. discriminate. + inv H2. 2: discriminate. + inv Heval. + intro EVAL. + destruct v1; try discriminate. + destruct v0; try discriminate. + unfold Int64.eq in EVAL. + change (Int64.unsigned Int64.zero) with 0 in EVAL. + unfold zeq in EVAL. + destruct (Z.eq_dec (Int64.unsigned i0) 0) as [EQ | NEQ]. + { discriminate. } + exists (Vlong (Int64.mods i i0)). split. + { + apply FPDivision64.fp_mods64_correct; auto. + pose proof (Int64.unsigned_range i0). + lia. + } + inv EVAL. + constructor. - apply eval_abs; assumption. - apply eval_absl; assumption. Qed. -- cgit