Property description for CFAs

[hajduakos]

The algorithms support arbitrary target predicates over states. However, the CFA tool always checks the reachability of the designated error location. It could be generalized by developing a simple property specification language for the CFA tool. For example:

• --model="sample.cfa" --property="reach={L12}"
• --model="sample.cfa" --property="expr={x > 0}"

[hajduakos]

Let's start with the first feature, namely being able to provide the error location separately (currently it is hardcoded in the CFA). For backward compatibility, I would still allow the error location to be specified inside the CFA, however, it would be optional, and command line tools would accept a --errorloc <LOC NAME> argument. There would be 4 cases:

	Error loc given in CFA	No error loc given in CFA
Error loc given as argument	Use argument, but possibly give a warning	Use argument
No error loc given as argument	Use error loc from CFA	Error: nothing to verify

I think the main question is what to do if both the CFA and the argument specifies an error location. I'd say that the argument should override the CFA, with possibly giving a warning.

Any thoughts @vincemolnar @as3810t ?

[vincemolnar]

Seems good to me, but maybe it would be better to give the argument a less specific (and tehrefore more futureproof) name, for example --targetloc (and then the result could be written more precisely too, e.g. Verification completed, [target|error] location is [reachable|unreachable].

[hajduakos]

We have now support for arbitrary error locations with the --errorloc parameter. Supporting properties like x >= 0 seems to have one critical point, which is large block encoding (LBE). In LBE, sequential paths (or sometimes even branching statements) are merged into a single step. This is not really possible if we want arbitrary properties. For example, x--; x++; could cause the property x >= 0 to be violated in intermediate steps that would not be found with LBE.