Generalize and stabilize control flow alignment

GaloisInc / pate

Patches Assured up to Trace Equivalence

Other

15 stars 2 forks source link

Generalize and stabilize control flow alignment #388

Closed thebendavis closed 2 months ago

thebendavis commented 2 months ago

Complete control flow alignment needed to support Target7

lcasburn commented 2 months ago

Branch includes test for core algorithm
Ch 10 running
Double checking changes to script
- Will need Jim to review updated script & create gui replay (ie. to update return points from trampoline to specify merge points)
- Now accepts list of sync points
Target 7 not yet tested, will be part of separate ticket

lcasburn commented 2 months ago

Scripts have been updated
Found test that had been marked as expected failure but it shouldn't have been. Fixed.
Tests running locally but not yet working on CI

danmatichuk commented 2 months ago

Correction: found a test that is timing out locally. It is a bug that's causing the verifier to loop, I'm investigating it now.

lcasburn commented 2 months ago

From @danmatichuk: The fundamental issue causing the test to time out seems to be that stubs that return to synchronization point appear to not be handled properly.

Implicit invariant that all exit points match a sync address that is defined, in case of stub, realized this invariant was violated.
When adding sync point that arose from calling stub and stub returns to a synchronization address, we need to make sure that synchronization point added to data structure is the return point of the stub and not the address of the stub function itself.