Add source metadata to program

[hernanponcedeleon]

This contains the changes from #1102 that were unreleaded to the witness generation.

[ThomasHaas]

I'm not sure if we should make any metadata mandatory. We can keep it like this for now, but it does feel a bit strange to me.

[hernanponcedeleon]

But then we should adapt other classes (e.g., OutputGenerator) which right now require this metadata to exists.

[ThomasHaas]

Yes, classes would need adapt. We can also make the input path an explicit field of Program (like you had it in #1102) to signify that is mandatory. We can also have mandatory metadata, but so far we didn't have that.

I think we will need to discuss guidelines for what Metadata should be used for, if it must be optional or can be mandatory, if it is allowed to affect semantics, and so on. At least some basic principles to follow would be useful.

[hernanponcedeleon]

I think we will need to discuss guidelines for what Metadata should be used for, if it must be optional or can be mandatory, if it is allowed to affect semantics, and so on. At least some basic principles to follow would be useful.

Can you draft a PR for this? That PR can also do the restructuring you suggested here (I think having the metadata as an inner class would be the best since otherwise we might forget we have some specific metadata for some class when doing changes to that class).

[ThomasHaas]

I can do the changes I mentioned in #1097. Do you want to use that PR as a discussion platform regarding Metadata? I thought about opening a discussion thread instead.

[hernanponcedeleon]

Let's have those changes and the documentation on guidelines as a single PR.

We can probably discuss offline about a first draft and during review we see if we need to adapt.

[ThomasHaas]

I'm still not so happy about the helper method here that throws an exception.
Can't we just get the metadata in OutputGenerator (the only user of that data, right? via getMetadata) and if it is absent default to the program's name instead? We could even go further and check if the program has a name and if not default to "unknown".

I would then also change the toSummary method back to use a string instead of a Path so that we can pass the program's name and possibly dummy value.

EDIT: Then you also don't need to invent fake source information in the UI code I think. Setting the name of the program is enough to get the correct output.

[github-actions]

Performance comparison

Linux x64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	12.718 ± 0.200 s	12.685 ± 0.269 s	➖ +0.2% [-20.8%, +21.3%]	UNKNOWN
benchmarks/locks/mutex_musl.c	24.875 ± 2.818 s	26.020 ± 2.740 s	➖ -5.4% [-94.1%, +83.4%]	UNKNOWN
benchmarks/lfds/dglm.c	21.922 ± 2.013 s	21.440 ± 1.465 s	➖ +1.8% [-46.0%, +49.6%]	UNKNOWN
benchmarks/lfds/ms.c	32.300 ± 0.688 s	35.843 ± 4.607 s	➖ -11.2% [-106.4%, +84.1%]	UNKNOWN
benchmarks/lfds/treiber.c	10.013 ± 0.331 s	9.307 ± 0.397 s	➖ +6.9% [-32.0%, +45.8%]	UNKNOWN
benchmarks/lfds/safe_stack.c	7.895 ± 0.686 s	7.198 ± 0.337 s	➖ +8.2% [-58.0%, +74.3%]	UNKNOWN
benchmarks/challenging/cna.c	36.703 ± 4.906 s	32.059 ± 0.140 s	➖ +11.5% [-59.6%, +82.7%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	6.440 ± 0.142 s	6.435 ± 0.093 s	➖ +0.1% [-10.3%, +10.5%]	UNKNOWN
benchmarks/challenging/cna.c	14.611 ± 1.415 s	14.430 ± 0.154 s	➖ +0.6% [-58.2%, +59.3%]	UNKNOWN
benchmarks/challenging/wsq.c	5.757 ± 0.096 s	5.667 ± 0.038 s	➖ +1.6% [-8.9%, +12.0%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	16.579 ± 0.419 s	16.486 ± 0.682 s	➖ +0.5% [-22.6%, +23.7%]	UNKNOWN
benchmarks/locks/mutex_musl.c	16.647 ± 0.441 s	16.172 ± 0.460 s	✅ +2.9% [+1.1%, +4.6%]	UNKNOWN
benchmarks/lfds/dglm.c	4.779 ± 0.154 s	5.032 ± 0.191 s	❌ -5.3% [-9.0%, -1.6%]	UNKNOWN
benchmarks/lfds/ms.c	24.621 ± 3.496 s	22.834 ± 1.224 s	➖ +6.5% [-38.6%, +51.7%]	UNKNOWN
benchmarks/lfds/treiber.c	15.357 ± 0.810 s	16.149 ± 0.922 s	➖ -5.2% [-21.8%, +11.5%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	251.219 ± 6.052 s	247.757 ± 4.686 s	➖ +1.4% [-12.2%, +14.9%]

3 benchmark(s) omitted because both averages were below 5 seconds.

macOS ARM64

Benchmark details

Memory model: vmm

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/cna.c	25.442 ± 0.531 s	22.959 ± 0.242 s	✅ +9.7% [+2.1%, +17.4%]	UNKNOWN
benchmarks/locks/mutex_musl.c	27.200 ± 0.905 s	28.191 ± 2.584 s	➖ -3.6% [-46.9%, +39.7%]	UNKNOWN
benchmarks/lfds/dglm.c	50.400 ± 1.585 s	48.889 ± 4.081 s	➖ +3.1% [-27.4%, +33.6%]	UNKNOWN
benchmarks/lfds/ms.c	72.333 ± 9.074 s	73.000 ± 6.245 s	➖ -1.5% [-54.8%, +51.8%]	UNKNOWN
benchmarks/lfds/treiber.c	15.811 ± 2.828 s	14.786 ± 1.633 s	➖ +5.4% [-60.1%, +70.8%]	UNKNOWN
benchmarks/lfds/safe_stack.c	11.341 ± 0.568 s	11.517 ± 0.516 s	➖ -1.6% [-10.7%, +7.6%]	UNKNOWN
benchmarks/challenging/cna.c	49.828 ± 2.615 s	51.118 ± 0.872 s	➖ -2.8% [-33.0%, +27.5%]	UNKNOWN

Memory model: aarch64

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	27.112 ± 4.674 s	23.831 ± 1.426 s	➖ +10.8% [-56.2%, +77.7%]	UNKNOWN
benchmarks/locks/mutex_musl.c	17.515 ± 1.608 s	18.155 ± 1.492 s	➖ -3.9% [-43.7%, +36.0%]	UNKNOWN
benchmarks/lfds/dglm.c	13.162 ± 0.113 s	13.612 ± 2.287 s	➖ -3.5% [-108.2%, +101.1%]	PASS
benchmarks/lfds/ms.c	15.844 ± 0.280 s	14.862 ± 0.243 s	✅ +6.2% [+3.0%, +9.4%]	UNKNOWN
benchmarks/challenging/cna.c	38.762 ± 2.217 s	35.103 ± 4.091 s	➖ +9.5% [-35.1%, +54.1%]	UNKNOWN
benchmarks/challenging/wsq.c	21.553 ± 4.797 s	18.875 ± 1.135 s	➖ +9.1% [-119.3%, +137.5%]	UNKNOWN

Memory model: power

Benchmark	Base branch	PR branch	Improvement (99% CI)	Result
benchmarks/locks/linuxrwlock.c	55.138 ± 3.176 s	66.629 ± 7.831 s	➖ -20.6% [-63.5%, +22.4%]	UNKNOWN
benchmarks/locks/mutex_musl.c	37.284 ± 7.622 s	33.699 ± 4.477 s	➖ +8.6% [-43.6%, +60.9%]	UNKNOWN
benchmarks/lfds/dglm.c	9.868 ± 0.811 s	9.828 ± 1.067 s	➖ +0.4% [-45.1%, +45.9%]	UNKNOWN
benchmarks/lfds/ms.c	51.080 ± 4.187 s	48.754 ± 2.637 s	➖ +3.9% [-67.3%, +75.1%]	UNKNOWN
benchmarks/lfds/treiber.c	21.467 ± 1.491 s	19.708 ± 1.302 s	➖ +7.7% [-54.8%, +70.2%]	UNKNOWN

Total

Benchmarks	Base branch	PR branch	Improvement (99% CI)
All reported benchmarks	561.142 ± 17.535 s	553.515 ± 16.117 s	➖ +1.3% [-19.2%, +21.9%]