project-everest / everparse

Automated generation of provably secure, zero-copy parsers from format specifications
https://project-everest.github.io/everparse
Apache License 2.0
251 stars 15 forks source link

Generate test checker executable #106

Closed tahina-pro closed 12 months ago

tahina-pro commented 1 year ago

This PR introduces 3D option --test_checker, which, when followed by a parser name of the form Modulename.parsername, generates a test executable, test.exe, so that ./test.exe filename.dat arg1 arg2... opens the file filename.dat and runs the validator for Modulename.parsername, with arguments arg1, arg2..., on the binary data contained in that file, and returns 0 if the data in the file passes validation, 1 if it fails validation, 2 for any other error (wrong number of arguments, file is missing, cannot mmap, etc.)

The file passed to test.exe is assumed to contain all of the input data to be passed to the validator, in binary form. If the user wants to start from some filename.hex that contains hex data instead (e.g. .pcap), it is the responsibility of the user to first run something like xxd -r -p filename.hex filename.dat to convert that hex file to a binary file before passing the latter to test.exe

This should fix #105

nikswamy commented 1 year ago

Thanks for adding the error handler!

tahina-pro commented 1 year ago

The generated test checker now rejects test files that contain data beyond a valid object: in other words, if the validator succeeds but does not read all input, then the test checker now considers the test failing, and returns status code 1. Validator failure returns status code 2, and 3 for any other kind of errors.

tahina-pro commented 1 year ago

The --z3_test and --z3_diff_test modes now output each test case generated by Z3 into a raw binary file, whose name is of the form witness.nnn.POS.validatorname.arg1.arg2.dat and witness.nnn.NEG.validatorname.arg1.arg2.dat for positive and negative test cases generated by --z3_test , and witness.nnn.POS.validatorname1.NEG.validatorname2.arg1.arg2.arg3.dat for differential test cases generated by --z3_diff_test. Those are raw binary files, so it is the responsibility of the user to run xxd -p on those files to convert them to hexadecimal format.

lemmy commented 12 months ago

There seems to be a off-by-one of some sorts s.t. the first negative witness is actually a positive one.

@lemmy ➜ /workspaces/RFC-3D/foo2 (mku-tshark) $ for f in witness*; do echo $f && hexdump $f; done
witness.0.POS.VxlanValidateVxlanHeader.dat
0000000 0808 0808 0808                         
0000006
witness.1.POS.VxlanValidateVxlanHeader.dat
0000000 0f0f 0f00 0f0f                         
0000006
witness.2.POS.VxlanValidateVxlanHeader.dat
0000000 0018 0000 0000                         
0000006
witness.3.NEG.VxlanValidateVxlanHeader.dat <- payload same as 0.Pos
0000000 0808 0808 0808                         
0000006
witness.4.NEG.VxlanValidateVxlanHeader.dat
0000000 0000                                   
0000001
witness.5.NEG.VxlanValidateVxlanHeader.dat
0000000 0001                                   
0000001