Goose  Artifact [8b894488fc]

Artifact 8b894488fcd757fa958168d131fa1b4f328d04c495eb91d482c951b7de0668ef:

• File bs/verify/condition.h — part of check-in [b00c682e34] at 2020-06-03 23:08:17 on branch trunk —
  • Verifier: a bunch of refactoring to better keep track of the types of the z3 expressions stored in variables.
  • Verifier: handle "LoadFromAddress" for addresses that point to tuple members.
  (user: achavasse size: 1276)

#ifndef GOOSE_VERIFY_CONDITION_H
#define GOOSE_VERIFY_CONDITION_H

namespace goose::builtins
{
    class FuncType;
}

namespace goose::verify
{
    // Checks that a function's pre/post consitions are
    // satisfiable, and emits any necessary diagnostic.
    class Condition
    {
        public:
            Condition( const sema::Context& c );
            Condition( const sema::Context& c, const builtins::FuncType& funcType );

            // Add an assertion list in the form of a Vector of values.
            // Emits a diagnostic and returns false if any of the expression
            // can't be represented as a z3 expression.
            bool addConditionsList( const pvec& assList );

            // Checks the satisfiability of the conditions. Emits diagnostics and return
            // false if they aren't.
            bool verify();

        private:
            const sema::Context& m_context;
            z3::solver m_solver;
            Builder m_builder;

            // Keep track of the ids of bool constants we generated to track which
            // conditions have failed, along with the location of the corresponding expressions.
            vector< pair< uint32_t, uint32_t > > m_idAndLocs;

            uint32_t m_nextIndex = 0;
    };
}

#endif