Assert fail in Bdc_ManAlloc function

[NanXiao]

Hi all,

Greetings from me! I want to implement a simple matrix multiplication using Cingulata, and modify hello.cxx as following:

#include <iostream>
#include <fstream>
#include <vector>

/* local includes */
#include <integer.hxx>

/* namespaces */
using namespace std;

int main()
{
	vector<vector<Integer8>> a = {{1, 2}, {3, 4}};
	vector<vector<Integer8>> b = {{5, 6}, {7, 8}};
	vector<vector<Integer8>> c(2, vector<Integer8>(2));

	for (vector<vector<Integer8>>::size_type row = 0; row < a.size(); row++) {
		for (vector<Integer8>::size_type col = 0; col < b[row].size(); col++) {
			c[row][col] = 0;
			for (vector<Integer8>::size_type i = 0; i < a[row].size(); i++) {
				c[row][col] += a[row][i] * b[i][col];
			}
		}
	}

	for (vector<vector<Integer8>>::size_type row = 0; row < a.size(); row++) {
		for (vector<Integer8>::size_type col = 0; col < b[row].size(); col++) {
			cout << c[row][col];
		}
	}
	
	FINALIZE_CIRCUIT("hello.blif");
}

Compile it and generate following core dump:

[ 27%] Built target generator
Scanning dependencies of target hello-gen
[ 33%] Building CXX object tests/hello/CMakeFiles/hello-gen.dir/hello.cxx.o
[ 38%] Linking CXX executable hello-gen
[ 38%] Built target hello-gen
[ 83%] Built target abc
[ 88%] Generating hello.blif
false false false false true true true true false false false true false false false false false false true false true false true true false false true true false false true false [ 94%] Generating hello-opt.blif
abc: /home/xiaonan/Cingulata/build/optim/abc/src/abc/src/bool/bdc/bdcCore.c:73: Bdc_ManAlloc: Assertion `pPars->nVarsMax > 1 && pPars->nVarsMax < 16' failed.
../../optim/abc_optimize.bash: line 62: 126624 Aborted                 (core dumped) $ABC_PATH/abc -c "$1"
make[2]: *** [tests/hello/CMakeFiles/hello.dir/build.make:65: tests/hello/hello-opt.blif] Error 1
make[1]: *** [CMakeFiles/Makefile2:746: tests/hello/CMakeFiles/hello.dir/all] Error 2
make: *** [Makefile:84: all] Error 2

Use gdb to check the stack backtrace:

Program terminated with signal SIGABRT, Aborted.
#0  0x00007f978fb9b860 in raise () from /usr/lib/libc.so.6
(gdb) bt
#0  0x00007f978fb9b860 in raise () from /usr/lib/libc.so.6
#1  0x00007f978fb9cec9 in abort () from /usr/lib/libc.so.6
#2  0x00007f978fb940bc in __assert_fail_base () from /usr/lib/libc.so.6
#3  0x00007f978fb94133 in __assert_fail () from /usr/lib/libc.so.6
#4  0x000055eff23e420f in Bdc_ManAlloc ()
#5  0x000055eff1c4670f in Abc_NtkBidecResyn ()
#6  0x000055eff1be73b3 in Abc_CommandBidec ()
#7  0x000055eff1d8b4aa in CmdCommandDispatch ()
#8  0x000055eff1d8ba4f in CmdApplyAlias ()
#9  0x000055eff1d7b19f in Cmd_CommandExecute ()
#10 0x000055eff1dfdf99 in Abc_RealMain ()
#11 0x000055eff1df4af1 in main ()

Could you help to check this issue? Thanks very much in advance!

Update:
If I modify the code get matrix values from input, it works:

#include <iostream>
#include <fstream>
#include <vector>

/* local includes */
#include <integer.hxx>

/* namespaces */
using namespace std;

int main()
{
	vector<vector<Integer8>> a(2, vector<Integer8>(2));
	vector<vector<Integer8>> b(2, vector<Integer8>(2));
	vector<vector<Integer8>> c(2, vector<Integer8>(2));
	
	cin >> a[0][0];
	cin >> a[0][1];
	cin >> a[1][0];
	cin >> a[1][1];
	cin >> b[0][0];
	cin >> b[0][1];
	cin >> b[1][0];
	cin >> b[1][1];
	
	for (vector<vector<Integer8>>::size_type row = 0; row < a.size(); row++) {
		for (vector<Integer8>::size_type col = 0; col < b[row].size(); col++) {
			c[row][col] = 0;
			for (vector<Integer8>::size_type i = 0; i < a[row].size(); i++) {
				c[row][col] += a[row][i] * b[i][col];
			}
		}
	}

	for (vector<vector<Integer8>>::size_type row = 0; row < a.size(); row++) {
		for (vector<Integer8>::size_type col = 0; col < b[row].size(); col++) {
			cout << c[row][col];
		}
	}
	
	FINALIZE_CIRCUIT("hello.blif");
}

So could you explain the reason? Thanks!

Best Regards
Nan Xiao

[renaud-sirdey]

Dear Nan,

Thanks a lot for your feedback.

Indeed, the second version of the code above is the correct one.

This is so because encrypted-domain variables have to be read from the standard input in your Cingulata programs.

In the first version of your code, the matrix values are constant clear domain values and treated as such through the Integer8 type (which in such a case performs compile-time mixed clear domain/encrypted domain calculation simplifications in order to rightfully save non necessary FHE calculations).

This will result in an circuit with a constant output which does as such never need to be run in the encrypted domain (although the resulting core dump in ABC is far from graceful and should be fixed to get a more meaningful warning or error).

So in summary, if you do something like this :

Integer8 a=5,b=3;
cout<<a+b; 

All is created is a circuit which always output 8 and does never require any encrypted-domain calculations, whereas if you do something like,

Integer8 a,b;
cin>>a;
cin>>b;
cout<<a+b;

Then, you create a program which takes two encrypted values and output their (encrypted) sum.

As a further subtetly, a and/or b may be still be clear-domain variables but since they are read from the standard input their values will not induce any simplification or constant progagation in the resulting circuit (the “cardio” test case gives an example of handling mixed clear/crypto domain variables in Cingulata programs) – avoidable homomorphic operations will then be simplified as runtime.

Hope this helps clarifying,
Best regards, Renaud

[NanXiao]

Hi Renaud,

Got it! Thanks very much for your time and help!

Best Regards
Nan Xiao