goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Ego-Lane-Derived-Digests for Privatizations: `ProtectionBasedTIDPriv` #1398

Closed michael-schwarz closed 3 months ago

michael-schwarz commented 3 months ago

Introduces one of the new privatizations which will need to be evaluated for my thesis. This might actually be a lightweight interesting instance that might be worth evaluating it in practice.

This takes the protection based analysis and replaces [g] and [g]' by [g,A] and [g,A]' respectively, where A is an ego-lane derived digest.

Implementation-wise we once more use the Reduced-Cardinal-Powerset construction and change types of unknowns from ValD to partial maps Digest -> ValD with default value bot.

TODO:

michael-schwarz commented 3 months ago

I was able to cast this as a generic lifter, which means we get no additional code duplication here :smile: