write_aig: Normalize symmetry in multiplication

[RyanGlScott]

This bumps the aig submodule to bring in the changes from GaloisInc/aig#14, which changes how aig performs multiplication to swap the order of arguments if the second argument is a constant. This has two benefits:

• This ensures that write_aig will produce the same networks for X * C and C * X, where C is a constant and X is a variable.
• The algorithm that mul uses to compute multiplication is biased in its order of arguments, and having the first argument be a constant tends to produce networks that ABC has an easier time verifying. (The FFS example under doc/tutorial/code/ffs.c is a notable example of this.)

I have added a test case to check to see if the test case from #1828 now produces identical AIGs regardless of the order of arguments. Since this addresses many of the symptoms of #1788, I've also added a test case for #1788.

Fixes #1828.

[RyanGlScott]

Unfortunately, this appears to cause the test_tutorial1 test case to hang:

  test_tutorial1:                     TIMEOUT (500.10s)
    Timed out after 500s
    Use -p '/test_tutorial1/' to rerun this test only.

I will mark this as a draft until I figure out why this happens.

[RyanGlScott]

A smaller example of the issue, distilled from ffs_llvm.saw:

// bug.c
#include <stdint.h>

// returns the index of the first non-zero bit
uint32_t ffs_ref(uint32_t word) {
    int i = 0;
    if(!word)
        return 0;
    for(int cnt = 0; cnt < 32; cnt++)
        if(((1 << i++) & word) != 0)
            return i;
    return 0; // notreached
}

uint32_t ffs_musl (uint32_t x)
{
  static const char debruijn32[32] = {
    0, 1, 23, 2, 29, 24, 19, 3, 30, 27, 25, 11, 20, 8, 4, 13,
    31, 22, 28, 18, 26, 10, 7, 12, 21, 17, 9, 6, 16, 5, 15, 14
  };
  return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0;
}

// bug.saw
print "Extracting reference term: ffs_ref";
l <- llvm_load_module "bug.bc";
ffs_ref <- llvm_extract l "ffs_ref";

print "Extracting implementation term: ffs_musl";
ffs_musl <- llvm_extract l "ffs_musl";

print "Proving equivalence: ffs_ref == ffs_musl";
let thm2 = {{ \x -> ffs_ref x == ffs_musl x }};
result <- prove abc thm2;
print result;

print "Done.";

With this patch, running bug.saw will spin forever:

$ clang -c -g -emit-llvm bug.c
$ ./bin/saw bug.saw



[20:14:48.132] Loading file "/home/rscott/Documents/Hacking/Haskell/saw-script/bug.saw"
[20:14:48.133] Extracting reference term: ffs_ref
[20:14:48.146] Extracting implementation term: ffs_musl
[20:14:48.148] Proving equivalence: ffs_ref == ffs_musl
# Hangs when calling out to abc

Most likely, this is due to the use of multiplication in the implementation of ffs_musl. In particular, I suspect that Crucible would generate an expression that looks like 0x076be629 * x (where x is symbolic), and this aig patch would rewrite that to x * 0x076be629 before generating an AIGER file. To be honest, I am surprised that abc is unable to handle the resulting AIGER file, given that it should be using more full adders (and should, in theory, more easier for a tool like abc to handle).

One possible solution would be to change the implementation of mul' in aig to bias the arguments in the opposite order. I'll give that a shot.

[RyanGlScott]

One possible solution would be to change the implementation of mul' in aig to bias the arguments in the opposite order.

That didn't work. And indeed, the root of the issue is that abc seems to have a harder time proving that ffs_musl is equivalent to ffs_ref when the multiplication is expressed as 0x076be629 * x (which results in more full adders) as opposed to the multiplication is expressed as x * 0x076be629 (which results in fewer full adders). The order of the arguments isn't really important here: it's the shape of the resulting AIG file.

Unfortunately, I'm not really sure what to do here, as this implies that the approach to normalizing multiplication, while beneficial for the particular test program in in #1828, is at odds with proving the two ffs implementations equivalent...

[RyanGlScott]

Oops, this was closed accidentally by #1835 misattributing the issue number. Reopening.

[RyanGlScott]

For the sake of analyzing this outside of SAW, here is the .aig file that prove abc thm2 produces before this patch: thm2_before.txt (This is a .txt file only because GitHub won't let me upload .aig files—you will have to change the file extension yourself.)

$ abc -q "read_aiger thm2_before.aig; sat; write_cex thm2_before.cex"    
UNSATISFIABLE  Time =    22.75 sec
Counter-example is not available.

And after this patch: thm2_after.txt

$ abc -q "read_aiger thm2_after.aig; sat; write_cex thm2_after.cex"
# Hangs

[RyanGlScott]

I've pushed a new version of the PR that does not try to maximize the number full adders used in the AIGs that multiplication produces. We still achieve the end result of making X * C and C * X (where C is a constant and X is a variable) produce the same AIGs, which is enough to make the program in #1788 work. I've added that program as a test case.