Verifier 1

[SkymanOne]

Summary

• We use z3 as a SMT solver
• Translate expression to Z3 AST
• For this iteration, we only support checking constraints in st blocks for satisfiability
• It also includes a small draft of the mathematical model behind the checking.

Description

In this iteration of the verifier, we approach checking the logical bounds of different declarations for satisfiability. We first parse the declaration blocks and construct the scopes of Z3 constants so we can refer to them in logical formulas.

We then establish any links between declarations (i.e., an encapsulated model in a state, state transition bound in function, state inheritance bound in states). This later allows us to verify that constraints in linked entities don't contradict each other.

The next stage is to parse the expression AST into concrete Z3 AST.
With parsing, we have several limitations and workarounds:

• We disallow function call and structure initialisation for this iteration.
• The variable expression is turned into Z3 constant from the provided scope.
• If we refer to the other state (e.g. s1.field), then we resolve the s1 scope and lookup the Z3 constant for field.
• Enum access is naively transformed to constant with name enum_ident.field_name
• Models, Structs field access is transformed similarly to ident.field_no
• When parsing the whole expression, we bind it with a boolean constant that uniquely tracks the constraint (i.e. k!1 => a > b)

Having parsed the expression, we can now check the constraints of individual blocks for satisfiability. We extract a list of constraints for each declaration block and use the solver to check. If the bounds are unsatisfiable, then we find the unsatisfiable core (the constants that contradict each other) and return their numbers to the caller, which later gets reported by the CLI.

With constraints from linked blocks, we construct an undirected graph of linked nodes and find linked components using the Tarjan scc algorithm. For each block of connected components, we collect constraints and map them to their respective declaration symbols. The verification procedure is the same as above, except we return constraint numbers with their respective symbols in order to find conflicting declarations.