Implement remaining missing operations in native ONNX parser #630

MatthewDaggitt · 2023-04-10T04:18:54Z

Also fixes a couple of bugs in the parser I found and adds a better error message for when the user forgets to provide a network file on the command line.

wu-haoze

Hi Matthew, thanks for this contribution.
The implementation looks correct to me. However, given the amount of details in the conv operation, is it possible to add some unit tests to the onnx parser?
One way might be to load a small convolutional network, set the input to constant, solve it and see if the output variable assignment matches the expectation.

Otherwise, the PR looks good to me.

Here are some unit tests that we have for the onnx parser implemented in the python API. I think those networks are small enough to be considered for the unit test.

Marabou/maraboupy/test/test_onnx.py

Lines 67 to 74 in 663835d

    
           def test_conv_mp1(): 
        
               """ 
        
               Test a convolutional network using max pool, exported from pytorch 
        
               Uses Conv, Relu, MaxPool, Constant, Reshape, Transpose, 
        
               Matmul, and Add layers 
        
               """ 
        
               filename =  "conv_mp1.onnx" 
        
               evaluateFile(filename, inputNames = ['X'], outputNames = ['Y'])

Marabou/maraboupy/test/test_onnx.py

Lines 50 to 57 in 663835d

    
           def test_KJ_TinyTaxiNet(): 
        
               """ 
        
               Test a convolutional network, exported from tensorflow 
        
               Uses Transpose, Conv, Add, Relu, Cast, Reshape, 
        
               Matmul, and Identity layers 
        
               """ 
        
               filename =  "KJ_TinyTaxiNet.onnx" 
        
               evaluateFile(filename)

wu-haoze · 2023-04-25T22:02:53Z

src/engine/Marabou.cpp

+            printf( "Error: no network file provided!\n" );
+            throw MarabouError( MarabouError::FILE_DOESNT_EXIST, networkFilePath.ascii() );
+        }
+
        if ( !File::exists( networkFilePath ) )


Change this line to "else if" then?

I'd prefer not to. I think early return points are much cleaner to read and require less mental effort. However, if you insist I can change it?

MatthewDaggitt · 2023-04-26T07:04:13Z

Thanks for the review!

However, given the amount of details in the conv operation, is it possible to add some unit tests to the onnx parser?

Yup sure! I'm trying to add your example networks now, but I'm having to implement some of the missing operators such as transpose as well.

MatthewDaggitt · 2023-05-08T11:50:11Z

Added the missing operation implementations. Will add the tests later this week.

MatthewDaggitt · 2023-05-12T08:45:54Z

@anwu1219 in the end I decided it would be far better to add some proper unit tests rather than simply pushing through large networks. I've therefore added a zoo of ONNX networks each consisting of a single node (+ some constants), one for each layer type that we support.

There are two layers for which I've run into problems:

A single constant layer runs into Minor bug in Python/C++ parsing of ONNX networks with constant outputs #637
A single sigmoid layer runs into a segfault in Marabou itself when trying to solve:

Running 1 testAddressSanitizer:DEADLYSIGNAL
=================================================================
==1511045==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x557671a36fd6 bp 0x7fff1c539f20 sp 0x7fff1c539ec0 T0)
==1511045==The signal is caused by a READ memory access.
==1511045==Hint: address points to the zero page.
    #0 0x557671a36fd6 in Tableau::storeState(TableauState&, TableauStateStorageLevel) const /home/matthew/Code/AISEC/Marabou/src/engine/Tableau.cpp:1632
    #1 0x5576718ff041 in Engine::storeState(EngineState&, TableauStateStorageLevel) const /home/matthew/Code/AISEC/Marabou/src/engine/Engine.cpp:1699
    #2 0x55767199a657 in PrecisionRestorer::storeInitialEngineState(IEngine const&) /home/matthew/Code/AISEC/Marabou/src/engine/PrecisionRestorer.cpp:27
    #3 0x5576718d8b45 in Engine::storeInitialEngineState() /home/matthew/Code/AISEC/Marabou/src/engine/Engine.cpp:2194
    #4 0x5576718fa592 in Engine::solve(unsigned int) /home/matthew/Code/AISEC/Marabou/src/engine/Engine.cpp:188
    #5 0x5576718cb017 in OnnxParserTestSuite::run_test(String, Vector<double>, Vector<double>) (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x54017)
    #6 0x5576718cce64 in OnnxParserTestSuite::test_sigmoid() (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x55e64)
    #7 0x5576718cd403 in TestDescription_OnnxParserTestSuite_test_sigmoid::runTest() (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x56403)
    #8 0x5576718b8fc8 in CxxTest::RealTestDescription::run() /home/matthew/Code/AISEC/Marabou/tools/cxxtest/cxxtest/RealDescriptions.cpp:96
    #9 0x5576718bfe7c in CxxTest::TestRunner::runSuite(CxxTest::SuiteDescription&) (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x48e7c)
    #10 0x5576718c048b in CxxTest::TestRunner::runWorld() (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x4948b)
    #11 0x5576718c0734 in CxxTest::TestRunner::runAllTests(CxxTest::TestListener&) (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x49734)
    #12 0x5576718ba161 in CxxTest::ErrorFormatter::run() /home/matthew/Code/AISEC/Marabou/tools/cxxtest/cxxtest/ErrorFormatter.h:47
    #13 0x5576718ba161 in main /home/matthew/Code/AISEC/Marabou/build/src/input_parsers/Test_OnnxParser.cc:16
    #14 0x7f5fcb029d8f in __libc_start_call_main ../sysdeps/nptl/libc_start_call_main.h:58
    #15 0x7f5fcb029e3f in __libc_start_main_impl ../csu/libc-start.c:392
    #16 0x5576718b6d74 in _start (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x3fd74)

Given the simplicity of the sigmoid parsing code, I don't really think it can be the fault of the ONNX parser as it's identical to that for the python ONNX parser sigmoid implementation.

Given that sigmoid was already implemented already, it not working doesn't make things any worse than they previously were. I therefore propose that we file an issue for that, and this PR is ready to merge in, subject to your final approval?

MatthewDaggitt · 2023-05-12T08:46:43Z

Oh I forgot to say that I updated the version of the C++ ONNX library we build against, so that we use the same version of ONNX for both the Python and the C++ backends 👍

MatthewDaggitt · 2023-05-13T04:46:42Z

Same non-deterministic test failure with the ipq format as always...

wu-haoze · 2023-05-16T05:00:40Z

Hi @MatthewDaggitt , thanks a lot for the added test! The PR LGTM!

wu-haoze · 2023-05-16T05:01:05Z

@anwu1219 in the end I decided it would be far better to add some proper unit tests rather than simply pushing through large networks. I've therefore added a zoo of ONNX networks each consisting of a single node (+ some constants), one for each layer type that we support.

There are two layers for which I've run into problems:

A single constant layer runs into Minor bug in Python/C++ parsing of ONNX networks with constant outputs #637
A single sigmoid layer runs into a segfault in Marabou itself when trying to solve:

Running 1 testAddressSanitizer:DEADLYSIGNAL
=================================================================
==1511045==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x557671a36fd6 bp 0x7fff1c539f20 sp 0x7fff1c539ec0 T0)
==1511045==The signal is caused by a READ memory access.
==1511045==Hint: address points to the zero page.
    #0 0x557671a36fd6 in Tableau::storeState(TableauState&, TableauStateStorageLevel) const /home/matthew/Code/AISEC/Marabou/src/engine/Tableau.cpp:1632
    #1 0x5576718ff041 in Engine::storeState(EngineState&, TableauStateStorageLevel) const /home/matthew/Code/AISEC/Marabou/src/engine/Engine.cpp:1699
    #2 0x55767199a657 in PrecisionRestorer::storeInitialEngineState(IEngine const&) /home/matthew/Code/AISEC/Marabou/src/engine/PrecisionRestorer.cpp:27
    #3 0x5576718d8b45 in Engine::storeInitialEngineState() /home/matthew/Code/AISEC/Marabou/src/engine/Engine.cpp:2194
    #4 0x5576718fa592 in Engine::solve(unsigned int) /home/matthew/Code/AISEC/Marabou/src/engine/Engine.cpp:188
    #5 0x5576718cb017 in OnnxParserTestSuite::run_test(String, Vector<double>, Vector<double>) (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x54017)
    #6 0x5576718cce64 in OnnxParserTestSuite::test_sigmoid() (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x55e64)
    #7 0x5576718cd403 in TestDescription_OnnxParserTestSuite_test_sigmoid::runTest() (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x56403)
    #8 0x5576718b8fc8 in CxxTest::RealTestDescription::run() /home/matthew/Code/AISEC/Marabou/tools/cxxtest/cxxtest/RealDescriptions.cpp:96
    #9 0x5576718bfe7c in CxxTest::TestRunner::runSuite(CxxTest::SuiteDescription&) (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x48e7c)
    #10 0x5576718c048b in CxxTest::TestRunner::runWorld() (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x4948b)
    #11 0x5576718c0734 in CxxTest::TestRunner::runAllTests(CxxTest::TestListener&) (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x49734)
    #12 0x5576718ba161 in CxxTest::ErrorFormatter::run() /home/matthew/Code/AISEC/Marabou/tools/cxxtest/cxxtest/ErrorFormatter.h:47
    #13 0x5576718ba161 in main /home/matthew/Code/AISEC/Marabou/build/src/input_parsers/Test_OnnxParser.cc:16
    #14 0x7f5fcb029d8f in __libc_start_call_main ../sysdeps/nptl/libc_start_call_main.h:58
    #15 0x7f5fcb029e3f in __libc_start_main_impl ../csu/libc-start.c:392
    #16 0x5576718b6d74 in _start (/home/matthew/Code/AISEC/Marabou/build/tests/parser/Test_OnnxParser+0x3fd74)

Given the simplicity of the sigmoid parsing code, I don't really think it can be the fault of the ONNX parser as it's identical to that for the python ONNX parser sigmoid implementation.

Given that sigmoid was already implemented already, it not working doesn't make things any worse than they previously were. I therefore propose that we file an issue for that, and this PR is ready to merge in, subject to your final approval?

Interesting.. Yes, please file an issue for this. Thank you!

MatthewDaggitt added 2 commits April 10, 2023 13:17

Implement MaxPool and Conv layers in native ONNX parser

437cb11

Fixed string compile error

50c7cd0

MatthewDaggitt requested a review from wu-haoze April 22, 2023 03:59

wu-haoze requested changes Apr 25, 2023

View reviewed changes

Merge branch 'master' into conv-support

df91f13

Add implementations for all missing operations except Cast

1c269e1

MatthewDaggitt changed the title ~~Implement MaxPool and Conv layers in native ONNX parser~~ Implement remaining missing operations in native ONNX parser May 8, 2023

MatthewDaggitt added 2 commits May 8, 2023 21:01

Fix stricter compile error

0a16cd5

Add unit tests for all supported ONNX layers

36090b3

MatthewDaggitt added 2 commits May 12, 2023 18:25

Remove rogue optimise pragma

025a320

Make test paths relative

2ae596d

wu-haoze approved these changes May 16, 2023

View reviewed changes

MatthewDaggitt merged commit fc0400c into NeuralNetworkVerification:master May 16, 2023

MatthewDaggitt mentioned this pull request May 16, 2023

Segfault when solving for network with single sigmoid layer #638

Closed

wenkokke mentioned this pull request Jun 20, 2023

Add infrastructure for packaging and distributing maraboupy #633

Merged

wu-haoze pushed a commit that referenced this pull request Mar 4, 2024

Implement remaining missing operations in native ONNX parser (#630)

588d1bd

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement remaining missing operations in native ONNX parser #630

Implement remaining missing operations in native ONNX parser #630

MatthewDaggitt commented Apr 10, 2023

wu-haoze left a comment

wu-haoze Apr 25, 2023

MatthewDaggitt Apr 26, 2023

MatthewDaggitt commented Apr 26, 2023

MatthewDaggitt commented May 8, 2023

MatthewDaggitt commented May 12, 2023

MatthewDaggitt commented May 12, 2023

MatthewDaggitt commented May 13, 2023 •

edited

Loading

wu-haoze commented May 16, 2023

wu-haoze commented May 16, 2023

	def test_conv_mp1():
	"""
	Test a convolutional network using max pool, exported from pytorch
	Uses Conv, Relu, MaxPool, Constant, Reshape, Transpose,
	Matmul, and Add layers
	"""
	filename = "conv_mp1.onnx"
	evaluateFile(filename, inputNames = ['X'], outputNames = ['Y'])

	def test_KJ_TinyTaxiNet():
	"""
	Test a convolutional network, exported from tensorflow
	Uses Transpose, Conv, Add, Relu, Cast, Reshape,
	Matmul, and Identity layers
	"""
	filename = "KJ_TinyTaxiNet.onnx"
	evaluateFile(filename)

Implement remaining missing operations in native ONNX parser #630

Implement remaining missing operations in native ONNX parser #630

Conversation

MatthewDaggitt commented Apr 10, 2023

wu-haoze left a comment

Choose a reason for hiding this comment

wu-haoze Apr 25, 2023

Choose a reason for hiding this comment

MatthewDaggitt Apr 26, 2023

Choose a reason for hiding this comment

MatthewDaggitt commented Apr 26, 2023

MatthewDaggitt commented May 8, 2023

MatthewDaggitt commented May 12, 2023

MatthewDaggitt commented May 12, 2023

MatthewDaggitt commented May 13, 2023 • edited Loading

wu-haoze commented May 16, 2023

wu-haoze commented May 16, 2023

MatthewDaggitt commented May 13, 2023 •

edited

Loading