diff --git a/src/SolverBoolectorConstraintBuilder.cpp b/src/SolverBoolectorConstraintBuilder.cpp index 2fc0bec..cb2eabf 100644 --- a/src/SolverBoolectorConstraintBuilder.cpp +++ b/src/SolverBoolectorConstraintBuilder.cpp @@ -327,6 +327,42 @@ void SolverBoolectorConstraintBuilder::visitTypeExprBin(dm::ITypeExprBin *e) { DEBUG_LEAVE("visitTypeExprBin"); } +void SolverBoolectorConstraintBuilder::visitTypeExprRefBottomUp(dm::ITypeExprRefBottomUp *e) { + DEBUG_ENTER("visitTypeExprRefBottomUp"); + + DEBUG_LEAVE("visitTypeExprRefBottomUp"); +} + +void SolverBoolectorConstraintBuilder::visitTypeExprRefPath(dm::ITypeExprRefPath *e) { + DEBUG_ENTER("visitTypeExprRefPath"); + int32_t prefix_sz = m_path_prefix.size(); + e->getTarget()->accept(m_this); + + m_path_prefix.insert( + m_path_prefix.end(), + e->getPath().begin(), + e->getPath().end() + ); + + m_expr.first = m_field_m.find(m_path_prefix); + + DEBUG("node @ %s: %p", RefPathField(m_path_prefix).toString().c_str(), m_expr.first); + + DataTypeMode dt_mode = m_dt_mode; + m_dt_mode = DataTypeMode::RefSign; + TaskPath2Field(m_root_field).toField(m_path_prefix)->getDataType()->accept(m_this); + m_dt_mode = dt_mode; + + m_path_prefix.resize(prefix_sz); + DEBUG_LEAVE("visitTypeExprRefPath"); +} + +void SolverBoolectorConstraintBuilder::visitTypeExprRefTopDown(dm::ITypeExprRefTopDown *e) { + DEBUG_ENTER("visitTypeExprRefTopDown"); + + DEBUG_LEAVE("visitTypeExprRefTopDown"); +} + void SolverBoolectorConstraintBuilder::visitTypeExprFieldRef(dm::ITypeExprFieldRef *e) { #ifdef UNDEFINED DEBUG_ENTER("visitTypeExprFieldRef path.size=%d prefix=%s", diff --git a/src/SolverBoolectorConstraintBuilder.h b/src/SolverBoolectorConstraintBuilder.h index f7236b6..4995b09 100644 --- a/src/SolverBoolectorConstraintBuilder.h +++ b/src/SolverBoolectorConstraintBuilder.h @@ -66,6 +66,12 @@ class SolverBoolectorConstraintBuilder : public dm::VisitorBase { virtual void visitTypeExprBin(dm::ITypeExprBin *e) override; + virtual void visitTypeExprRefBottomUp(dm::ITypeExprRefBottomUp *e) override; + + virtual void visitTypeExprRefPath(dm::ITypeExprRefPath *e) override; + + virtual void visitTypeExprRefTopDown(dm::ITypeExprRefTopDown *e) override; + virtual void visitTypeExprFieldRef(dm::ITypeExprFieldRef *e) override; virtual void visitTypeExprRangelist(dm::ITypeExprRangelist *e) override; diff --git a/src/TaskBuildSolveSets.cpp b/src/TaskBuildSolveSets.cpp index b8fe5f4..0ab0ec4 100644 --- a/src/TaskBuildSolveSets.cpp +++ b/src/TaskBuildSolveSets.cpp @@ -38,7 +38,8 @@ TaskBuildSolveSets::TaskBuildSolveSets( ) : m_phase(0), m_root_field(root_field), m_target_fields(target_fields), m_fixed_fields(fixed_fields), m_include_constraints(include_constraints), - m_exclude_constraints(exclude_constraints) { + m_exclude_constraints(exclude_constraints), + m_ref_depth(0) { DEBUG_INIT("vsc::solvers::TaskBuildSolveSets", dmgr); } @@ -49,6 +50,7 @@ TaskBuildSolveSets::~TaskBuildSolveSets() { void TaskBuildSolveSets::build( std::vector &solvesets, RefPathSet &unconstrained) { + DEBUG_ENTER("build"); m_active_ss_idx = -1; m_constraint_depth = 0; m_unconstrained = &unconstrained; @@ -67,6 +69,29 @@ void TaskBuildSolveSets::build( solvesets.push_back(ISolveSetUP(it->release())); } } + + if (DEBUG_EN) { + DEBUG("Result: %d solve sets", solvesets.size()); + + for (std::vector::const_iterator + it=solvesets.begin(); + it!=solvesets.end(); it++) { + DEBUG("Solve Set:"); + const RefPathMap &paths = (*it)->getFields(); + RefPathMap::iterator fi = paths.begin(); + while (fi.next()) { + const std::vector &path = fi.path(); + DEBUG("Path:"); + for (std::vector::const_iterator + pi=path.begin(); + pi!=path.end(); pi++) { + DEBUG(" %d", *pi); + } + } + } + } + + DEBUG_LEAVE("build"); } void TaskBuildSolveSets::visitTypeConstraintExpr(dm::ITypeConstraintExpr *c) { @@ -178,6 +203,40 @@ void TaskBuildSolveSets::visitTypeExprBin(dm::ITypeExprBin *e) { DEBUG_LEAVE("visitTypeExprBin"); } +void TaskBuildSolveSets::visitTypeExprRefBottomUp(dm::ITypeExprRefBottomUp *e) { + DEBUG_ENTER("visitTypeExprRefBottomUp"); + + DEBUG_LEAVE("visitTypeExprRefBottomUp"); +} + +void TaskBuildSolveSets::visitTypeExprRefPath(dm::ITypeExprRefPath *e) { + DEBUG_ENTER("visitTypeExprRefPath"); + uint32_t sz = m_field_path.size(); + + m_ref_depth++; + e->getTarget()->accept(m_this); + m_ref_depth--; + + m_field_path.insert( + m_field_path.end(), + e->getPath().begin(), + e->getPath().end()); + + if (!m_ref_depth) { + processFieldRef(m_field_path); + } + + m_field_path.resize(sz); + + DEBUG_LEAVE("visitTypeExprRefPath"); +} + +void TaskBuildSolveSets::visitTypeExprRefTopDown(dm::ITypeExprRefTopDown *e) { + DEBUG_ENTER("visitTypeExprRefTopDown"); + + DEBUG_LEAVE("visitTypeExprRefTopDown"); +} + void TaskBuildSolveSets::visitTypeExprFieldRef(dm::ITypeExprFieldRef *e) { DEBUG_ENTER("visitTypeExprFieldRef"); uint32_t sz = m_field_path.size(); diff --git a/src/TaskBuildSolveSets.h b/src/TaskBuildSolveSets.h index 2aee6e6..671ade9 100644 --- a/src/TaskBuildSolveSets.h +++ b/src/TaskBuildSolveSets.h @@ -68,6 +68,12 @@ class TaskBuildSolveSets : public virtual dm::VisitorBase { virtual void visitTypeExprBin(dm::ITypeExprBin *e) override; + virtual void visitTypeExprRefBottomUp(dm::ITypeExprRefBottomUp *e) override; + + virtual void visitTypeExprRefPath(dm::ITypeExprRefPath *e) override; + + virtual void visitTypeExprRefTopDown(dm::ITypeExprRefTopDown *e) override; + virtual void visitTypeExprFieldRef(dm::ITypeExprFieldRef *e) override; virtual void visitTypeFieldPhy(dm::ITypeFieldPhy *f) override; @@ -89,6 +95,7 @@ class TaskBuildSolveSets : public virtual dm::VisitorBase { const RefPathSet &m_include_constraints; const RefPathSet &m_exclude_constraints; std::vector m_field_s; + int32_t m_ref_depth; RefPathField m_field_path; std::vector m_constraint_path; diff --git a/tests/src/TestBuildSolveSets.cpp b/tests/src/TestBuildSolveSets.cpp index 61e5cd3..2ff2db0 100644 --- a/tests/src/TestBuildSolveSets.cpp +++ b/tests/src/TestBuildSolveSets.cpp @@ -158,7 +158,8 @@ TEST_F(TestBuildSolveSets, nested_struct_local_constraints) { @vdc.randclass class MyC(object): - a : vdc.rand[MyI] + #a : vdc.rand[MyI] + pass )"); #include "TestBuildSolveSets_nested_struct_local_constraints.h" @@ -199,7 +200,8 @@ TEST_F(TestBuildSolveSets, nested_struct_local_constraints_nested_unconstrained) @vdc.randclass class MyC(object): - a : vdc.rand[MyI] + #a : vdc.rand[MyI] + pass )"); #include "TestBuildSolveSets_nested_struct_local_constraints_nested_unconstrained.h" diff --git a/tests/src/TestConstraintsLinear.cpp b/tests/src/TestConstraintsLinear.cpp index 5cfb4ca..671eafd 100644 --- a/tests/src/TestConstraintsLinear.cpp +++ b/tests/src/TestConstraintsLinear.cpp @@ -149,17 +149,19 @@ TEST_F(TestConstraintsLinear, struct_32bit_ne) { include_constraints, exclude_constraints, flags); - /* dm::ValRefStruct field_v(field->getImmVal()); - dm::ValRefInt val_a(field_v.getField(0)); - dm::ValRefInt val_b(field_v.getField(1)); - // ASSERT_LT(val_a.get_val_u(), val_b.get_val_u()); - */ + dm::ValRefInt val_a(field_v.getFieldRef(0)); + dm::ValRefInt val_b(field_v.getFieldRef(1)); + ASSERT_NE(val_a.get_val_u(), val_b.get_val_u()); } } TEST_F(TestConstraintsLinear, nested_struct_32bit_ne) { VSC_DATACLASSES(TestConstraintsLinear_nested_struct_32bit_ne, MyC, R"( + import logging + + logging.basicConfig(level=logging.DEBUG) + @vdc.randclass class MyI(object): a : vdc.rand_uint32_t @@ -181,7 +183,7 @@ TEST_F(TestConstraintsLinear, nested_struct_32bit_ne) { d : vdc.rand[MyI] )"); #include "TestConstraintsLinear_nested_struct_32bit_ne.h" - enableDebug(false); + enableDebug(true); fprintf(stdout, "MyC_t.name: %s\n", MyC_t->name().c_str()); fflush(stdout); @@ -194,7 +196,7 @@ TEST_F(TestConstraintsLinear, nested_struct_32bit_ne) { RefPathSet target_fields, fixed_fields, include_constraints, exclude_constraints; SolveFlags flags = SolveFlags::NoFlags; - for (uint32_t i=0; i<1000; i++) { + for (uint32_t i=0; i<1; i++) { solver->randomize( randstate.get(), field.get(), @@ -203,12 +205,15 @@ TEST_F(TestConstraintsLinear, nested_struct_32bit_ne) { include_constraints, exclude_constraints, flags); - /* dm::ValRefStruct field_v(field->getImmVal()); - dm::ValRefInt val_a(field_v.getField(0)); - dm::ValRefInt val_b(field_v.getField(1)); - // ASSERT_LT(val_a.get_val_u(), val_b.get_val_u()); - */ + dm::ValRefStruct field_a(field_v.getFieldRef(0)); + dm::ValRefInt val_a(field_a.getFieldRef(0)); + dm::ValRefInt val_b(field_a.getFieldRef(1)); + dm::ValRefInt val_c(field_a.getFieldRef(2)); + dm::ValRefInt val_d(field_a.getFieldRef(3)); + ASSERT_NE(val_a.get_val_u(), val_b.get_val_u()); + ASSERT_NE(val_b.get_val_u(), val_c.get_val_u()); + ASSERT_NE(val_c.get_val_u(), val_d.get_val_u()); } } @@ -254,12 +259,13 @@ TEST_F(TestConstraintsLinear, nested_struct_32bit_ne_single) { include_constraints, exclude_constraints, flags); - /* dm::ValRefStruct field_v(field->getImmVal()); - dm::ValRefInt val_a(field_v.getField(0)); - dm::ValRefInt val_b(field_v.getField(1)); - // ASSERT_LT(val_a.get_val_u(), val_b.get_val_u()); - */ + dm::ValRefStruct field_a(field_v.getFieldRef(0)); + dm::ValRefInt val_a(field_a.getFieldRef(0)); + dm::ValRefInt val_b(field_a.getFieldRef(1)); + dm::ValRefInt val_c(field_a.getFieldRef(2)); + ASSERT_NE(val_a.get_val_u(), val_b.get_val_u()); + ASSERT_NE(val_b.get_val_u(), val_c.get_val_u()); } } @@ -308,12 +314,15 @@ TEST_F(TestConstraintsLinear, nested_struct_32bit_4_subfield) { include_constraints, exclude_constraints, flags); - /* dm::ValRefStruct field_v(field->getImmVal()); - dm::ValRefInt val_a(field_v.getField(0)); - dm::ValRefInt val_b(field_v.getField(1)); - // ASSERT_LT(val_a.get_val_u(), val_b.get_val_u()); - */ + for (uint32_t si=0; si<4; si++) { + dm::ValRefStruct field_x(field_v.getFieldRef(si)); + dm::ValRefInt val_a(field_x.getFieldRef(0)); + dm::ValRefInt val_b(field_x.getFieldRef(1)); + dm::ValRefInt val_c(field_x.getFieldRef(2)); + ASSERT_NE(val_a.get_val_u(), val_b.get_val_u()); + ASSERT_NE(val_b.get_val_u(), val_c.get_val_u()); + } } }