Merge pull request #1833 from GaloisInc/T1828

`write_aig`: Normalize symmetry in multiplication

intTests/test1788/Makefile

@@ -0,0 +1,17 @@
+CC = clang
+CFLAGS = -g -frecord-command-line -O0
+
+all: test.bc test.exe
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c -emit-llvm $< -o $@
+
+test.o: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+test.exe: test.o
+	$(CC) $(CFLAGS) $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc test.exe

intTests/test1788/test.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t mult(uint32_t x) {
+  return x * 0x85EBCA77U;
+}

intTests/test1788/test.saw

@@ -0,0 +1,13 @@
+// This test case ensures that ABC can prove that a C implementation of the
+// `mult` function is equivalent to a direct Cryptol implementation of the
+// same function.
+
+let
+{{
+cryptol_mult : [32] -> [32]
+cryptol_mult x = x * 0x85EBCA77
+}};
+
+m <- llvm_load_module "test.bc";
+llvm_mult <- llvm_extract m "mult";
+prove abc {{ \x -> llvm_mult x == cryptol_mult x }};

intTests/test1788/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

intTests/test1828/.gitignore

@@ -0,0 +1,2 @@
+left.aig
+right.aig

intTests/test1828/test.saw

@@ -0,0 +1,2 @@
+write_aig "left.aig" {{ \x -> x * 0x12345678 }};
+write_aig "right.aig" {{ \x -> 0x12345678 * x }};

intTests/test1828/test.sh

@@ -0,0 +1,9 @@
+set -e
+
+# This test case uses `write_aiger` to produce AIG files for two nearly
+# identical functions, where the only difference is the order of arguments (one
+# symbolic and one concrete) in a bitvector multiplication. If the `aig` library
+# does its job correctly, these should produce identical AIG files, so check
+# this using `diff`.
+$SAW test.saw
+diff -ru left.aig right.aig