Merge pull request #7811 from tautschnig/bugfixes/big-endian

tautschnig · web-flow · commit cdea666b9f17 · 2023-07-24T21:39:55.000+02:00
Fix big endian compatibility
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.c
@@ -9,7 +9,7 @@ int main()
   x[2] = 0;
   uint8_t *c = x;
   c[1] = 1;
-  assert(x[0] == 256);
+  assert(x[0] == 256 || x[0] == 1);
   assert(x[0] == 0);
   assert(x[1] == 0);
   assert(x[2] == 0);
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc
@@ -1,7 +1,7 @@
 CORE
 array-misalign-between.c
 
-\[main\.assertion\.1\] line \d+ assertion x\[0\] == 256: SUCCESS
+\[main\.assertion\.1\] line \d+ assertion x\[0\] == 256 \|\| x\[0\] == 1: SUCCESS
 \[main\.assertion\.2\] line \d+ assertion x\[0\] == 0: FAILURE
 \[main\.assertion\.3\] line \d+ assertion x\[1\] == 0: SUCCESS
 \[main\.assertion\.4\] line \d+ assertion x\[2\] == 0: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.c
@@ -9,7 +9,7 @@ int main()
   x[2] = 0;
   uint8_t *c = x;
   c[1] = 1;
-  assert(x[0] == 256ul);
+  assert(x[0] == 256ul || x[0] == 1ul);
   assert(x[0] == 0ul);
   assert(x[1] == 0ul);
   assert(x[2] == 0ul);
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc
@@ -1,7 +1,7 @@
 CORE
 array-misalign.c
 
-\[main.assertion\.1\] line \d+ assertion x\[0\] == 256ul: SUCCESS
+\[main.assertion\.1\] line \d+ assertion x\[0\] == 256ul \|\| x\[0\] == 1ul: SUCCESS
 \[main.assertion\.2\] line \d+ assertion x\[0\] == 0ul: FAILURE
 \[main.assertion\.3\] line \d+ assertion x\[1\] == 0ul: SUCCESS
 \[main.assertion\.4\] line \d+ assertion x\[2\] == 0ul: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.c
@@ -8,6 +8,6 @@ int main()
   x[1] = 0;
   uint16_t *y = x;
   *y = 258;
-  assert(x[0] == 2);
-  assert(x[1] == 1);
+  assert(x[0] == 2 || x[1] == 2);
+  assert(x[1] == 1 || x[0] == 1);
 }
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc
@@ -1,8 +1,8 @@
 CORE
 byte-update-small.c
 
-\[main\.assertion\.1\] line \d+ assertion x\[0\] == 2: SUCCESS
-\[main\.assertion\.2\] line \d+ assertion x\[1\] == 1: SUCCESS
+\[main\.assertion\.1\] line \d+ assertion x\[0\] == 2 \|\| x\[1\] == 2: SUCCESS
+\[main\.assertion\.2\] line \d+ assertion x\[1\] == 1 \|\| x\[0\] == 1: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.c
@@ -6,5 +6,5 @@ int main()
   uint16_t x = 0;
   uint8_t *y = &x;
   y[1] = 1;
-  assert(x == 256);
+  assert(x == 256 || x == 1);
 }
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc
@@ -1,7 +1,7 @@
 CORE
 byte-update.c
 
-\[main\.assertion\.1\] line \d+ assertion x == 256: SUCCESS
+\[main\.assertion\.1\] line \d+ assertion x == 256 \|\| x == 1: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_extract.desc b/regression/cbmc-incr-smt2/pointers-conversions/byte_extract.desc
@@ -5,8 +5,8 @@ Running incremental SMT2 solving via
 Building error trace
 \[main\.assertion\.\d+\] line \d+ assertion \*ptr != 42: FAILURE
 \[main\.assertion\.\d+\] line \d+ assertion input != original: SUCCESS
-  input=42ul? \(00000000 00000000 00000000 00101010\)
-  original=42ul? \(00000000 00000000 00000000 00101010\)
+  input=(42|704643072)ul? \((00000000|00101010) 00000000 00000000 (00101010|00000000)\)
+  original=(42|704643072)ul? \((00000000|00101010) 00000000 00000000 (00101010|00000000)\)
 Violated property:
   file byte_extract.c function main line \d+ thread \d+
   assertion \*ptr != 42
diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc b/regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc
@@ -5,12 +5,12 @@ Running incremental SMT2 solving via
 Building error trace
 \[main\.assertion\.\d+\] line \d+ assertion x != 256u: FAILURE
 State \d+ file byte_update\.c function main line \d+ thread \d
-  offset=1ul? \(00000000 00000000 00000000 00000001\)
+  offset=(1|2)ul? \(00000000 00000000 00000000 000000(01|10)\)
 Assumption:
   file byte_update\.c line \d+ function main
   offset >= 0u && offset < 4u
 State \d+ file byte_update\.c function main line \d+ thread \d+
-  byte_extract_little_endian\(x, \(.*\)offset, uint8_t\)=1 \(00000001\)
+  byte_extract_(little|big)_endian\(x, \(.*\)offset, uint8_t\)=1 \(00000001\)
 Violated property:
   file byte_update.c function main line \d+ thread \d+
   assertion x != 256u
diff --git a/regression/cbmc/Array_Pointer7/main.c b/regression/cbmc/Array_Pointer7/main.c
@@ -7,8 +7,12 @@ void f1()
   for(unsigned i = 0; i < sizeof(array1); i++)
     *(p + i) = i;
 
-  assert(array1[0] == 0x03020100);
-  assert(array1[1] == 0x07060504);
+  assert(
+    array1[0] == 0x03020100 /* little endian */ ||
+    array1[0] == 0x00010203 /* big endian */);
+  assert(
+    array1[1] == 0x07060504 /* little endian */ ||
+    array1[1] == 0x04050607 /* big endian */);
 }
 
 void f2()
@@ -20,7 +24,9 @@ void f2()
   array2[1] = 0x0200;
   p[4] = 1;
 
-  assert(array2[1] == 0x0201);
+  assert(
+    array2[1] == 0x0201 /* little endian */ ||
+    array2[1] == 0x01000200 /* big endian */);
 }
 
 int main()
diff --git a/regression/cbmc/Pointer_array7/big-endian.desc b/regression/cbmc/Pointer_array7/big-endian.desc
@@ -1,6 +1,6 @@
 CORE new-smt-backend
 main.c
---big-endian -D__BIG_ENDIAN__
+--big-endian -DUSE_BIG_ENDIAN
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Pointer_array7/main.c b/regression/cbmc/Pointer_array7/main.c
@@ -1,13 +1,13 @@
 #include <assert.h>
 #include <stdint.h>
 
-#if !defined(__LITTLE_ENDIAN__) && !defined(__BIG_ENDIAN__)
+#if !defined(USE_LITTLE_ENDIAN) && !defined(USE_BIG_ENDIAN)
 
 #  if defined(__avr32__) || defined(__hppa__) || defined(__m68k__) ||          \
     defined(__mips__) || defined(__powerpc__) || defined(__s390__) ||          \
     defined(__s390x__) || defined(__sparc__)
 
-#    define __BIG_ENDIAN__
+#    define USE_BIG_ENDIAN
 
 #  endif
 
@@ -21,7 +21,7 @@ int main()
   uint8_t *y = (uint8_t *)x;
   uint16_t z = *((uint16_t *)(y + 1));
 
-#ifdef __BIG_ENDIAN__
+#ifdef USE_BIG_ENDIAN
   assert(z == 256u);
 #else
   assert(z == 512u);
diff --git a/regression/cbmc/Pointer_array7/test.desc b/regression/cbmc/Pointer_array7/test.desc
@@ -1,6 +1,6 @@
 CORE new-smt-backend
 main.c
---little-endian -D__LITTLE_ENDIAN__
+--little-endian -DUSE_LITTLE_ENDIAN
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc/Struct_Bytewise1/struct_bytewise.c b/regression/cbmc/Struct_Bytewise1/struct_bytewise.c
@@ -1,18 +1,3 @@
-// Determine endianness.
-// Follows http://wiki.debian.org/ArchitectureSpecificsMemo
-
-#if !defined(__LITTLE_ENDIAN__) && !defined(__BIG_ENDIAN__)
-
-#if defined(__avr32__) || defined(__hppa__)    || defined(__m68k__) || \
-    defined(__mips__)  || defined(__powerpc__) || defined(__s390__) || \
-    defined(__s390x__) || defined(__sparc__)
-
-#define __BIG_ENDIAN__
-
-#endif
-
-#endif
-
 typedef struct my_struct
 {
   // We hope these are 32 bit each on all architectures,
@@ -37,7 +22,7 @@ int main()
   logAppl.b=0x01000002;
   CopyBuffer((unsigned char *)&logAppl);
 
-  #ifdef __BIG_ENDIAN__
+#if defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__
   assert(arrayTmp[0]==0);
   assert(arrayTmp[1]==0);
   assert(arrayTmp[2]==0);
diff --git a/regression/cbmc/__builtin_clz-01/big-endian.desc b/regression/cbmc/__builtin_clz-01/big-endian.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--bounds-check --big-endian
+^\[main.bit_count.\d+\] line 61 count leading zeros is undefined for value zero in __builtin_clz\(0u\): FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/__builtin_ctz-01/big-endian.desc b/regression/cbmc/__builtin_ctz-01/big-endian.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--bounds-check --big-endian
+^\[main.bit_count.\d+\] line 46 count trailing zeros is undefined for value zero in __builtin_ctz\(0u\): FAILURE$
+^\[main.assertion.2\] line 47 count trailing zeros of 0 is bit width: SUCCESS$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/__builtin_ffs-01/big-endian.desc b/regression/cbmc/__builtin_ffs-01/big-endian.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --big-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/array-cell-sensitivity8/test.desc b/regression/cbmc/array-cell-sensitivity8/test.desc
@@ -10,7 +10,7 @@ main::1::array!0@1#2\[\[6\]\] =
 main::1::array!0@1#2\[\[7\]\] =
 main::1::array!0@1#2\[\[8\]\] =
 main::1::array!0@1#2\[\[9\]\] =
-main::1::array!0@1#3 =.*byte_extract_little_endian
+main::1::array!0@1#3 =.*byte_extract_(big|little)_endian
 main::1::array!0@1#3\[\[0\]\] =
 main::1::array!0@1#3\[\[1\]\] =
 main::1::array!0@1#3\[\[2\]\] =
diff --git a/regression/cbmc/byte-op-metric/test.desc b/regression/cbmc/byte-op-metric/test.desc
@@ -5,11 +5,11 @@ main.c
 ^SIGNAL=0$
 ^Byte Extracts:$
 ^.*main\.c line 8 function main$
-^.* byte\_extract\_little\_endian\(.*\)$
+^.* byte\_extract\_(big|little)\_endian\(.*\)$
 ^Number of byte extracts: 1$
 ^Byte Updates:$
 ^.*main\.c line 8 function main$
-^.* byte\_update\_little\_endian\(.*\)$
+^.* byte\_update\_(big|little)\_endian\(.*\)$
 ^Number of byte updates: 1$
 --
 --
diff --git a/regression/cbmc/byte-op-metric/test_json.desc b/regression/cbmc/byte-op-metric/test_json.desc
@@ -4,7 +4,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-"byteOpsStats": \{\n\s*"byteExtractStats": \{\n\s*"byteExtractList": \[\n\s*\{\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"ssaExpr": \{(\n.*)*\},\n\s*"ssaExprString": ".* .* byte\_extract\_little\_endian\(.*\)"\n\s*\}\n\s*\],\n\s*"numOfExtracts": 1\n\s*\},\n\s*"byteUpdateStats": \{\n\s*"byteUpdateList": \[\n\s*\{\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"ssaExpr": \{(\n.*)*\},\n\s*"ssaExprString": ".* .* byte\_update\_little\_endian\(.*\)"\n\s*\}\n\s*\],\n\s*"numOfUpdates": 1\n\s*\}
+"byteOpsStats": \{\n\s*"byteExtractStats": \{\n\s*"byteExtractList": \[\n\s*\{\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"ssaExpr": \{(\n.*)*\},\n\s*"ssaExprString": ".* .* byte\_extract\_(big|little)\_endian\(.*\)"\n\s*\}\n\s*\],\n\s*"numOfExtracts": 1\n\s*\},\n\s*"byteUpdateStats": \{\n\s*"byteUpdateList": \[\n\s*\{\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"ssaExpr": \{(\n.*)*\},\n\s*"ssaExprString": ".* .* byte\_update\_(big|little)\_endian\(.*\)"\n\s*\}\n\s*\],\n\s*"numOfUpdates": 1\n\s*\}
 --
 --
 To test json output for --show-byte-ops option that displays byte extract and update metrics.
diff --git a/regression/cbmc/byte_update12/main.c b/regression/cbmc/byte_update12/main.c
@@ -15,6 +15,9 @@ int main()
   struct S s;
   s.j = 1;
   memcpy(&s, A, x);
-  __CPROVER_assert((s.i & 0xFF) == 42, "lowest byte is 42");
+  __CPROVER_assert(
+    (s.i & 0xFF) == 42 /* little endian */ ||
+      (s.i >> ((sizeof(int) - 1) * 8)) == 42 /* big endian */,
+    "lowest byte is 42");
   __CPROVER_assert(s.j == 1, "s.j is unaffected by upate");
 }
diff --git a/regression/cbmc/float-nan-check/test.desc b/regression/cbmc/float-nan-check/test.desc
@@ -1,16 +1,16 @@
 CORE
 main.c
 --nan-check
-\[main.NaN.1\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
+\[main.NaN.1\] line \d+ NaN on \+ in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
 \[main.NaN.2\] line \d+ NaN on / in myzero / myzero: FAILURE
 \[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE
 \[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE
 \[main.NaN.5\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE
 \[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE
 \[main.NaN.7\] line \d+ NaN on - in myinf - myinf: FAILURE
 \[main.NaN.8\] line \d+ NaN on - in -myinf - -myinf: FAILURE
-\[main.NaN.9\] line \d+ NaN on \+ in byte_extract_little_endian\(c, (0|0l|0ll), float\) \+ byte_extract_little_endian\(c, (0|0l|0ll), float\): SUCCESS
-\[main.NaN.10\] line \d+ NaN on / in byte_extract_little_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
+\[main.NaN.9\] line \d+ NaN on \+ in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) \+ byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\): SUCCESS
+\[main.NaN.10\] line \d+ NaN on / in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) / myzero: SUCCESS
 \[main.NaN.11\] line \d+ NaN on \* in mynan \* mynan: SUCCESS
 \[main.NaN.12\] line \d+ NaN on \+ in mynan \+ mynan: SUCCESS
 \[main.NaN.13\] line \d+ NaN on - in mynan - mynan: SUCCESS
diff --git a/regression/cbmc/points-to-sets/test_json.desc b/regression/cbmc/points-to-sets/test_json.desc
@@ -4,7 +4,7 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_little_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\}
+\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_(big|little)_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\},\n\s*\{\n\s*"Pointer": "main::1::p!0@1",\n\s*"PointsToSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"PointsToSetSize": 1,\n\s*"RetainedValuesSet": \[ "object_descriptor\(integer_address, unknown\)" \],\n\s*"RetainedValuesSetSize": 1,\n\s*"Value": "byte_extract_(big|little)_endian\(__CPROVER_memory, pointer_offset\(main::1::p!0@1\), signedbv\[32\]\)"\n\s*\}
 --
 --
 To test output for --show-points-to-sets option that displays the size and contents of points-to sets in json format.
diff --git a/regression/cbmc/union15/main.c b/regression/cbmc/union15/main.c
@@ -50,13 +50,13 @@ int main()
   // following examples demonstrate.
   union B ub = {.c = 0xFF};
   ub.b = 0;
-  assert(ub.c == 0xFE);
+  assert(ub.c == 0xFE || ub.c == 0x7F);
 
   union C uc = {.i = 0xFFFFFFFF};
   uc.c = 0;
-  assert(uc.i == 0xFFFFFF00);
+  assert(uc.i == 0xFFFFFF00 || uc.i == 0x00FFFFFF);
 
   union A ua = {.i = 0xFFFFFFFF};
   ua.c = 0;
-  assert(ua.i == 0xFFFFFF00);
+  assert(ua.i == 0xFFFFFF00 || ua.i == 0x00FFFFFF);
 }
diff --git a/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c
@@ -4,7 +4,14 @@ typedef int (*fptr_t)(long long);
 
 void use_f(fptr_t fptr)
 {
+#if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   assert(fptr(10) == 11);
+#else
+  if(sizeof(int) == sizeof(long long))
+    assert(fptr(10) == 11);
+  else
+    assert(fptr(10) == 1);
+#endif
 }
 
 int f(int x)
diff --git a/src/goto-programs/elf_reader.cpp b/src/goto-programs/elf_reader.cpp
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp

Original file line number	Diff line number	Diff line change
`@@ -8,6 +8,6 @@ int main()`
`8`	`8`	`x[1] = 0;`
`9`	`9`	`uint16_t *y = x;`
`10`	`10`	`*y = 258;`
`11`		`- assert(x[0] == 2);`
`12`		`- assert(x[1] == 1);`
	`11`	`+ assert(x[0] == 2 \|\| x[1] == 2);`
	`12`	`+ assert(x[1] == 1 \|\| x[0] == 1);`
`13`	`13`	`}`
Original file line number	Diff line number	Diff line change
`@@ -6,5 +6,5 @@ int main()`
`6`	`6`	`uint16_t x = 0;`
`7`	`7`	`uint8_t *y = &x;`
`8`	`8`	`y[1] = 1;`
`9`		`- assert(x == 256);`
	`9`	`+ assert(x == 256 \|\| x == 1);`
`10`	`10`	`}`