Bitvector and array literal support for Theta backend

[as3810t]

This pull request adds support for bitvector expressions and array literals in the Theta backend. Also as a minor improvement closes #37 .

• [x] Bitvector support
• [x] Array literal support
• [x] Functional tests for the new features (Depends on this pull request in Theta)

[hajduakos]

https://github.com/ftsrg/theta/pull/77 was merged

[hajduakos]

As far as I know, https://github.com/ftsrg/theta/pull/77 only added syntactical support for bitvectors, besides --refinement UNSAT_CORE the other refinement algorithms do not really work. However, I am going to merge https://github.com/ftsrg/theta/pull/82 soon, which will add new refinement algorithms. It would be nice to use them by default for bitvectors. (Currently SEQ_ITP is the default.)

[hajduakos]

PR https://github.com/ftsrg/theta/pull/82 was merged, so Theta v2.4 has advanced refinement algorithms that support bitvectors. If #41 also gets merged here, functional tests could use these new algorithms.

[radl97]

Don't forget to enable testing theta with flat memory model:

Build result:

UNSUPPORTED: gazer :: theta/verif/memory/arrays1.c (15 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/arrays2_fail.c (16 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals1.c (17 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals2.c (18 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals3.c (19 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/globals4.c (20 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/local_passbyref1_fail.c (21 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref1_false.c (22 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref2.c (23 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref3_fail.c (24 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref4.c (25 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref5.c (26 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref6.c (27 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/passbyref7_fail.c (28 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/pointers1.c (29 of 102)
UNSUPPORTED: gazer :: theta/verif/memory/structs1.c (30 of 102)

The change would be deleting this file:

https://github.com/ftsrg/gazer/blob/master/test/theta/verif/memory/lit.local.cfg

(I think there was a change in these files in the PR)

@as3810t

[as3810t]

As of now, the functional tests in test/theta/verif/memory yield the following result:

Testing Time: 177.19s
********************
Failing Tests (1):
    gazer :: theta/verif/memory/globals2.c

********************
Timed Out Tests (4):
    gazer :: theta/verif/memory/globals4.c
    gazer :: theta/verif/memory/passbyref2.c
    gazer :: theta/verif/memory/passbyref5.c
    gazer :: theta/verif/memory/passbyref6.c

  Expected Passes    : 97
  Unexpected Failures: 1
  Individual Timeouts: 4

The failing test (globals2.c) generates a counterexample, which is correct if the error described in #42 is present in the CFA. Furthermore, as far as I can tell, the timeouts are the result of the massive amount of extremely computation-heavy bitvector operations, not infinite loops in the veriication algorithm.