Generating XCFA instead of CFA and some other changes

[radl97]

This is a draft PR for possible contributions to the upstream Gazer project.
The point is not to directly merge or cherry-pick from here, rather select features that can be (with some extra work) integrated upstream.

The commits add some features for me to work with. This breaks normal functionality like gazer-bmc, even gazer-theta!, but I can fix these up (in my spare time?) if you'd like to accept some of these contributions.

The changes/features right now:

• Disable loops to recursion transformation
• XCFA generation
• Global variables support
• Simple memory model for globals and alloca'd locals
• Swap function call with an inline implementation; decoupled analysis and inline implementation
• Demo for non-reentrant mutex usage checks
• Demo for handling generated stub implementations (written in Xcfa)

A bit more precisely:

• NOT CLEAN COMMITS: Loops to recursion transformation at the CFA level is disabled (this is useful for non-gazer-bmc). For gazer-theta there is currently an undoing transformation (which does more right now, so I couldn't remove it), which looks as a maintenance overhead.

  Note that some codes are disabled which are related to using loops, but I guess disabling the loop registration is enough (because there will be no loops detected to transform to a separate CFA).
  This way there is a one-to-one mapping between LLVM functions and CFAs.

  EDIT: I don't know whether Phi nodes are handled in this skipped step. (If yes, it would mean unlinked variables along loop exits maybe?) It looks suspicious, but the functional tests did not show anything scary...

• NOT CLEAN: XCFA generation seems pretty well working right now (only minor hacks), so creating a common base for CFA generation and XCFA generation can be designed from the changes (What did change, what did not change).

  Call transition stmt was added, also some syntax changed (high-level syntax, because of how multiple functions are supported)

• NOT CLEAN: Tracing is currently disabled, so most functional tests run well (if used with xcfa-cli instead of cfa-cli on Theta side; with the latest changes in branch https://github.com/ftsrg/theta/xcfa-partial-order ).

• RELATIVELY CLEAN Also, I plan to add global variables (or rather, add a storage of regular global vars to AutomataSystem). This seems like a different layer than MemoryModels, but I am not so sure about the implementation...

  EDIT:
  I will be trying to implement a memory model that handles this. In the future, it would be awesome if this could be composed with another memory model (e.g. try with noaliasing memorymodel, when it would not be sound, work with flat mapping, etc.)
  It seems that this problem is closely coupled with how arrays will be handled, so this will probably be related to handling arrays in Theta. I know there are on-going efforts for this, but I don't know how my work will be part of the big picture...

• RELATIVELY CLEAN COMMITS: (from the above point) I've implemented a simple memory model, which seems to work for XCFAs. For global variables, it is out-of-scope in the viewpoint of gazer-bmc (as it rolls with its MemSSA instead of what I use) and Theta CFA (not XCFA).
  The AutomataSystem contains global variables, I've tested with some of the functional tests.

• POC (clean commits, but not configurable as of now): Generate optimizable implementation from known functions. The point would be some intrinsics like llvm.memcpy, for known domain-specific API. There could be overlapping with: gazer.SpecialFunctions gazer.Checks and llvm., but:

  • gazer.SpecialFunctions: is at a too late stage (at CFA level), where a call GetFixPointer() -> GetFixPointer_var change could not be implemented. This is because lowering to CFA level probably does not want a pointer returning function. Also, there are a lot of optimizations around pointers, which we could surely use.
  • gazer.Checks: this is at the right abstraction level, good for optimizations, but it's main goal is to create checks, and I haven't seen if we can use it.

• Demo for non-reentrant mutex usage checks: Enter.* and Exit.* functions are swapped with a global variable check. Also, initialization takes place at the start of main, and usage is checked at the end of the program (just before returning).

• (Not entirely functional) A whole demo for using generated XCFAs and calling across them with C calls through declared, but undefined functions. Also contains a small driver which runs Gazer's core through all of the files in the given directory.

Please feel free to add some comments on what would make a good contribution. I'd like to emphasize that the changes in the commits contain only temporary solutions, but looking at them seems like a good way to see what changes would be needed.

Lit output:

Testing Time: 69.24s
********************
Failing Tests (16):
    gazer :: theta/cfa/counter.c
    gazer :: theta/cfa/multicfa.c
    gazer :: theta/verif/memory/arrays1.c
    gazer :: theta/verif/memory/arrays2_fail.c
    gazer :: theta/verif/memory/globals1.c
    gazer :: theta/verif/memory/globals2.c
    gazer :: theta/verif/memory/globals3.c
    gazer :: theta/verif/memory/local_passbyref1_fail.c
    gazer :: theta/verif/memory/passbyref1_false.c
    gazer :: theta/verif/memory/passbyref2.c
    gazer :: theta/verif/memory/passbyref3_fail.c
    gazer :: theta/verif/memory/passbyref4.c
    gazer :: theta/verif/memory/passbyref5.c
    gazer :: theta/verif/memory/passbyref6.c
    gazer :: theta/verif/memory/passbyref7_fail.c
    gazer :: theta/verif/memory/structs1.c

********************
Timed Out Tests (3):
    gazer :: theta/verif/base/loops2_fail.c
    gazer :: theta/verif/base/loops3_fail.c
    gazer :: theta/verif/memory/globals4.c

Note that some are failing because they are unsupported (and reach an assertion fail in Gazer), some fail because Theta xcfa backend (which does not follow havoc'd variables, because it cannot handle predicate abstractions as of now).

Resolves #17

[radl97]

Testing Time: 76.08s
********************
Failing Tests (10):
    gazer :: theta/verif/memory/arrays1.c
    gazer :: theta/verif/memory/arrays2_fail.c
    gazer :: theta/verif/memory/globals2.c
    gazer :: theta/verif/memory/globals3.c
    gazer :: theta/verif/memory/local_passbyref1_fail.c
    gazer :: theta/verif/memory/passbyref2.c
    gazer :: theta/verif/memory/passbyref5.c
    gazer :: theta/verif/memory/passbyref6.c
    gazer :: theta/verif/memory/passbyref7_fail.c
    gazer :: theta/verif/memory/structs1.c

********************
Timed Out Tests (3):
    gazer :: theta/verif/base/loops2_fail.c
    gazer :: theta/verif/base/loops3_fail.c
    gazer :: theta/verif/memory/globals4.c

after adding stub (unsound) implementations to simple memory model so intrinsics do not break the naive simple memory model (see #24 )

[radl97]

Also resolves #17

[ghost]

Removing --timeout is not needed. However, psutil python package (pip3 install psutil) is required then.

[ghost]

Duplicate