Reconsider the `architecture` description in the witness graphml files
MartinSpiessl opened this issue · 1 comments
For the task definition files we now have a consistent filed named data_model
that contains either ILP32
or LP64
:
https://github.com/sosy-lab/sv-benchmarks#task-definitions
- options: parameters that are relevant for verification or give extra information:
- language: programming language that the program is written in (C or Java)
- data_model data model of the computer architecture (ILP32, LP64, see http://www.unix.org/whitepapers/64bit.html, only for C programs)
This is more precise than what we currently put under architecture in the witness(32bit
/64bit
), as the number of bits in the architecture doesn't fix the whole data model (e.g. there are differences in the data model for ARM64 vs. AMD64).
So we should consider to extend the witness format by a datamodel
/data-model
field that stores this more precise information. We could then deprecate the old architecture field, so validators still undetstand that one but use the data model if specified.
In general, using the same strings as in the task definitions is certainly a good idea.
Note sosy-lab/sv-benchmarks#1125: would be beneficial to come to a conclusion on that issue before adding the same values to the witness format.