summaryrefslogtreecommitdiff
path: root/tests/coq/misc
diff options
context:
space:
mode:
authorSon HO2023-11-29 16:02:42 +0100
committerGitHub2023-11-29 16:02:42 +0100
commit789ba1473acd287814a0d659b5f5a0e480e4e9d7 (patch)
tree983ad685eb6b3c60b0baa3e3920dedbc6eaa0e57 /tests/coq/misc
parent90e42e0e1c1889aabfa66283fb15b43a5852a02a (diff)
parente732f97d09179fae43fafcb244340f98e3ca9229 (diff)
Merge pull request #39 from AeneasVerif/afromher_shifts
Add support for bitshifts
Diffstat (limited to 'tests/coq/misc')
-rw-r--r--tests/coq/misc/Bitwise.v38
-rw-r--r--tests/coq/misc/Primitives.v76
-rw-r--r--tests/coq/misc/_CoqProject1
3 files changed, 115 insertions, 0 deletions
diff --git a/tests/coq/misc/Bitwise.v b/tests/coq/misc/Bitwise.v
new file mode 100644
index 00000000..94771b37
--- /dev/null
+++ b/tests/coq/misc/Bitwise.v
@@ -0,0 +1,38 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [bitwise] *)
+Require Import Primitives.
+Import Primitives.
+Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
+Local Open Scope Primitives_scope.
+Module Bitwise.
+
+(** [bitwise::shift_u32]: forward function
+ Source: 'src/bitwise.rs', lines 3:0-3:31 *)
+Definition shift_u32 (a : u32) : result u32 :=
+ t <- u32_shr a 16%usize; u32_shl t 16%usize
+.
+
+(** [bitwise::shift_i32]: forward function
+ Source: 'src/bitwise.rs', lines 10:0-10:31 *)
+Definition shift_i32 (a : i32) : result i32 :=
+ t <- i32_shr a 16%isize; i32_shl t 16%isize
+.
+
+(** [bitwise::xor_u32]: forward function
+ Source: 'src/bitwise.rs', lines 17:0-17:37 *)
+Definition xor_u32 (a : u32) (b : u32) : result u32 :=
+ Return (u32_xor a b).
+
+(** [bitwise::or_u32]: forward function
+ Source: 'src/bitwise.rs', lines 21:0-21:36 *)
+Definition or_u32 (a : u32) (b : u32) : result u32 :=
+ Return (u32_or a b).
+
+(** [bitwise::and_u32]: forward function
+ Source: 'src/bitwise.rs', lines 25:0-25:37 *)
+Definition and_u32 (a : u32) (b : u32) : result u32 :=
+ Return (u32_and a b).
+
+End Bitwise.
diff --git a/tests/coq/misc/Primitives.v b/tests/coq/misc/Primitives.v
index 83f860b6..99ffe070 100644
--- a/tests/coq/misc/Primitives.v
+++ b/tests/coq/misc/Primitives.v
@@ -255,6 +255,12 @@ Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty
Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)).
+Axiom scalar_xor : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_or : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_and : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_shl : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
(* TODO: check the semantics of casts in Rust *)
Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) :=
@@ -372,6 +378,76 @@ Definition u32_mul := @scalar_mul U32.
Definition u64_mul := @scalar_mul U64.
Definition u128_mul := @scalar_mul U128.
+(** Xor *)
+Definition u8_xor := @scalar_xor U8.
+Definition u16_xor := @scalar_xor U16.
+Definition u32_xor := @scalar_xor U32.
+Definition u64_xor := @scalar_xor U64.
+Definition u128_xor := @scalar_xor U128.
+Definition usize_xor := @scalar_xor Usize.
+Definition i8_xor := @scalar_xor I8.
+Definition i16_xor := @scalar_xor I16.
+Definition i32_xor := @scalar_xor I32.
+Definition i64_xor := @scalar_xor I64.
+Definition i128_xor := @scalar_xor I128.
+Definition isize_xor := @scalar_xor Isize.
+
+(** Or *)
+Definition u8_or := @scalar_or U8.
+Definition u16_or := @scalar_or U16.
+Definition u32_or := @scalar_or U32.
+Definition u64_or := @scalar_or U64.
+Definition u128_or := @scalar_or U128.
+Definition usize_or := @scalar_or Usize.
+Definition i8_or := @scalar_or I8.
+Definition i16_or := @scalar_or I16.
+Definition i32_or := @scalar_or I32.
+Definition i64_or := @scalar_or I64.
+Definition i128_or := @scalar_or I128.
+Definition isize_or := @scalar_or Isize.
+
+(** And *)
+Definition u8_and := @scalar_and U8.
+Definition u16_and := @scalar_and U16.
+Definition u32_and := @scalar_and U32.
+Definition u64_and := @scalar_and U64.
+Definition u128_and := @scalar_and U128.
+Definition usize_and := @scalar_and Usize.
+Definition i8_and := @scalar_and I8.
+Definition i16_and := @scalar_and I16.
+Definition i32_and := @scalar_and I32.
+Definition i64_and := @scalar_and I64.
+Definition i128_and := @scalar_and I128.
+Definition isize_and := @scalar_and Isize.
+
+(** Shift left *)
+Definition u8_shl {ty} := @scalar_shl U8 ty.
+Definition u16_shl {ty} := @scalar_shl U16 ty.
+Definition u32_shl {ty} := @scalar_shl U32 ty.
+Definition u64_shl {ty} := @scalar_shl U64 ty.
+Definition u128_shl {ty} := @scalar_shl U128 ty.
+Definition usize_shl {ty} := @scalar_shl Usize ty.
+Definition i8_shl {ty} := @scalar_shl I8 ty.
+Definition i16_shl {ty} := @scalar_shl I16 ty.
+Definition i32_shl {ty} := @scalar_shl I32 ty.
+Definition i64_shl {ty} := @scalar_shl I64 ty.
+Definition i128_shl {ty} := @scalar_shl I128 ty.
+Definition isize_shl {ty} := @scalar_shl Isize ty.
+
+(** Shift right *)
+Definition u8_shr {ty} := @scalar_shr U8 ty.
+Definition u16_shr {ty} := @scalar_shr U16 ty.
+Definition u32_shr {ty} := @scalar_shr U32 ty.
+Definition u64_shr {ty} := @scalar_shr U64 ty.
+Definition u128_shr {ty} := @scalar_shr U128 ty.
+Definition usize_shr {ty} := @scalar_shr Usize ty.
+Definition i8_shr {ty} := @scalar_shr I8 ty.
+Definition i16_shr {ty} := @scalar_shr I16 ty.
+Definition i32_shr {ty} := @scalar_shr I32 ty.
+Definition i64_shr {ty} := @scalar_shr I64 ty.
+Definition i128_shr {ty} := @scalar_shr I128 ty.
+Definition isize_shr {ty} := @scalar_shr Isize ty.
+
(** Small utility *)
Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x).
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 0828bced..abbf6aa8 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -13,5 +13,6 @@ Constants.v
PoloniusList.v
NoNestedBorrows.v
External_FunsExternal.v
+Bitwise.v
External_TypesExternal_Template.v
External_FunsExternal_Template.v