Skip to content

Some memory model simplifications #768

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.

Sign up for GitHub

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

Jump to bottom
Draft
maul-esel wants to merge 20 commits into
base: dev
Choose a base branch
from
Draft

Some memory model simplifications #768

maul-esel wants to merge 20 commits into from

Conversation

@maul-esel
Copy link
Contributor

@maul-esel maul-esel commented Dec 21, 2025 •
edited
Loading

Since the dedicated work by @jankoerner in #756, our C translation uses general interfaces to encapsulate different memory model implementations, rather than hardcoding a single memory model all throughout the translation (thanks again for this work!).

This PR collects some simplifications and refactorings of the code for which there was not enough time in the project / before SV-COMP; with the goal to improve maintainability and make it easier to implement further memory models in the future.

To review the changes in this PR, it might be a good idea to view them commit-by-commit.

In addition to the changes already here, the following items could also be improved (some of them may simply require more documentation):

  • It would probably make sense to move a lot of this code into a dedicated sub-package, to bundle it in one place. Then, we should also see which parts need to be public and what can be package-private.
  • what is the meaning of the lists of tuples returned by
    • IMemoryAddressing::constructMallocSpecificationExpressions
    • IMemoryAddressing::constructDeallocSpecificationExpressions
    • IMemoryAddressing::constructAllocInitSpecificationExpressions
  • What is the meaning of these methods? (Improve documentation or reconsider if they should be implemented differently.)
    • IMemoryAddressing::constructUltimateInitStatements (what do these statements do?)
    • IMemoryAddressing::getFixedAddressCounterCountingStep
    • IMemoryAddressing::constructRhsAssignmentStatementHda
  • what is the relation between the methods ::doPointerArithmetic, ::addExpressionToPointer, addIntegerConstantToPointer and ::doPointerSubtraction on IMemoryAdressing? Can some of them be implemented in terms of the others?
  • These methods seem overly specific. Can they be implemented by a caller, using the other existing methods?
    • IMemoryAddressing::constructAddressForStructField (perhaps implementable using ::addIntegerConstantToPointer?)
    • IMemoryAddressing::getLastCharOfString
    • IMemoryAddressing::constructStrChrAssumeStatement (if not, improve documentation and let it return an expression)
    • IMemoryAddressing::checksForStringCopyOverlapping (otherwise, document parameters and return an expression)
    • IMemoryAddressing::constructReallocBodyStatements
  • Having two methods IMemoryAddressing::constructPointerValidityCheckExpr and ::constructPointerTargetFullyAllocatedCheckExpr seems specific to the 2-dimensional model. Can they be merged into a single method? (that perhaps returns a list of expressions ; and callers would need to take care of the size parameter separately e.g. through a call to ::addExpressionToPointer)
  • IMemoryAddressing::getChecksForFreeCall should return expressions (or ExpressionResults) rather than assert statements
  • Can IMemoryAddressing::constructMemSafeStatementsForPointerExpression be implemented in terms of ::constructPointerValidityCheckExpr and ::constructPointerTargetFullyAllocatedCheckExpr?
  • IMemoryAddressing::constructInitialPointerFromPointer only makes sense for the 2-dimensional model. It is used for variadic arguments; they must be implemented in another way.
  • IMemoryAddressing::getValidArray only makes sense for the 2-dimensional model. It is used only for memory neutrality checks; these should be implemented like ::constructPointerValidityCheckExpr etc.
  • An instance of IMemoryPointer is not actually a pointer. Can we rename the interface?
  • (where) is LocalLValueILocationPair needed? (if we keep it, make it a record, possibly private, and improve field names)
  • MemoryAddressingFactory violates the open-closed principle (for every new IMemoryPointer implementation, we would need to change this class). Can this functionality become a method on IMemoryPointer?
  • The construction of a suitable pointer-integer conversion in MemoryAddressingBase violates the open-closed principle (for every new IMemoryPointer implementation, we would need to change this class). Can this functionality become a method on IMemoryPointer?
  • update the documentation (in particular, of parameters) for MemoryHandler::getWriteCall
  • update the documentation for MemoryHandler::constructMemsafetyChecksForPointerExpression
  • document MemoryStructureMultiBitprecise
  • documentation for SimpleIncreasingStrategy mentions a type parameter that does not exist
  • The documentation for NonBijectiveMapping1D talks about base and offset (copy-pasted from 2D case). Is the mapping even non-bijective in the 1-dimensional case?
  • The fields SFO.MEMCPY and SFO.MEMSET are not used and can be deleted
  • the documentation of FakePointer1D talks about base and offset

@maul-esel
remove unused "unchecked read procedures"
0c8cc6c 
Unchecked reads are done directly as array accesses
(as documented for MemoryHandler::getReadUnchecked)
hence there do not exist corresponding procedures.
@maul-esel
MemoryHandler::getReadUnchecked is guaranteed to return only an expre…
82cc759 
…ssion

Hence, there is no need to wrap it into an ExpressionResult.
@maul-esel
MemoryStructureMultiBitprecise: exhaustive switch
99b1239
@maul-esel
IMemoryPointer::isNullPointer: avoid throwing ClassCastExceptions
7fddee1 
Perform instanceof-check inside the method for safe casting,
instead of leaving it to the caller.
Simplify the implementations and the calling code.
@maul-esel
IMemoryPointer::constructPointerRelationExpression: exhaustive switches
7fcd3ad
@maul-esel
use pattern-matching instead of casts
0610056
@maul-esel
move handling of specifications out of IMemoryAddressing
3d15c5b 
The appropriate accounting for CheckMode, the correct Spec, etc.
should not have to be implemented anew for every addressing mode.
@maul-esel
exhaustive switch
2809bae
@maul-esel
remove ITypeHandler::getMemoryPointer() method
09ad6ba 
It is not clear why this method should be part of this interface, and
the only usage of this method was on a concrete implementation anyway.
@maul-esel
make class private again
c9b7511
@maul-esel
exhaustive switch
9767f71
@maul-esel
SFO: remove unused MEMSET, MEMCPY fields
eb71653
@maul-esel
Move creation of AssertStatements out of IMemoryAddressing::getChecks…
819339d 
…ForFreeCall

The appropriate accounting for settings, the correct Spec, etc.
should not have to be implemented anew for every addressing mode.
@maul-esel
remove redundant method IMemoryAddressing::constructMemSafeStatements…
6f17b07 
…ForPointerExpression

The logic implemented in this method was essentially the same as in
the two already existing methods ::constructPointerValidityCheckExpr
and ::constructPointerTargetFullyAllocatedCheckExpr.

There is a slight edge case where the functionality differs:
the old code checked "offset < length", whereas the new code
(in ::constructPointerTargetFullyAllocatedCheckExpr) checks
only "offset <= length". However, I suspect this difference
is unintentional (I have added a TODO to clarify the correct
behaviour).
@maul-esel
replace IMemoryAddressing::getValidArray with ::constructMemoryNeutra…
180a8e3 
…lityCheckExpr

The old method was only used for this purpose, but did not make sense
for all memory models. Hence, this is now handled analogously to the
methods for pointer validity checks.
@maul-esel
Remove IMemoryAddressing::getLastCharOfString
fee3914 
This method was overly specific and can easily be implemented by the
single caller, using existing methods.

Furthermore, the implementation in MemoryAddressing1D was incorrect:
it simply returned "len-1" as a pointer.
@maul-esel
replace IMemoryAdressing::constructAddressForStructField by ::addExpr…
5eed0e5 
…essionToPointer
@maul-esel
allocation procedures: replace lists of tuples by meaningful record
6bc146e 
Instead of encoding the specifications of malloc, dealloc and allocInit
as lists of tuples containing expressions (which are used in "ensures"
resp. "free ensures" clauses) and sets of variables (which are used in
the "modifies" clause), they are now encoded using a specialized record.
@maul-esel
move "ptrBase" string constant to SFO
15a9ef8
@maul-esel
MemoryHandler: minor internal refactoring, removing some unused code
7f5e455
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@bahnwaerter bahnwaerter Awaiting requested review from bahnwaerter

@schuessf schuessf Awaiting requested review from schuessf

@jankoerner jankoerner Awaiting requested review from jankoerner

Assignees

No one assigned

Labels

C translation enhancement

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@maul-esel