Skip to content

goto-model validation: Validate constant_exprt#6786

Merged
kroening merged 2 commits intodiffblue:developfrom
tautschnig:feature/more-checks
Apr 11, 2022
Merged

goto-model validation: Validate constant_exprt#6786
kroening merged 2 commits intodiffblue:developfrom
tautschnig:feature/more-checks

Conversation

@tautschnig
Copy link
Collaborator

@tautschnig tautschnig commented Apr 6, 2022

We silently accept, and sometimes handle correctly, bitvector constants
that are encoded as -[absolute value] instead of two's complement. The
simplifier, however, will not handle this ambiguity as equalities over
constants are evaluated by comparing the value strings. Therefore, use
goto-model validation to ensure we do not process bitvector constants
that don't use two's complement encoding.

Fixes: #6759

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig mentioned this pull request Apr 6, 2022
Closed
@tautschnig tautschnig force-pushed the feature/more-checks branch 2 times, most recently from 6362898 to d5ccfcd Compare April 6, 2022 21:21
@kroening
Copy link
Collaborator

kroening commented Apr 6, 2022

While at it, we should also check that there are no leading zeros.

@kroening
Copy link
Collaborator

kroening commented Apr 6, 2022

Oh, and we need to stick to either 'A'-'F' or 'a'-'f', but shouldn't allow both.

@tautschnig tautschnig force-pushed the feature/more-checks branch from d5ccfcd to d1c2c0e Compare April 7, 2022 21:08
@tautschnig
Copy link
Collaborator Author

tautschnig commented Apr 7, 2022

While at it, we should also check that there are no leading zeros.

Done!

@tautschnig
Copy link
Collaborator Author

tautschnig commented Apr 7, 2022

Oh, and we need to stick to either 'A'-'F' or 'a'-'f', but shouldn't allow both.

Oh, that would indeed just cause the same sort of trouble. Check is now more constrained.

@tautschnig
goto-model validation: Validate constant_exprt
9624d5d 
We silently accept, and sometimes handle correctly, bitvector constants
that are encoded as -[absolute value] instead of two's complement. The
simplifier, however, will not handle this ambiguity as equalities over
constants are evaluated by comparing the value strings. Therefore, use
goto-model validation to ensure we do not process bitvector constants
that don't use two's complement encoding.

Fixes: diffblue#6759
@tautschnig
Enable goto-model validation for ternary and bitvector expressions
9c12e0f 
The code was almost there, but was never triggered.
@tautschnig tautschnig force-pushed the feature/more-checks branch from d1c2c0e to 9c12e0f Compare April 9, 2022 19:39
@tautschnig tautschnig removed their assignment Apr 9, 2022
@codecov
Copy link

codecov bot commented Apr 9, 2022

Codecov Report

Merging #6786 (9c12e0f) into develop (b7c6692) will increase coverage by 0.07%.
The diff coverage is 88.34%.

@@             Coverage Diff             @@
##           develop    #6786      +/-   ##
===========================================
+ Coverage    76.90%   76.98%   +0.07%     
===========================================
  Files         1590     1593       +3     
  Lines       183969   184145     +176     
===========================================
+ Hits        141486   141755     +269     
+ Misses       42483    42390      -93
Impacted Files Coverage Δ
..._incremental/smt2_incremental_decision_procedure.h 75.00% <ø> (ø)
src/util/std_expr.h 93.18% <50.00%> (-0.48%) ⬇️
...c/solvers/smt2_incremental/convert_expr_to_smt.cpp 84.87% <76.74%> (+12.78%) ⬆️
src/util/validate_expressions.cpp 93.75% <90.00%> (-1.71%) ⬇️
src/solvers/smt2_incremental/object_tracking.cpp 97.87% <97.87%> (ø)
src/goto-programs/goto_function.cpp 100.00% <100.00%> (ø)
src/solvers/smt2_incremental/object_tracking.h 100.00% <100.00%> (ø)
...ncremental/smt2_incremental_decision_procedure.cpp 94.15% <100.00%> (+0.14%) ⬆️
src/util/std_expr.cpp 69.67% <100.00%> (+1.56%) ⬆️
...t/solvers/smt2_incremental/convert_expr_to_smt.cpp 100.00% <100.00%> (ø)
... and 8 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 1a4c66e...9c12e0f. Read the comment docs.

@kroening kroening merged commit 196e7d1 into diffblue:develop Apr 11, 2022
@tautschnig tautschnig deleted the feature/more-checks branch April 11, 2022 20:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

Assignees

@kroening kroening

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

CBMC accepts -<hex> constants at the irep level, but does the wrong thing with them

2 participants

@tautschnig @kroening