Skip to content

goto-cc crashes on softfloat code using __int128 #5103

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
andreast271 opened this issue Sep 11, 2019 · 1 comment · Fixed by #5758
Closed

goto-cc crashes on softfloat code using __int128 #5103

andreast271 opened this issue Sep 11, 2019 · 1 comment · Fixed by #5758

Comments

@andreast271
Copy link
Contributor

CBMC version: gcc (goto-cc 5.12 (crest.merged-48-gabe78fc77-dirty)) 7.4.0
Operating system: 4.15.0-45-generic x86_64 GNU/Linux
Exact command line resulting in the issue: goto-cc sf.c
What behaviour did you expect: no crash
What happened instead: invariant failure

The following is a reduced version of the softfloat code causing the crash:
file sf.c:

void softfloat_mul128To256M(unsigned a)
{
  unsigned __int128 z;
  z = (unsigned __int128) a;
  z += (a < 1);
}

command: goto-cc sf.c

output:

--- begin invariant violation report ---
Invariant check failed
File: ../util/std_types.h:1091 function: to_bitvector_type
Condition: can_cast_type<bitvector_typet>(type)
Reason: Precondition
...
@hannes-steffenhagen-diffblue
Copy link
Contributor

This is caused by the implicit promotion of the boolean a < 1 to __int128 failing because the promotion code assumes that what it's getting is going to be a bitvector already (and our internal bool type is its own thing rather than a bitvector)

tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 17, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 18, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 19, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 19, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 19, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 24, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 28, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Jan 29, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 1, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 2, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 3, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 3, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 11, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 15, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 3, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Mar 30, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue May 7, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue May 14, 2021
We use Booleans instead of int as type of binary predicates. This must
not preclude mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 9, 2022
We use Booleans instead of int as type of binary predicates, and enums
don't convert to bitvector types directly either. This must not preclude
mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
tautschnig added a commit to tautschnig/cbmc that referenced this issue Feb 9, 2022
We use Booleans instead of int as type of binary predicates, and enums
don't convert to bitvector types directly either. This must not preclude
mixing binary predicates with bitvector-typed expressions.

Fixes: diffblue#5103
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants