diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index d55198e101c..ed71ad439ef 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -36,6 +36,7 @@ add_subdirectory(cbmc-incr-smt2) add_subdirectory(cbmc-incr) add_subdirectory(cbmc-with-incr) add_subdirectory(array-refinement-with-incr) +add_subdirectory(goto-instrument-json) add_subdirectory(goto-instrument-wmm-core) add_subdirectory(goto-instrument-typedef) add_subdirectory(smt2_solver) diff --git a/regression/Makefile b/regression/Makefile index 538c704199d..cac9d590b2f 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -14,6 +14,7 @@ DIRS = cbmc \ cbmc-incr \ cbmc-with-incr \ array-refinement-with-incr \ + goto-instrument-json \ goto-instrument-wmm-core \ goto-instrument-typedef \ smt2_solver \ diff --git a/regression/goto-instrument-json/CMakeLists.txt b/regression/goto-instrument-json/CMakeLists.txt new file mode 100644 index 00000000000..385d97d851f --- /dev/null +++ b/regression/goto-instrument-json/CMakeLists.txt @@ -0,0 +1,3 @@ +add_test_pl_tests( + "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $ $" +) diff --git a/regression/goto-instrument-json/Makefile b/regression/goto-instrument-json/Makefile new file mode 100644 index 00000000000..5ce76853266 --- /dev/null +++ b/regression/goto-instrument-json/Makefile @@ -0,0 +1,20 @@ +default: tests.log + +include ../../src/config.inc +include ../../src/common + +test: + @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/goto-instrument/goto-instrument' + +tests.log: + @../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/goto-instrument/goto-instrument' + +clean: + @for dir in *; do \ + $(RM) tests.log; \ + if [ -d "$$dir" ]; then \ + cd "$$dir"; \ + $(RM) *.out *.gb; \ + cd ..; \ + fi \ + done diff --git a/regression/goto-instrument-json/chain.sh b/regression/goto-instrument-json/chain.sh new file mode 100755 index 00000000000..44543abf1a6 --- /dev/null +++ b/regression/goto-instrument-json/chain.sh @@ -0,0 +1,13 @@ +#!/bin/bash + +set -e + +symtab2gb_exe=$1 +goto_instrument_exe=$2 + +name=${*:$#} + +args=${*:3:$#-3} + +$symtab2gb_exe "${name}" +$goto_instrument_exe "${args}" a.out diff --git a/regression/goto-instrument-json/rol_signed/test-signed.desc b/regression/goto-instrument-json/rol_signed/test-signed.desc new file mode 100644 index 00000000000..9102af322a7 --- /dev/null +++ b/regression/goto-instrument-json/rol_signed/test-signed.desc @@ -0,0 +1,14 @@ +CORE +test-signed.json +--dump-c +^EXIT=0$ +^SIGNAL=0$ +signed char rol8=\(unsigned char\)'8' << 3 % 8 \| \(unsigned char\)'8' >> 8 - 3 % 8; +-- +irep +-- +This tests that the rol goto operation is converted into suitable bit +twiddling operations in C representation. This is also checks that +signed rotations cast to unsigned to perform the shifts to avoid +sign bit problems. Also the negative check for "irep" checks that no +irep is failing conversion. diff --git a/regression/goto-instrument-json/rol_signed/test-signed.json b/regression/goto-instrument-json/rol_signed/test-signed.json new file mode 100644 index 00000000000..bbf814a17a4 --- /dev/null +++ b/regression/goto-instrument-json/rol_signed/test-signed.json @@ -0,0 +1,591 @@ +{ + "symbolTable": { + "VoidUnit": { + "baseName": "VoidUnit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "VoidUnit", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main": { + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main", + "prettyName": "main", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_0" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::rol8" + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "label": { + "id": "bb0" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "assign" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::rol8" + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + }, + { + "id": "rol", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "38" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "3" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "destination": { + "id": "bb1" + }, + "statement": { + "id": "goto" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "label": { + "id": "bb1" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "skip" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "statement": { + "id": "return" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "VoidUnit" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + } + ] + } + }, + "main::1::var_0": { + "baseName": "var_0", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_0", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main::1::var_1::rol8": { + "baseName": "rol8", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_1::rol8", + "prettyName": "", + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "nil" + } + }, + "tag-Unit": { + "baseName": "Unit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "tag-Unit", + "prettyName": "", + "type": { + "id": "struct", + "namedSub": { + "components": { + "id": "" + }, + "tag": { + "id": "Unit" + } + } + }, + "value": { + "id": "nil" + } + } + } +} diff --git a/regression/goto-instrument-json/rol_unsigned/test.desc b/regression/goto-instrument-json/rol_unsigned/test.desc new file mode 100644 index 00000000000..80d25caa0c1 --- /dev/null +++ b/regression/goto-instrument-json/rol_unsigned/test.desc @@ -0,0 +1,12 @@ +CORE +test.json +--dump-c +^EXIT=0$ +^SIGNAL=0$ +unsigned char rol8=56 << 3 % 8 \| 56 >> 8 - 3 % 8; +-- +irep +-- +This tests that the rol goto operation is converted into suitable bit +twiddling operations in C representation. Also the negative check for +"irep" checks that no irep is failing conversion. diff --git a/regression/goto-instrument-json/rol_unsigned/test.json b/regression/goto-instrument-json/rol_unsigned/test.json new file mode 100644 index 00000000000..d55269b3126 --- /dev/null +++ b/regression/goto-instrument-json/rol_unsigned/test.json @@ -0,0 +1,591 @@ +{ + "symbolTable": { + "VoidUnit": { + "baseName": "VoidUnit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "VoidUnit", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main": { + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main", + "prettyName": "main", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_0" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::rol8" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "label": { + "id": "bb0" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "assign" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::rol8" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + }, + { + "id": "rol", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "38" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "3" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "destination": { + "id": "bb1" + }, + "statement": { + "id": "goto" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "label": { + "id": "bb1" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "skip" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "statement": { + "id": "return" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "VoidUnit" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + } + ] + } + }, + "main::1::var_0": { + "baseName": "var_0", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_0", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main::1::var_1::rol8": { + "baseName": "rol8", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_1::rol8", + "prettyName": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "nil" + } + }, + "tag-Unit": { + "baseName": "Unit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "tag-Unit", + "prettyName": "", + "type": { + "id": "struct", + "namedSub": { + "components": { + "id": "" + }, + "tag": { + "id": "Unit" + } + } + }, + "value": { + "id": "nil" + } + } + } +} \ No newline at end of file diff --git a/regression/goto-instrument-json/ror_signed/test-signed.desc b/regression/goto-instrument-json/ror_signed/test-signed.desc new file mode 100644 index 00000000000..4d2517e484d --- /dev/null +++ b/regression/goto-instrument-json/ror_signed/test-signed.desc @@ -0,0 +1,14 @@ +CORE +test-signed.json +--dump-c +^EXIT=0$ +^SIGNAL=0$ +signed char ror8=\(unsigned char\)'8' >> 3 % 8 \| \(unsigned char\)'8' << 8 - 3 % 8; +-- +irep +-- +This tests that the ror goto operation is converted into suitable bit +twiddling operations in C representation. This is also checks that +signed rotations cast to unsigned to perform the shifts to avoid +sign bit problems. Also the negative check for "irep" checks that no +irep is failing conversion. diff --git a/regression/goto-instrument-json/ror_signed/test-signed.json b/regression/goto-instrument-json/ror_signed/test-signed.json new file mode 100644 index 00000000000..6e93735891b --- /dev/null +++ b/regression/goto-instrument-json/ror_signed/test-signed.json @@ -0,0 +1,591 @@ +{ + "symbolTable": { + "VoidUnit": { + "baseName": "VoidUnit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "VoidUnit", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main": { + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main", + "prettyName": "main", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_0" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::ror8" + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "label": { + "id": "bb0" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "assign" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::ror8" + }, + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + }, + { + "id": "ror", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "38" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "3" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "destination": { + "id": "bb1" + }, + "statement": { + "id": "goto" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "label": { + "id": "bb1" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "skip" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "statement": { + "id": "return" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "VoidUnit" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + } + ] + } + }, + "main::1::var_0": { + "baseName": "var_0", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_0", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main::1::var_1::ror8": { + "baseName": "ror8", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_1::ror8", + "prettyName": "", + "type": { + "id": "signedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "nil" + } + }, + "tag-Unit": { + "baseName": "Unit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "tag-Unit", + "prettyName": "", + "type": { + "id": "struct", + "namedSub": { + "components": { + "id": "" + }, + "tag": { + "id": "Unit" + } + } + }, + "value": { + "id": "nil" + } + } + } +} diff --git a/regression/goto-instrument-json/ror_unsigned/test.desc b/regression/goto-instrument-json/ror_unsigned/test.desc new file mode 100644 index 00000000000..a75a03ba50b --- /dev/null +++ b/regression/goto-instrument-json/ror_unsigned/test.desc @@ -0,0 +1,12 @@ +CORE +test.json +--dump-c +^EXIT=0$ +^SIGNAL=0$ +unsigned char ror8=56 >> 3 % 8 \| 56 << 8 - 3 % 8; +-- +irep +-- +This tests that the ror goto operation is converted into suitable bit +twiddling operations in C representation. Also the negative check for +"irep" checks that no irep is failing conversion. diff --git a/regression/goto-instrument-json/ror_unsigned/test.json b/regression/goto-instrument-json/ror_unsigned/test.json new file mode 100644 index 00000000000..5e8beda421c --- /dev/null +++ b/regression/goto-instrument-json/ror_unsigned/test.json @@ -0,0 +1,591 @@ +{ + "symbolTable": { + "VoidUnit": { + "baseName": "VoidUnit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "VoidUnit", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main": { + "baseName": "main", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main", + "prettyName": "main", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "1" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_0" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "decl" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::ror8" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "label": { + "id": "bb0" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "statement": { + "id": "block" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "assign" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "main::1::var_1::ror8" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + } + }, + { + "id": "ror", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "38" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "3" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "16" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "destination": { + "id": "bb1" + }, + "statement": { + "id": "goto" + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "label": { + "id": "bb1" + }, + "statement": { + "id": "label" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "statement": { + "id": "skip" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "statement": { + "id": "return" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "VoidUnit" + }, + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + } + } + } + ] + } + ] + } + }, + "main::1::var_0": { + "baseName": "var_0", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "11" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "6" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_0", + "prettyName": "", + "type": { + "id": "struct_tag", + "namedSub": { + "identifier": { + "id": "tag-Unit" + } + } + }, + "value": { + "id": "nil" + } + }, + "main::1::var_1::ror8": { + "baseName": "ror8", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "column": { + "id": "9" + }, + "file": { + "id": "/Users/vecchiot/Documents/rmc/src/test/cbmc/test.rs" + }, + "function": { + "id": "main" + }, + "line": { + "id": "7" + } + } + }, + "mode": "C", + "module": "", + "name": "main::1::var_1::ror8", + "prettyName": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "width": { + "id": "8" + } + } + }, + "value": { + "id": "nil" + } + }, + "tag-Unit": { + "baseName": "Unit", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "tag-Unit", + "prettyName": "", + "type": { + "id": "struct", + "namedSub": { + "components": { + "id": "" + }, + "tag": { + "id": "Unit" + } + } + }, + "value": { + "id": "nil" + } + } + } +} \ No newline at end of file diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 5384ff9f5d2..c3bb3403a04 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2290,6 +2290,66 @@ std::string expr2ct::convert_initializer_list(const exprt &src) return dest; } +std::string expr2ct::convert_rox(const shift_exprt &src, unsigned precedence) +{ + // AAAA rox n == (AAAA lhs_op n % width(AAAA)) + // | (AAAA rhs_op (width(AAAA) - n % width(AAAA))) + // Where lhs_op and rhs_op depend on whether it is rol or ror + // Get AAAA and if it's signed wrap it in a cast to remove + // the sign since this messes with C shifts + exprt op0 = src.op(); + size_t type_width; + if(can_cast_type(op0.type())) + { + // Set the type width + type_width = to_signedbv_type(op0.type()).get_width(); + // Shifts in C are arithmetic and care about sign, by forcing + // a cast to unsigned we force the shifts to perform rol/r + op0 = typecast_exprt(op0, unsignedbv_typet(type_width)); + } + else if(can_cast_type(op0.type())) + { + // Set the type width + type_width = to_unsignedbv_type(op0.type()).get_width(); + } + else + { + UNREACHABLE; + } + // Construct the "width(AAAA)" constant + const exprt width_expr = from_integer(type_width, src.distance().type()); + // Apply modulo to n since shifting will overflow + // That is: 0001 << 4 == 0, but 0001 rol 4 == 0001 + const exprt distance_modulo_width = mod_exprt(src.distance(), width_expr); + // Now put the pieces together + // width(AAAA) - (n % width(AAAA)) + const auto complement_width_expr = + minus_exprt(width_expr, distance_modulo_width); + // lhs and rhs components defined according to rol/ror + exprt lhs_expr; + exprt rhs_expr; + if(src.id() == ID_rol) + { + // AAAA << (n % width(AAAA)) + lhs_expr = shl_exprt(op0, distance_modulo_width); + // AAAA >> complement_width_expr + rhs_expr = ashr_exprt(op0, complement_width_expr); + } + else if(src.id() == ID_ror) + { + // AAAA >> (n % width(AAAA)) + lhs_expr = ashr_exprt(op0, distance_modulo_width); + // AAAA << complement_width_expr + rhs_expr = shl_exprt(op0, complement_width_expr); + } + else + { + // Someone called this function when they shouldn't have. + UNREACHABLE; + } + return convert_with_precedence(bitor_exprt(lhs_expr, rhs_expr), precedence); +} + std::string expr2ct::convert_designated_initializer(const exprt &src) { if(src.operands().size()!=1) @@ -3794,6 +3854,9 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_type) return convert(src.type()); + else if(src.id() == ID_rol || src.id() == ID_ror) + return convert_rox(to_shift_expr(src), precedence); + auto function_string_opt = convert_function(src); if(function_string_opt.has_value()) return *function_string_opt; diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 50c4dd5210a..fcc98022150 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -126,6 +126,15 @@ class expr2ct const std::string &symbol2, unsigned precedence); + /// Conversion function from rol/ror expressions to C code strings + /// Note that this constructs a complex expression to do bit + /// twiddling since rol/ror operations are not native to ANSI-C. + /// The complex expression is then recursively converted. + /// \param src: is an exprt that must be either an rol or ror + /// \param precedence: precedence for bracketing + /// \returns string for performing rol/ror as bit twiddling with C + std::string convert_rox(const shift_exprt &src, unsigned precedence); + std::string convert_overflow( const exprt &src, unsigned &precedence); diff --git a/unit/Makefile b/unit/Makefile index 4e730e7dc5f..bb4a334b18e 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -36,6 +36,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \ analyses/variable-sensitivity/value_set_abstract_object/widening_merge.cpp \ analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \ + ansi-c/expr2c.cpp \ ansi-c/max_malloc_size.cpp \ ansi-c/type2name.cpp \ big-int/big-int.cpp \ diff --git a/unit/ansi-c/expr2c.cpp b/unit/ansi-c/expr2c.cpp new file mode 100644 index 00000000000..cfbed21dcb4 --- /dev/null +++ b/unit/ansi-c/expr2c.cpp @@ -0,0 +1,68 @@ +/*******************************************************************\ + +Module: Unit test for expr2c + +Author: Diffblue + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include +#include + +TEST_CASE("rol_2_c_conversion_unsigned", "[core][ansi-c][expr2c]") +{ + auto lhs = from_integer(31, unsignedbv_typet(32)); + auto rhs = from_integer(3, unsignedbv_typet(32)); + auto rol = shift_exprt(lhs, ID_rol, rhs); + CHECK( + expr2c(rol, namespacet{symbol_tablet{}}) == + "31 << 3 % 32 | 31 >> 32 - 3 % 32"); +} + +TEST_CASE("rol_2_c_conversion_signed", "[core][ansi-c][expr2c]") +{ + // The config lines are necessary since when we do casting from signed + // to unsigned in the rol/ror bit twiddling we need to output a + // suitable cast type (e.g. "unsigned int" and not + // "unsigned __CPROVER_bitvector"). + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_i386(); + auto lhs = from_integer(31, signedbv_typet(8)); + auto rhs = from_integer(3, signedbv_typet(8)); + auto rol = shift_exprt(lhs, ID_rol, rhs); + CHECK( + expr2c(rol, namespacet{symbol_tablet{}}) == + "(unsigned char)31 << 3 % 8 | (unsigned char)31 >> 8 - 3 % 8"); +} + +TEST_CASE("ror_2_c_conversion_unsigned", "[core][ansi-c][expr2c]") +{ + auto lhs = from_integer(31, unsignedbv_typet(32)); + auto rhs = from_integer(3, unsignedbv_typet(32)); + auto ror = shift_exprt(lhs, ID_ror, rhs); + CHECK( + expr2c(ror, namespacet{symbol_tablet{}}) == + "31 >> 3 % 32 | 31 << 32 - 3 % 32"); +} + +TEST_CASE("ror_2_c_conversion_signed", "[core][ansi-c][expr2c]") +{ + // The config lines are necessary since when we do casting from signed + // to unsigned in the rol/ror bit twiddling we need to output a + // suitable cast type (e.g. "unsigned int" and not + // "unsigned __CPROVER_bitvector"). + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_i386(); + auto lhs = from_integer(31, integer_bitvector_typet(ID_signedbv, 32)); + auto rhs = from_integer(3, integer_bitvector_typet(ID_signedbv, 32)); + auto ror = shift_exprt(lhs, ID_ror, rhs); + CHECK( + expr2c(ror, namespacet{symbol_tablet{}}) == + "(unsigned int)31 >> 3 % 32 | (unsigned int)31 << 32 - 3 % 32"); +} diff --git a/unit/ansi-c/module_dependencies.txt b/unit/ansi-c/module_dependencies.txt index 2a77c3a0403..c090b3f7751 100644 --- a/unit/ansi-c/module_dependencies.txt +++ b/unit/ansi-c/module_dependencies.txt @@ -1,2 +1,3 @@ testing-utils ansi-c +util