Skip to content

Commit

Permalink
Tweaks and fixes while bringing (back) up vsc-solvers
Browse files Browse the repository at this point in the history 
Signed-off-by: Matthew Ballance <matt.ballance@gmail.com>
  • Loading branch information
@mballance
mballance committed Mar 8, 2024
1 parent 8b68733 commit 073a7a7
Show file tree
Hide file tree
Showing 6 changed files with 144 additions and 25 deletions.
36 changes: 36 additions & 0 deletions src/SolverBoolectorConstraintBuilder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
6 changes: 6 additions & 0 deletions src/SolverBoolectorConstraintBuilder.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
61 changes: 60 additions & 1 deletion src/TaskBuildSolveSets.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}

Expand All @@ -49,6 +50,7 @@ TaskBuildSolveSets::~TaskBuildSolveSets() {
void TaskBuildSolveSets::build(
std::vector<ISolveSetUP> &solvesets,
RefPathSet &unconstrained) {
DEBUG_ENTER("build");
m_active_ss_idx = -1;
m_constraint_depth = 0;
m_unconstrained = &unconstrained;
Expand All @@ -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<ISolveSetUP>::const_iterator
it=solvesets.begin();
it!=solvesets.end(); it++) {
DEBUG("Solve Set:");
const RefPathMap<SolveSetFieldType> &paths = (*it)->getFields();
RefPathMap<SolveSetFieldType>::iterator fi = paths.begin();
while (fi.next()) {
const std::vector<int32_t> &path = fi.path();
DEBUG("Path:");
for (std::vector<int32_t>::const_iterator
pi=path.begin();
pi!=path.end(); pi++) {
DEBUG(" %d", *pi);
}
}
}
}

DEBUG_LEAVE("build");
}

void TaskBuildSolveSets::visitTypeConstraintExpr(dm::ITypeConstraintExpr *c) {
Expand Down Expand Up @@ -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();
Expand Down
7 changes: 7 additions & 0 deletions src/TaskBuildSolveSets.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -89,6 +95,7 @@ class TaskBuildSolveSets : public virtual dm::VisitorBase {
const RefPathSet &m_include_constraints;
const RefPathSet &m_exclude_constraints;
std::vector<dm::ITypeField *> m_field_s;
int32_t m_ref_depth;
RefPathField m_field_path;
std::vector<int32_t> m_constraint_path;

Expand Down
6 changes: 4 additions & 2 deletions tests/src/TestBuildSolveSets.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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"
Expand Down
53 changes: 31 additions & 22 deletions tests/src/TestConstraintsLinear.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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);
Expand All @@ -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(),
Expand All @@ -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());
}
}

Expand Down Expand Up @@ -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());
}
}

Expand Down Expand Up @@ -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());
}
}
}

Expand Down

0 comments on commit 073a7a7

Please sign in to comment.