Fix test expectations to succeed on big-endian architectures

tautschnig · tautschnig · commit 9ce5c3ad1ebf · 2023-07-24T08:53:30.000Z
Values checked for in some tests depend on endianness. Also, don't
hard-code "byte_(extract|update)_little_endian and instead also accept
the big-endian variant thereof.
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/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)

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`	`}`