Skip to content

Commit 21f425f

Browse files
lperronlperron
committed
more work on CP-SAT python; lots of fixes for bugs found by fuzzer
1 parent c7d7f5d commit 21f425f

23 files changed

+1193
-918
lines changed

‎ortools/sat/cp_model_expand.cc‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -652,10 +652,14 @@ void ExpandInverse(ConstraintProto* ct, PresolveContext* context) {
652652
const int r_j = f_inverse[j];
653653
int r_j_i;
654654
if (context->HasVarValueEncoding(r_j, i, &r_j_i)) {
655-
context->InsertVarValueEncoding(r_j_i, f_i, j);
655+
if (!context->InsertVarValueEncoding(r_j_i, f_i, j)) {
656+
return;
657+
}
656658
} else {
657659
const int f_i_j = context->GetOrCreateVarValueEncoding(f_i, j);
658-
context->InsertVarValueEncoding(f_i_j, r_j, i);
660+
if (!context->InsertVarValueEncoding(f_i_j, r_j, i)) {
661+
return;
662+
}
659663
}
660664
}
661665
}

‎ortools/sat/cp_model_presolve.cc‎

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1806,9 +1806,19 @@ bool CpModelPresolver::PresolveIntProd(ConstraintProto* ct) {
18061806
linear_for_true);
18071807
context_->CanonicalizeLinearConstraint(constraint_for_false);
18081808
context_->CanonicalizeLinearConstraint(constraint_for_true);
1809-
context_->UpdateRuleStats("int_prod: boolean affine term");
1810-
context_->UpdateNewConstraintsVariableUsage();
1811-
return RemoveConstraint(ct);
1809+
if (PossibleIntegerOverflow(*context_->working_model,
1810+
linear_for_false->vars(),
1811+
linear_for_false->coeffs()) ||
1812+
PossibleIntegerOverflow(*context_->working_model,
1813+
linear_for_true->vars(),
1814+
linear_for_true->coeffs())) {
1815+
context_->working_model->mutable_constraints()->RemoveLast();
1816+
context_->working_model->mutable_constraints()->RemoveLast();
1817+
} else {
1818+
context_->UpdateRuleStats("int_prod: boolean affine term");
1819+
context_->UpdateNewConstraintsVariableUsage();
1820+
return RemoveConstraint(ct);
1821+
}
18121822
}
18131823
}
18141824

@@ -13388,7 +13398,7 @@ bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model,
1338813398
}
1338913399

1339013400
bool ImportModelAndDomainsWithBasicPresolveIntoContext(
13391-
const CpModelProto& in_model, const std::vector<Domain>& domains,
13401+
const CpModelProto& in_model, absl::Span<const Domain> domains,
1339213402
std::function<bool(int)> active_constraints, PresolveContext* context) {
1339313403
CHECK_EQ(domains.size(), in_model.variables_size());
1339413404
ModelCopy copier(context);

‎ortools/sat/cp_model_presolve.h‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -498,7 +498,7 @@ bool ImportModelWithBasicPresolveIntoContext(const CpModelProto& in_model,
498498
// Same as ImportModelWithBasicPresolveIntoContext() except that variable
499499
// domains are read from domains.
500500
bool ImportModelAndDomainsWithBasicPresolveIntoContext(
501-
const CpModelProto& in_model, const std::vector<Domain>& domains,
501+
const CpModelProto& in_model, absl::Span<const Domain> domains,
502502
std::function<bool(int)> active_constraints, PresolveContext* context);
503503

504504
// Copies the non constraint, non variables part of the model.

‎ortools/sat/cp_model_solver_fuzz.cc‎

Lines changed: 127 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ namespace operations_research::sat {
3232

3333
namespace {
3434

35+
static constexpr int kMaxNumVars = 200;
36+
3537
std::string GetTestDataDir() {
3638
return file::JoinPathRespectAbsolute(::testing::SrcDir(),
3739
"_main/ortools/sat/fuzz_testdata");
@@ -83,15 +85,12 @@ void Solve(const CpModelProto& proto) {
8385
<< "Presolve should not change feasibility";
8486
}
8587

86-
fuzztest::Domain<IntegerVariableProto> CpVariableDomain() {
87-
fuzztest::Domain<int64_t> bound_domain =
88-
fuzztest::InRange<int64_t>(-std::numeric_limits<int64_t>::max() / 2,
89-
std::numeric_limits<int64_t>::max() / 2);
88+
fuzztest::Domain<IntegerVariableProto> CpVariableDomain(int64_t min,
89+
int64_t max) {
90+
fuzztest::Domain<int64_t> bound_domain = fuzztest::InRange<int64_t>(min, max);
9091
fuzztest::Domain<std::pair<int64_t, int64_t>> complex_domain_gap_and_size =
91-
fuzztest::PairOf(fuzztest::InRange<int64_t>(
92-
1, std::numeric_limits<int64_t>::max() / 2),
93-
fuzztest::InRange<int64_t>(
94-
0, std::numeric_limits<int64_t>::max() / 2));
92+
fuzztest::PairOf(fuzztest::InRange<int64_t>(1, max),
93+
fuzztest::InRange<int64_t>(0, max));
9594
fuzztest::Domain<IntegerVariableProto> var_domain = fuzztest::ReversibleMap(
9695
[](int64_t bound1, int64_t bound2,
9796
std::vector<std::pair<int64_t, int64_t>> complex_domain_segments) {
@@ -129,9 +128,8 @@ fuzztest::Domain<IntegerVariableProto> CpVariableDomain() {
129128
fuzztest::VectorOf(complex_domain_gap_and_size));
130129

131130
return fuzztest::Filter(
132-
[](IntegerVariableProto var) {
133-
return var.domain(var.domain().size() - 1) <=
134-
std::numeric_limits<int64_t>::max() / 2;
131+
[max](IntegerVariableProto var) {
132+
return var.domain(var.domain().size() - 1) <= max;
135133
},
136134
var_domain);
137135
}
@@ -147,7 +145,107 @@ ModelProtoVariablesDomain() {
147145
}
148146
return ValidateCpModel(model).empty();
149147
},
150-
fuzztest::VectorOf(CpVariableDomain()));
148+
fuzztest::VectorOf(
149+
CpVariableDomain(-std::numeric_limits<int64_t>::max() / 2,
150+
std::numeric_limits<int64_t>::max() / 2))
151+
.WithMaxSize(kMaxNumVars));
152+
}
153+
154+
fuzztest::Domain<LinearExpressionProto> LinearExprDomain() {
155+
fuzztest::Domain<int64_t> offset_domain =
156+
fuzztest::InRange<int64_t>(-std::numeric_limits<int64_t>::max() / 2,
157+
std::numeric_limits<int64_t>::max() / 2);
158+
fuzztest::Domain<std::pair<int64_t, int64_t>> variable_and_coefficient =
159+
fuzztest::PairOf(
160+
fuzztest::InRange<int64_t>(0, kMaxNumVars - 1),
161+
fuzztest::InRange<int64_t>(-std::numeric_limits<int64_t>::max() / 2,
162+
std::numeric_limits<int64_t>::max() / 2));
163+
return fuzztest::ReversibleMap(
164+
[](int64_t offset,
165+
std::vector<std::pair<int64_t, int64_t>> variable_and_coefficient) {
166+
LinearExpressionProto expr;
167+
for (const auto& [var, coeff] : variable_and_coefficient) {
168+
expr.add_vars(var);
169+
expr.add_coeffs(coeff);
170+
}
171+
expr.set_offset(offset);
172+
return expr;
173+
},
174+
[](LinearExpressionProto expr) {
175+
using Type =
176+
std::tuple<int64_t, std::vector<std::pair<int64_t, int64_t>>>;
177+
Type expr_inputs;
178+
expr_inputs = {expr.offset(), {}};
179+
std::vector<std::pair<int64_t, int64_t>>& variable_and_coefficient =
180+
std::get<1>(expr_inputs);
181+
if (expr.vars_size() != expr.coeffs_size()) {
182+
return std::optional<Type>();
183+
}
184+
for (int i = 0; i < expr.vars_size(); ++i) {
185+
variable_and_coefficient.push_back({expr.vars(i), expr.coeffs(i)});
186+
}
187+
return std::optional<Type>(expr_inputs);
188+
},
189+
offset_domain, fuzztest::VectorOf(variable_and_coefficient));
190+
}
191+
192+
fuzztest::Domain<LinearConstraintProto> LinearConstraintDomain() {
193+
fuzztest::Domain<std::pair<int64_t, int64_t>> variable_and_coefficient =
194+
fuzztest::PairOf(
195+
fuzztest::InRange<int64_t>(0, kMaxNumVars - 1),
196+
fuzztest::InRange<int64_t>(-std::numeric_limits<int64_t>::max() / 2,
197+
std::numeric_limits<int64_t>::max() / 2));
198+
return fuzztest::ReversibleMap(
199+
[](IntegerVariableProto domain,
200+
std::vector<std::pair<int64_t, int64_t>> variable_and_coefficient) {
201+
LinearConstraintProto constraint;
202+
for (const auto& [var, coeff] : variable_and_coefficient) {
203+
constraint.add_vars(var);
204+
constraint.add_coeffs(coeff);
205+
}
206+
*constraint.mutable_domain() = domain.domain();
207+
return constraint;
208+
},
209+
[](LinearConstraintProto constraint) {
210+
using Type = std::tuple<IntegerVariableProto,
211+
std::vector<std::pair<int64_t, int64_t>>>;
212+
Type constraint_inputs = {IntegerVariableProto(), {}};
213+
*std::get<0>(constraint_inputs).mutable_domain() = constraint.domain();
214+
std::vector<std::pair<int64_t, int64_t>>& variable_and_coefficient =
215+
std::get<1>(constraint_inputs);
216+
if (constraint.vars_size() != constraint.coeffs_size() ||
217+
constraint.vars().empty()) {
218+
return std::optional<Type>();
219+
}
220+
for (int i = 0; i < constraint.vars_size(); ++i) {
221+
variable_and_coefficient.push_back(
222+
{constraint.vars(i), constraint.coeffs(i)});
223+
}
224+
return std::optional<Type>(constraint_inputs);
225+
},
226+
CpVariableDomain(std::numeric_limits<int64_t>::min(),
227+
std::numeric_limits<int64_t>::max()),
228+
fuzztest::VectorOf(variable_and_coefficient));
229+
}
230+
231+
fuzztest::Domain<IntervalConstraintProto> IntervalConstraintDomain() {
232+
return fuzztest::Arbitrary<IntervalConstraintProto>()
233+
.WithProtobufField("start", LinearExprDomain())
234+
.WithProtobufField("end", LinearExprDomain())
235+
.WithProtobufField("size", LinearExprDomain());
236+
}
237+
238+
fuzztest::Domain<LinearArgumentProto> LinearArgumentDomain() {
239+
return fuzztest::Arbitrary<LinearArgumentProto>()
240+
.WithProtobufField("target", LinearExprDomain())
241+
.WithRepeatedProtobufField("exprs",
242+
fuzztest::VectorOf(LinearExprDomain()));
243+
}
244+
245+
fuzztest::Domain<BoolArgumentProto> BoolArgumentDomain() {
246+
return fuzztest::Arbitrary<BoolArgumentProto>().WithRepeatedInt32Field(
247+
"literals", fuzztest::VectorOf(fuzztest::InRange<int32_t>(
248+
-kMaxNumVars, kMaxNumVars - 1)));
151249
}
152250

153251
// Fuzzing repeats solve() 100 times, and timeout after 600s.
@@ -158,10 +256,23 @@ FUZZ_TEST(CpModelProtoFuzzer, Solve)
158256
.WithRepeatedProtobufField("variables", ModelProtoVariablesDomain())
159257
.WithRepeatedProtobufField(
160258
"constraints",
161-
fuzztest::VectorOf(fuzztest::Arbitrary<ConstraintProto>()
162-
.WithOneofAlwaysSet("constraint")
163-
.WithFieldUnset("name")
164-
.WithFieldUnset("dummy_constraint")))
259+
fuzztest::VectorOf(
260+
fuzztest::Arbitrary<ConstraintProto>()
261+
.WithOneofAlwaysSet("constraint")
262+
.WithFieldUnset("name")
263+
.WithFieldUnset("dummy_constraint")
264+
.WithProtobufField("bool_or", BoolArgumentDomain())
265+
.WithProtobufField("bool_and", BoolArgumentDomain())
266+
.WithProtobufField("at_most_one", BoolArgumentDomain())
267+
.WithProtobufField("exactly_one", BoolArgumentDomain())
268+
.WithProtobufField("bool_xor", BoolArgumentDomain())
269+
.WithProtobufField("int_div", LinearArgumentDomain())
270+
.WithProtobufField("int_mod", LinearArgumentDomain())
271+
.WithProtobufField("int_prod", LinearArgumentDomain())
272+
.WithProtobufField("lin_max", LinearArgumentDomain())
273+
.WithProtobufField("linear", LinearConstraintDomain())
274+
.WithProtobufField("interval",
275+
IntervalConstraintDomain())))
165276
.WithFieldUnset("name")
166277
.WithFieldUnset("symmetry")
167278
.WithProtobufField("objective",

0 commit comments

Comments
 (0)