SymblicAbstractionTest Class Reference

Public Member Functions
	SymblicAbstractionTest ()=default
	~SymblicAbstractionTest ()=default
void	test_print ()
AbstractState	RSY_time (AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
AbstractState	Bilateral_time (AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
AbstractState	BS_time (AbstractState &inv, const Z3Expr &phi, RelationSolver &rs)
void	testRelExeState1_1 ()
void	testRelExeState1_2 ()
void	testRelExeState2_1 ()
void	testRelExeState2_2 ()
void	testRelExeState2_3 ()
void	testRelExeState2_4 ()
void	testRelExeState2_5 ()
void	testRelExeState3_1 ()
void	testRelExeState3_2 ()
void	testRelExeState3_3 ()
void	testRelExeState3_4 ()
void	testRelExeState4_1 ()
void	testsValidation ()

Static Public Member Functions
static z3::context &	getContext ()

Detailed Description

Definition at line 54 of file ae.cpp.

Constructor & Destructor Documentation

SymblicAbstractionTest()

SymblicAbstractionTest::SymblicAbstractionTest ( )

default

~SymblicAbstractionTest()

SymblicAbstractionTest::~SymblicAbstractionTest ( )

default

Member Function Documentation

Bilateral_time()

AbstractState SymblicAbstractionTest::Bilateral_time ( AbstractState &  inv, const Z3Expr &  phi, RelationSolver &  rs  )

inline

Definition at line 83 of file ae.cpp.

    {
        auto start_time = std::chrono::high_resolution_clock::now();
        AbstractState resBilateral = rs.bilateral(inv, phi);
        auto end_time = std::chrono::high_resolution_clock::now();
        auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
                            end_time - start_time);
        outs() << "running time of Bilateral: " << duration.count()
               << " microseconds\n";
        return resBilateral;
    }

BS_time()

AbstractState SymblicAbstractionTest::BS_time ( AbstractState &  inv, const Z3Expr &  phi, RelationSolver &  rs  )

inline

Definition at line 95 of file ae.cpp.

    {
        auto start_time = std::chrono::high_resolution_clock::now();
        AbstractState resBS = rs.BS(inv, phi);
        auto end_time = std::chrono::high_resolution_clock::now();
        auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
                            end_time - start_time);
        outs() << "running time of BS       : " << duration.count()
               << " microseconds\n";
        return resBS;
    }

getContext()

static z3::context& SymblicAbstractionTest::getContext ( )

inlinestatic

Definition at line 61 of file ae.cpp.

    {
        return Z3Expr::getContext();
    }

RSY_time()

AbstractState SymblicAbstractionTest::RSY_time ( AbstractState &  inv, const Z3Expr &  phi, RelationSolver &  rs  )

inline

Definition at line 71 of file ae.cpp.

    {
        auto start_time = std::chrono::high_resolution_clock::now();
        AbstractState resRSY = rs.RSY(inv, phi);
        auto end_time = std::chrono::high_resolution_clock::now();
        auto duration = std::chrono::duration_cast<std::chrono::microseconds>(
                            end_time - start_time);
        outs() << "running time of RSY      : " << duration.count()
               << " microseconds\n";
        return resRSY;
    }

test_print()

void SymblicAbstractionTest::test_print ( )

inline

Definition at line 66 of file ae.cpp.

    {
        outs() << "hello print\n";
    }

testRelExeState1_1()

void SymblicAbstractionTest::testRelExeState1_1 ( )

inline

Definition at line 108 of file ae.cpp.

    {
        outs() << sucMsg("\t SUCCESS :") << "test1_1 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 1];
        itv[0] = IntervalValue(0, 1);
        relation[0] = getContext().int_const("0");
        // var1 := var0 + 1;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0") + 1;
        itv[1] = itv[0].getInterval() + IntervalValue(1);
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[1], res);
        assert(res == Set<u32_t>({0, 1}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[0,1] 1:[1,2]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 1)}, {1, IntervalValue(1, 2)}};
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState1_2()

void SymblicAbstractionTest::testRelExeState1_2 ( )

inline

Definition at line 142 of file ae.cpp.

    {
        outs() << "test1_2 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 1];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 1);
        // var1 := var0 + 1;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0") * 2;
        itv[1] = itv[0].getInterval() * IntervalValue(2);
 
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[1], res);
        assert(res == Set<u32_t>({0, 1}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[0,1] 1:[0,2]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 1)}, {1, IntervalValue(0, 2)}};
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState2_1()

void SymblicAbstractionTest::testRelExeState2_1 ( )

inline

Definition at line 177 of file ae.cpp.

    {
        outs() << "test2_1 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 10];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 10);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 - var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") - getContext().int_const("0");
        itv[2] = itv[1].getInterval() - itv[0].getInterval();
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[0,10] 1:[0,10] 2:[0,0]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 10)},
            {1, IntervalValue(0, 10)},
            {2, IntervalValue(0, 0)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState2_2()

void SymblicAbstractionTest::testRelExeState2_2 ( )

inline

Definition at line 219 of file ae.cpp.

    {
        outs() << "test2_2 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 100];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 100);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 - var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") - getContext().int_const("0");
        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[0,100] 1:[0,100] 2:[0,0]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 100)},
            {1, IntervalValue(0, 100)},
            {2, IntervalValue(0, 0)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState2_3()

void SymblicAbstractionTest::testRelExeState2_3 ( )

inline

Definition at line 262 of file ae.cpp.

    {
        outs() << "test2_3 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 1000];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 1000);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 - var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") - getContext().int_const("0");
        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[0,1000] 1:[0,1000] 2:[0,0]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 1000)},
            {1, IntervalValue(0, 1000)},
            {2, IntervalValue(0, 0)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState2_4()

void SymblicAbstractionTest::testRelExeState2_4 ( )

inline

Definition at line 305 of file ae.cpp.

    {
        outs() << "test2_4 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 10000];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 10000);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 - var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") - getContext().int_const("0");
        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = RSY_time(inv, phi, rs);
        AbstractState resBilateral = Bilateral_time(inv, phi, rs);
        AbstractState resBS = BS_time(inv, phi, rs);
        // 0:[0,10000] 1:[0,10000] 2:[0,0]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 10000)},
            {1, IntervalValue(0, 10000)},
            {2, IntervalValue(0, 0)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState2_5()

void SymblicAbstractionTest::testRelExeState2_5 ( )

inline

Definition at line 348 of file ae.cpp.

    {
        outs() << "test2_5 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 100000];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 100000);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 - var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") - getContext().int_const("0");
        itv[2] = itv[1].getInterval() - itv[0].getInterval();
 
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = RSY_time(inv, phi, rs);
        AbstractState resBilateral = Bilateral_time(inv, phi, rs);
        AbstractState resBS = BS_time(inv, phi, rs);
        // 0:[0,100000] 1:[0,100000] 2:[0,0]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 100000)},
            {1, IntervalValue(0, 100000)},
            {2, IntervalValue(0, 0)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState3_1()

void SymblicAbstractionTest::testRelExeState3_1 ( )

inline

Definition at line 391 of file ae.cpp.

    {
        outs() << "test3_1 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [1, 10];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(1, 10);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 / var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") / getContext().int_const("0");
        itv[2] = itv[1].getInterval() / itv[0].getInterval();
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[1,10] 1:[1,10] 2:[1,1]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 10)},
            {1, IntervalValue(1, 10)},
            {2, IntervalValue(1, 1)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState3_2()

void SymblicAbstractionTest::testRelExeState3_2 ( )

inline

Definition at line 433 of file ae.cpp.

    {
        outs() << "test3_2 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [1, 1000];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(1, 1000);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 / var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") / getContext().int_const("0");
        itv[2] = itv[1].getInterval() / itv[0].getInterval();
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = rs.RSY(inv, phi);
        AbstractState resBilateral = rs.bilateral(inv, phi);
        AbstractState resBS = rs.BS(inv, phi);
        // 0:[1,1000] 1:[1,1000] 2:[1,1]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 1000)},
            {1, IntervalValue(1, 1000)},
            {2, IntervalValue(1, 1)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState3_3()

void SymblicAbstractionTest::testRelExeState3_3 ( )

inline

Definition at line 475 of file ae.cpp.

    {
        outs() << "test3_3 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [1, 10000];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(1, 10000);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 / var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") / getContext().int_const("0");
        itv[2] = itv[1].getInterval() / itv[0].getInterval();
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = RSY_time(inv, phi, rs);
        AbstractState resBilateral = Bilateral_time(inv, phi, rs);
        AbstractState resBS = BS_time(inv, phi, rs);
        // 0:[1,10000] 1:[1,10000] 2:[1,1]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 10000)},
            {1, IntervalValue(1, 10000)},
            {2, IntervalValue(1, 1)}
        };
    }

testRelExeState3_4()

void SymblicAbstractionTest::testRelExeState3_4 ( )

inline

Definition at line 516 of file ae.cpp.

    {
        outs() << "test3_4 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [1, 100000];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(1, 100000);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 / var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") / getContext().int_const("0");
        itv[2] = itv[1].getInterval() / itv[0].getInterval();
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        AbstractState resRSY = RSY_time(inv, phi, rs);
        AbstractState resBilateral = Bilateral_time(inv, phi, rs);
        AbstractState resBS = BS_time(inv, phi, rs);
        // 0:[1,100000] 1:[1,100000] 2:[1,1]
        assert(resRSY == resBS && resBS == resBilateral && "inconsistency occurs");
        for (auto r : resRSY.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(1, 100000)},
            {1, IntervalValue(1, 100000)},
            {2, IntervalValue(1, 1)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testRelExeState4_1()

void SymblicAbstractionTest::testRelExeState4_1 ( )

inline

Definition at line 558 of file ae.cpp.

    {
        outs() << "test4_1 start\n";
        AbstractState itv;
        RelExeState relation;
        // var0 := [0, 10];
        relation[0] = getContext().int_const("0");
        itv[0] = IntervalValue(0, 10);
        // var1 := var0;
        relation[1] =
            getContext().int_const("1") == getContext().int_const("0");
        itv[1] = itv[0];
        // var2 := var1 / var0;
        relation[2] = getContext().int_const("2") ==
                      getContext().int_const("1") / getContext().int_const("0");
        itv[2] = itv[1].getInterval() / itv[0].getInterval();
        // Test extract sub vars
        Set<u32_t> res;
        relation.extractSubVars(relation[2], res);
        assert(res == Set<u32_t>({0, 1, 2}) && "inconsistency occurs");
        AbstractState inv = itv.sliceState(res);
        RelationSolver rs;
        const Z3Expr& relExpr = relation[2] && relation[1];
        const Z3Expr& initExpr = rs.gamma_hat(inv);
        const Z3Expr& phi = (relExpr && initExpr).simplify();
        // IntervalExeState resRSY = rs.RSY(inv, phi);
        outs() << "rsy done\n";
        // IntervalExeState resBilateral = rs.bilateral(inv, phi);
        outs() << "bilateral done\n";
        AbstractState resBS = rs.BS(inv, phi);
        outs() << "bs done\n";
        // 0:[0,10] 1:[0,10] 2:[-00,+00]
        // assert(resRSY == resBS && resBS == resBilateral);
        for (auto r : resBS.getVarToVal())
        {
            outs() << r.first << " " << r.second.getInterval() << "\n";
        }
        // ground truth
        AbstractState::VarToAbsValMap intendedRes = {{0, IntervalValue(0, 10)},
            {1, IntervalValue(0, 10)},
            {2, IntervalValue(0, 10)}
        };
        assert(AbstractState::eqVarToValMap(resBS.getVarToVal(), intendedRes) && "inconsistency occurs");
    }

testsValidation()

void SymblicAbstractionTest::testsValidation ( )

inline

top

Definition at line 603 of file ae.cpp.

    {
        SymblicAbstractionTest saTest;
        saTest.testRelExeState1_1();
        saTest.testRelExeState1_2();
 
        saTest.testRelExeState2_1();
        saTest.testRelExeState2_2();
        saTest.testRelExeState2_3();
        //        saTest.testRelExeState2_4(); /// 10000
        //        saTest.testRelExeState2_5(); /// 100000
 
        saTest.testRelExeState3_1();
        saTest.testRelExeState3_2();
        //        saTest.testRelExeState3_3(); /// 10000
        //        saTest.testRelExeState3_4(); /// 100000
 
        outs() << "start top\n";
        saTest.testRelExeState4_1(); 
    }

---

The documentation for this class was generated from the following file:

• /home/runner/work/SVF/SVF/svf-llvm/tools/AE/ae.cpp