Bug 1371894 - [cbmc] tests fail on big endian arches
Summary: [cbmc] tests fail on big endian arches
Status: CLOSED ERRATA
Alias: None
Product: Fedora
Classification: Fedora
Component: cbmc
Version: rawhide
Hardware: Unspecified
OS: Unspecified
unspecified
unspecified
Target Milestone: ---
Assignee: Jerry James
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Keywords:
Depends On:
Blocks: ZedoraTracker PPCTracker
TreeView+ depends on / blocked
 
Reported: 2016-08-31 11:46 UTC by Dan Horák
Modified: 2016-09-27 03:53 UTC (History)
3 users (show)

(edit)
Clone Of:
(edit)
Last Closed: 2016-09-22 07:33:40 UTC


Attachments (Terms of Use)

Description Dan Horák 2016-08-31 11:46:24 UTC
After update to version 5.5 some tests started to fail on big endian arches (ppc64, s390x)

from build.log
...
Tests failed
  2 of 383 tests failed, 19 tests skipped
Failed test: Pointer_array5
CBMC version 5.5 64-bit s390x linux
Parsing main.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (s390x)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 95 steps
simple slicing removed 24 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
12568 variables, 25409 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.042s
** Results:
[main.assertion.1] assertion address==&a0: FAILURE
** 1 of 1 failed (1 iteration)
VERIFICATION FAILED
EXIT=10
SIGNAL=0
Failed test: Pointer_byte_extract5
CBMC version 5.5 64-bit s390x linux
Parsing main.c
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (s390x)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 73 steps
simple slicing removed 5 assignments
Generated 9 VCC(s), 9 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
302 variables, 54 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
302 variables, 1 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
302 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.003s
** Results:
[main.array_bounds.1] array.List upper bound in p->List[0]: SUCCESS
[main.array_bounds.2] array.List upper bound in p->List[0]: SUCCESS
[main.assertion.1] p->List[0].b==555: SUCCESS
[main.assertion.2] p->List[0].a==555: SUCCESS
[main.array_bounds.3] array.List upper bound in p->List[1]: SUCCESS
[main.array_bounds.4] array.List upper bound in p->List[1]: SUCCESS
[main.assertion.3] p->List[1].b==999: FAILURE
[main.assertion.4] p->List[1].a==999: FAILURE
[main.array_bounds.5] array.List upper bound in p->List[2]: FAILURE
** 3 of 9 failed (3 iterations)
VERIFICATION FAILED
EXIT=10
SIGNAL=0
Makefile:4: recipe for target 'test' failed
make[1]: Leaving directory '/builddir/build/BUILD/cbmc-src/regression/cbmc'
make[1]: *** [test] Error 1
Makefile:4: recipe for target 'test' failed
make: Leaving directory '/builddir/build/BUILD/cbmc-src/regression'
make: *** [test] Error 1
..

for full logs please see http://s390.koji.fedoraproject.org/koji/taskinfo?taskID=2332684 or http://ppc.koji.fedoraproject.org/koji/taskinfo?taskID=3658891

Version-Release number of selected component (if applicable):
cbmc-5.5-1.fc26

Comment 1 Jerry James 2016-08-31 15:04:28 UTC
I don't have access to any big endian machines.  I've had guest accounts on various people's machines in the past.  I ran through all of them this morning, and all of the machines are either inaccessible or don't recognize my former username + password.  If somebody can provide me with an account on some big endian hardware somewhere, I am quite happy to debug this issue.  Anybody?  Anbody?  Bueller?

Just eyeballing the two failing tests, my guess is that the Pointer_array5 failure might go away if -fno-strict-aliasing is used.  The Pointer_byte_extract5 failure is more puzzling.  The first failing assertion happens like this:

  p->List[1].b = 999;

  __CPROVER_assert(p->List[1].b==999, "p->List[1].b==999");

We set that value to 999, then assert that the value is 999, and it isn't.  But the array index is higher than the array size declared by the packed type.  So I'm going to go out on a limb and conjecture that using a flexible array in the type declaration will fix this one; i.e., patching the code so the #ifdef __GNUC__ case reads:

typedef struct
{
  int Count;
  Union List[];
} __attribute__((packed)) Struct3;

If nobody is able to give me an account somewhere, could one of you with access to hardware please add this to %prep and try building again?

# Fix a test with type aliasing
sed -i '/main\.c/a-fno-strict-aliasing' regression/cbmc/Pointer_array5/test.desc

# Fix a test with out-of-bounds access to a packed array
sed -i '/__GNUC__/,/else/s/List\[1\]/List[]/' regression/cbmc/Pointer_byte_extract5/main.c

Comment 2 Ngo Than 2016-09-05 12:23:10 UTC
(In reply to Jerry James from comment #1)
> I don't have access to any big endian machines.  I've had guest accounts on
> various people's machines in the past.  I ran through all of them this
> morning, and all of the machines are either inaccessible or don't recognize
> my former username + password.  If somebody can provide me with an account
> on some big endian hardware somewhere, I am quite happy to debug this issue.
> Anybody?  Anbody?  Bueller?
> 

please take a look at following link to get access to th s390x machine
http://www-03.ibm.com/systems/z/os/linux/support/community.html

> Just eyeballing the two failing tests, my guess is that the Pointer_array5
> failure might go away if -fno-strict-aliasing is used.  The
> Pointer_byte_extract5 failure is more puzzling.  The first failing assertion
> happens like this:
> 
>   p->List[1].b = 999;
> 
>   __CPROVER_assert(p->List[1].b==999, "p->List[1].b==999");
> 
> We set that value to 999, then assert that the value is 999, and it isn't. 
> But the array index is higher than the array size declared by the packed
> type.  So I'm going to go out on a limb and conjecture that using a flexible
> array in the type declaration will fix this one; i.e., patching the code so
> the #ifdef __GNUC__ case reads:
> 
> typedef struct
> {
>   int Count;
>   Union List[];
> } __attribute__((packed)) Struct3;
> 
> If nobody is able to give me an account somewhere, could one of you with
> access to hardware please add this to %prep and try building again?
> 
> # Fix a test with type aliasing
> sed -i '/main\.c/a-fno-strict-aliasing'
> regression/cbmc/Pointer_array5/test.desc
> 

cbmc doesn't support this flag and failed with:
 
* *   CBMC 5.5 - Copyright (C) 2001-2016 (64-bit version)   * *
* *              Daniel Kroening, Edmund Clarke             * *
* * Carnegie Mellon University, Computer Science Department * *
* *                 kroening@kroening.com                   * *
* *        Protected in part by U.S. patent 7,225,417       * *

Usage:                       Purpose:

 cbmc [-?] [-h] [--help]      show help
 cbmc file.c ...              source file names
..

> # Fix a test with out-of-bounds access to a packed array
> sed -i '/__GNUC__/,/else/s/List\[1\]/List[]/'
> regression/cbmc/Pointer_byte_extract5/main.c
comfirmed that it fixes the issue

Comment 3 Ngo Than 2016-09-05 12:30:29 UTC
trace for the failed properties

CBMC version 5.5 64-bit s390x linux
Parsing regression/cbmc/Pointer_array5/main.c
file <Kommandozeile> line 0: <Kommandozeile>:0:0: Warnung: »__STDC_VERSION__« redefiniert
file <eingebaut> line 0: <eingebaut>:0:0: Anmerkung: dies ist die Stelle der vorherigen Definition
Converting
Type-checking main
Generating GOTO Program
Adding CPROVER library (s390x)
file <Kommandozeile> line 0: <Kommandozeile>:0:0: Warnung: »__STDC_VERSION__« redefiniert
file <eingebaut> line 0: <eingebaut>:0:0: Anmerkung: dies ist die Stelle der vorherigen Definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 95 steps
simple slicing removed 24 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
12568 variables, 25409 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0.038s

** Results:
[main.assertion.1] assertion address==&a0: FAILURE

Trace for main.assertion.1:

State 18 file regression/cbmc/Pointer_array5/main.c line 8 function main thread 0
----------------------------------------------------
  arraylen=0 (00000000000000000000000000000000)

State 19 file regression/cbmc/Pointer_array5/main.c line 8 function main thread 0
----------------------------------------------------
  arraylen=3 (00000000000000000000000000000011)

State 21 file regression/cbmc/Pointer_array5/main.c line 12 function main thread 0
----------------------------------------------------
  array_init=((signed int **)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 41 file regression/cbmc/Pointer_array5/main.c line 12 function main thread 0
----------------------------------------------------
  array_init=dynamic_object1 (0000001000000000000000000000000000000000000000000000000000000000)

State 42 file regression/cbmc/Pointer_array5/main.c line 14 function main thread 0
----------------------------------------------------
  a0=0 (00000000000000000000000000000000)

State 43 file regression/cbmc/Pointer_array5/main.c line 14 function main thread 0
----------------------------------------------------
  a1=0 (00000000000000000000000000000000)

State 44 file regression/cbmc/Pointer_array5/main.c line 14 function main thread 0
----------------------------------------------------
  a2=0 (00000000000000000000000000000000)

State 45 file regression/cbmc/Pointer_array5/main.c line 16 function main thread 0
----------------------------------------------------
  dynamic_object1[0l]=&a0!0@1 (0000001100000000000000000000000000000000000000000000000000000000)

State 46 file regression/cbmc/Pointer_array5/main.c line 17 function main thread 0
----------------------------------------------------
  dynamic_object1[1l]=&a1!0@1 (0000010000000000000000000000000000000000000000000000000000000000)

State 47 file regression/cbmc/Pointer_array5/main.c line 18 function main thread 0
----------------------------------------------------
  dynamic_object1[2l]=&a2!0@1 (0000010100000000000000000000000000000000000000000000000000000000)

State 48 file regression/cbmc/Pointer_array5/main.c line 20 function main thread 0
----------------------------------------------------
  local_array=((const void **)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 49 file regression/cbmc/Pointer_array5/main.c line 20 function main thread 0
----------------------------------------------------
  local_array=dynamic_object1 (0000001000000000000000000000000000000000000000000000000000000000)

State 50 file regression/cbmc/Pointer_array5/main.c line 22 function main thread 0
----------------------------------------------------
  address=((signed int *)NULL) (0000000000000000000000000000000000000000000000000000000000000000)

State 51 file regression/cbmc/Pointer_array5/main.c line 22 function main thread 0
----------------------------------------------------
  address=((signed int *)NULL) + 192 (0000000000000000000000000000000000000000000000000000000011000000)

Violated property:
  file regression/cbmc/Pointer_array5/main.c line 23 function main
  assertion address==&a0
  address == &a0


** 1 of 1 failed (1 iteration)
VERIFICATION FAILED

Comment 4 Fedora Update System 2016-09-16 19:43:45 UTC
cbmc-5.5-2.fc25 has been submitted as an update to Fedora 25. https://bodhi.fedoraproject.org/updates/FEDORA-2016-886bd77454

Comment 5 Fedora Update System 2016-09-16 19:43:53 UTC
cbmc-5.5-2.fc25 has been submitted as an update to Fedora 25. https://bodhi.fedoraproject.org/updates/FEDORA-2016-886bd77454

Comment 6 Fedora Update System 2016-09-16 19:44:53 UTC
cbmc-5.5-2.fc24 has been submitted as an update to Fedora 24. https://bodhi.fedoraproject.org/updates/FEDORA-2016-d045b1594c

Comment 7 Fedora Update System 2016-09-16 19:44:59 UTC
cbmc-5.5-2.fc24 has been submitted as an update to Fedora 24. https://bodhi.fedoraproject.org/updates/FEDORA-2016-d045b1594c

Comment 8 Fedora Update System 2016-09-18 06:51:54 UTC
cbmc-5.5-2.fc24 has been pushed to the Fedora 24 testing repository. If problems still persist, please make note of it in this bug report.
See https://fedoraproject.org/wiki/QA:Updates_Testing for
instructions on how to install test updates.
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2016-d045b1594c

Comment 9 Fedora Update System 2016-09-18 07:23:30 UTC
cbmc-5.5-2.fc25 has been pushed to the Fedora 25 testing repository. If problems still persist, please make note of it in this bug report.
See https://fedoraproject.org/wiki/QA:Updates_Testing for
instructions on how to install test updates.
You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2016-886bd77454

Comment 10 Fedora Update System 2016-09-22 07:33:40 UTC
cbmc-5.5-2.fc25 has been pushed to the Fedora 25 stable repository. If problems still persist, please make note of it in this bug report.

Comment 11 Fedora Update System 2016-09-27 03:53:55 UTC
cbmc-5.5-2.fc24 has been pushed to the Fedora 24 stable repository. If problems still persist, please make note of it in this bug report.


Note You need to log in before you can comment on or make changes to this bug.