aboutsummaryrefslogtreecommitdiffstatshomepage
path: root/validation
diff options
authorLuc Van Oostenryck <luc.vanoostenryck@gmail.com>2020-11-28 10:58:14 +0100
committerLuc Van Oostenryck <luc.vanoostenryck@gmail.com>2020-11-28 10:58:14 +0100
commit3bc348f6eea9b74fa93e72ea77e70b05a29b97eb (patch)
treee547a945fd6e6a59645ac542829b5f285e1e7cc5 /validation
parentf50c482ebabe3572cdd8a97d8b51ca94e44aba3a (diff)
parentcafabc769e77f14e47ab44866b304e51af42c44c (diff)
downloadsparse-dev-3bc348f6eea9b74fa93e72ea77e70b05a29b97eb.tar.gz
Merge branch 'bit-trans' into next
* factorize (x OP1 z) OP2 (y OP1 z) into (x OP2 y) OP1 z * factorize SHIFT(x, s) OP SHIFT(y, s) into SHIFT((x OP y), s) * factorize SEL(x, OP(y,z), y) into OP(SEL(x, z, 0), y) * convert SEL(x & BIT1, BIT2, 0) into SHIFT(x & BIT1, S)
Diffstat (limited to 'validation')
-rw-r--r--validation/optim/fact-add-mul.c27
-rw-r--r--validation/optim/fact-and-ior.c27
-rw-r--r--validation/optim/fact-and-shift.c26
-rw-r--r--validation/optim/fact-ior-and.c27
-rw-r--r--validation/optim/fact-ior-shift.c26
-rw-r--r--validation/optim/fact-select01.c25
-rw-r--r--validation/optim/fact-xor-and.c27
-rw-r--r--validation/optim/fact-xor-shift.c26
-rw-r--r--validation/optim/select-and-shift.c17
9 files changed, 228 insertions, 0 deletions
diff --git a/validation/optim/fact-add-mul.c b/validation/optim/fact-add-mul.c
new file mode 100644
index 00000000..9da6d71c
--- /dev/null
+++ b/validation/optim/fact-add-mul.c
@@ -0,0 +1,27 @@
+int fr_abx(int a, int b, int x) { return ((a * x) + (b * x)) == ((a + b) * x); }
+int fl_abx(int a, int b, int x) { return ((x * a) + (x * b)) == ((a + b) * x); }
+int fm_abx(int a, int b, int x) { return ((a * x) + (x * b)) == ((a + b) * x); }
+int fn_abx(int a, int b, int x) { return ((x * a) + (b * x)) == ((a + b) * x); }
+
+int fr_bax(int b, int a, int x) { return ((a * x) + (b * x)) == ((b + a) * x); }
+int fl_bax(int b, int a, int x) { return ((x * a) + (x * b)) == ((b + a) * x); }
+int fm_bax(int b, int a, int x) { return ((a * x) + (x * b)) == ((b + a) * x); }
+int fn_bax(int b, int a, int x) { return ((x * a) + (b * x)) == ((b + a) * x); }
+
+int fr_axb(int a, int x, int b) { return ((a * x) + (b * x)) == ((a + b) * x); }
+int fl_axb(int a, int x, int b) { return ((x * a) + (x * b)) == ((a + b) * x); }
+int fm_axb(int a, int x, int b) { return ((a * x) + (x * b)) == ((a + b) * x); }
+int fn_axb(int a, int x, int b) { return ((x * a) + (b * x)) == ((a + b) * x); }
+
+int fr_bxa(int b, int x, int a) { return ((b * x) + (a * x)) == ((b + a) * x); }
+int fl_bxa(int b, int x, int a) { return ((x * b) + (x * a)) == ((b + a) * x); }
+int fm_bxa(int b, int x, int a) { return ((b * x) + (x * a)) == ((b + a) * x); }
+int fn_bxa(int b, int x, int a) { return ((x * b) + (a * x)) == ((b + a) * x); }
+
+/*
+ * check-name: fact-add-mul
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-and-ior.c b/validation/optim/fact-and-ior.c
new file mode 100644
index 00000000..96466616
--- /dev/null
+++ b/validation/optim/fact-and-ior.c
@@ -0,0 +1,27 @@
+int fr_abx(int a, int b, int x) { return ((a | x) & (b | x)) == ((a & b) | x); }
+int fl_abx(int a, int b, int x) { return ((x | a) & (x | b)) == ((a & b) | x); }
+int fm_abx(int a, int b, int x) { return ((a | x) & (x | b)) == ((a & b) | x); }
+int fn_abx(int a, int b, int x) { return ((x | a) & (b | x)) == ((a & b) | x); }
+
+int fr_bax(int b, int a, int x) { return ((a | x) & (b | x)) == ((b & a) | x); }
+int fl_bax(int b, int a, int x) { return ((x | a) & (x | b)) == ((b & a) | x); }
+int fm_bax(int b, int a, int x) { return ((a | x) & (x | b)) == ((b & a) | x); }
+int fn_bax(int b, int a, int x) { return ((x | a) & (b | x)) == ((b & a) | x); }
+
+int fr_axb(int a, int x, int b) { return ((a | x) & (b | x)) == ((a & b) | x); }
+int fl_axb(int a, int x, int b) { return ((x | a) & (x | b)) == ((a & b) | x); }
+int fm_axb(int a, int x, int b) { return ((a | x) & (x | b)) == ((a & b) | x); }
+int fn_axb(int a, int x, int b) { return ((x | a) & (b | x)) == ((a & b) | x); }
+
+int fr_bxa(int b, int x, int a) { return ((b | x) & (a | x)) == ((b & a) | x); }
+int fl_bxa(int b, int x, int a) { return ((x | b) & (x | a)) == ((b & a) | x); }
+int fm_bxa(int b, int x, int a) { return ((b | x) & (x | a)) == ((b & a) | x); }
+int fn_bxa(int b, int x, int a) { return ((x | b) & (a | x)) == ((b & a) | x); }
+
+/*
+ * check-name: fact-and-ior
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-and-shift.c b/validation/optim/fact-and-shift.c
new file mode 100644
index 00000000..e9eb9cce
--- /dev/null
+++ b/validation/optim/fact-and-shift.c
@@ -0,0 +1,26 @@
+typedef unsigned int uint;
+typedef signed int sint;
+
+
+uint fact_and_shl(uint a, uint b, uint s)
+{
+ return ((a << s) & (b << s)) == ((a & b) << s);
+}
+
+uint fact_and_lsr(uint a, uint b, uint s)
+{
+ return ((a >> s) & (b >> s)) == ((a & b) >> s);
+}
+
+sint fact_and_asr(sint a, sint b, sint s)
+{
+ return ((a >> s) & (b >> s)) == ((a & b) >> s);
+}
+
+/*
+ * check-name: fact-and-shift
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-ior-and.c b/validation/optim/fact-ior-and.c
new file mode 100644
index 00000000..a6ad3c45
--- /dev/null
+++ b/validation/optim/fact-ior-and.c
@@ -0,0 +1,27 @@
+int fr_abx(int a, int b, int x) { return ((a & x) | (b & x)) == ((a | b) & x); }
+int fl_abx(int a, int b, int x) { return ((x & a) | (x & b)) == ((a | b) & x); }
+int fm_abx(int a, int b, int x) { return ((a & x) | (x & b)) == ((a | b) & x); }
+int fn_abx(int a, int b, int x) { return ((x & a) | (b & x)) == ((a | b) & x); }
+
+int fr_bax(int b, int a, int x) { return ((a & x) | (b & x)) == ((b | a) & x); }
+int fl_bax(int b, int a, int x) { return ((x & a) | (x & b)) == ((b | a) & x); }
+int fm_bax(int b, int a, int x) { return ((a & x) | (x & b)) == ((b | a) & x); }
+int fn_bax(int b, int a, int x) { return ((x & a) | (b & x)) == ((b | a) & x); }
+
+int fr_axb(int a, int x, int b) { return ((a & x) | (b & x)) == ((a | b) & x); }
+int fl_axb(int a, int x, int b) { return ((x & a) | (x & b)) == ((a | b) & x); }
+int fm_axb(int a, int x, int b) { return ((a & x) | (x & b)) == ((a | b) & x); }
+int fn_axb(int a, int x, int b) { return ((x & a) | (b & x)) == ((a | b) & x); }
+
+int fr_bxa(int b, int x, int a) { return ((b & x) | (a & x)) == ((b | a) & x); }
+int fl_bxa(int b, int x, int a) { return ((x & b) | (x & a)) == ((b | a) & x); }
+int fm_bxa(int b, int x, int a) { return ((b & x) | (x & a)) == ((b | a) & x); }
+int fn_bxa(int b, int x, int a) { return ((x & b) | (a & x)) == ((b | a) & x); }
+
+/*
+ * check-name: fact-ior-and
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-ior-shift.c b/validation/optim/fact-ior-shift.c
new file mode 100644
index 00000000..5fa91eb5
--- /dev/null
+++ b/validation/optim/fact-ior-shift.c
@@ -0,0 +1,26 @@
+typedef unsigned int uint;
+typedef signed int sint;
+
+
+uint fact_ior_shl(uint a, uint b, uint s)
+{
+ return ((a << s) | (b << s)) == ((a | b) << s);
+}
+
+uint fact_ior_lsr(uint a, uint b, uint s)
+{
+ return ((a >> s) | (b >> s)) == ((a | b) >> s);
+}
+
+sint fact_ior_asr(sint a, sint b, sint s)
+{
+ return ((a >> s) | (b >> s)) == ((a | b) >> s);
+}
+
+/*
+ * check-name: fact-ior-shift
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-select01.c b/validation/optim/fact-select01.c
new file mode 100644
index 00000000..9232fc90
--- /dev/null
+++ b/validation/optim/fact-select01.c
@@ -0,0 +1,25 @@
+int add_yx_y(int p, int x, int y) { return (p ? (y+x) : y) == ((p ? x : 0) + y); }
+int add_xy_y(int p, int y, int x) { return (p ? (x+y) : y) == ((p ? x : 0) + y); }
+int add_xy_x(int p, int x, int y) { return (p ? (x+y) : x) == ((p ? y : 0) + x); }
+int add_yx_x(int p, int y, int x) { return (p ? (y+x) : x) == ((p ? y : 0) + x); }
+int add_y_yx(int p, int x, int y) { return (p ? y : (y+x)) == ((p ? 0 : x) + y); }
+
+int ior_yx_y(int p, int x, int y) { return (p ? (y|x) : y) == ((p ? x : 0) | y); }
+int ior_xy_y(int p, int y, int x) { return (p ? (x|y) : y) == ((p ? x : 0) | y); }
+int ior_xy_x(int p, int x, int y) { return (p ? (x|y) : x) == ((p ? y : 0) | x); }
+int ior_yx_x(int p, int y, int x) { return (p ? (y|x) : x) == ((p ? y : 0) | x); }
+int ior_y_yx(int p, int x, int y) { return (p ? y : (y|x)) == ((p ? 0 : x) | y); }
+
+int xor_yx_y(int p, int x, int y) { return (p ? (y^x) : y) == ((p ? x : 0) ^ y); }
+int xor_xy_y(int p, int y, int x) { return (p ? (x^y) : y) == ((p ? x : 0) ^ y); }
+int xor_xy_x(int p, int x, int y) { return (p ? (x^y) : x) == ((p ? y : 0) ^ x); }
+int xor_yx_x(int p, int y, int x) { return (p ? (y^x) : x) == ((p ? y : 0) ^ x); }
+int xor_y_yx(int p, int x, int y) { return (p ? y : (y^x)) == ((p ? 0 : x) ^ y); }
+
+/*
+ * check-name: fact-select01
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-xor-and.c b/validation/optim/fact-xor-and.c
new file mode 100644
index 00000000..62232b29
--- /dev/null
+++ b/validation/optim/fact-xor-and.c
@@ -0,0 +1,27 @@
+int fr_abx(int a, int b, int x) { return ((a & x) ^ (b & x)) == ((a ^ b) & x); }
+int fl_abx(int a, int b, int x) { return ((x & a) ^ (x & b)) == ((a ^ b) & x); }
+int fm_abx(int a, int b, int x) { return ((a & x) ^ (x & b)) == ((a ^ b) & x); }
+int fn_abx(int a, int b, int x) { return ((x & a) ^ (b & x)) == ((a ^ b) & x); }
+
+int fr_bax(int b, int a, int x) { return ((a & x) ^ (b & x)) == ((b ^ a) & x); }
+int fl_bax(int b, int a, int x) { return ((x & a) ^ (x & b)) == ((b ^ a) & x); }
+int fm_bax(int b, int a, int x) { return ((a & x) ^ (x & b)) == ((b ^ a) & x); }
+int fn_bax(int b, int a, int x) { return ((x & a) ^ (b & x)) == ((b ^ a) & x); }
+
+int fr_axb(int a, int x, int b) { return ((a & x) ^ (b & x)) == ((a ^ b) & x); }
+int fl_axb(int a, int x, int b) { return ((x & a) ^ (x & b)) == ((a ^ b) & x); }
+int fm_axb(int a, int x, int b) { return ((a & x) ^ (x & b)) == ((a ^ b) & x); }
+int fn_axb(int a, int x, int b) { return ((x & a) ^ (b & x)) == ((a ^ b) & x); }
+
+int fr_bxa(int b, int x, int a) { return ((b & x) ^ (a & x)) == ((b ^ a) & x); }
+int fl_bxa(int b, int x, int a) { return ((x & b) ^ (x & a)) == ((b ^ a) & x); }
+int fm_bxa(int b, int x, int a) { return ((b & x) ^ (x & a)) == ((b ^ a) & x); }
+int fn_bxa(int b, int x, int a) { return ((x & b) ^ (a & x)) == ((b ^ a) & x); }
+
+/*
+ * check-name: fact-xor-and
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/fact-xor-shift.c b/validation/optim/fact-xor-shift.c
new file mode 100644
index 00000000..5fb228bd
--- /dev/null
+++ b/validation/optim/fact-xor-shift.c
@@ -0,0 +1,26 @@
+typedef unsigned int uint;
+typedef signed int sint;
+
+
+uint fact_xor_shl(uint a, uint b, uint s)
+{
+ return ((a << s) ^ (b << s)) == ((a ^ b) << s);
+}
+
+uint fact_xor_lsr(uint a, uint b, uint s)
+{
+ return ((a >> s) ^ (b >> s)) == ((a ^ b) >> s);
+}
+
+sint fact_xor_asr(sint a, sint b, sint s)
+{
+ return ((a >> s) ^ (b >> s)) == ((a ^ b) >> s);
+}
+
+/*
+ * check-name: fact-xor-shift
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */
diff --git a/validation/optim/select-and-shift.c b/validation/optim/select-and-shift.c
new file mode 100644
index 00000000..5313fe4b
--- /dev/null
+++ b/validation/optim/select-and-shift.c
@@ -0,0 +1,17 @@
+#define S1 2
+#define S2 5
+#define S (S2 - S1)
+
+#define A (1 << S1)
+#define B (1 << S2)
+
+int foo(int p) { return ((p & A) ? B : 0) == ((((unsigned)p) & A) << S); }
+int bar(int p) { return ((p & B) ? A : 0) == ((((unsigned)p) & B) >> S); }
+
+/*
+ * check-name: select-and-shift
+ * check-command: test-linearize -Wno-decl $file
+ *
+ * check-output-ignore
+ * check-output-returns: 1
+ */