@@ -265,11 +265,17 @@ std::optional<Constraint> approximateOrTermEqualPair(const Abstract::Op aOp,
265265 if (aOp == Eq && bOp == GtS) {
266266 return Constraint{GeS, term};
267267 }
268+ if (aOp == Eq && bOp == GtU) {
269+ return Constraint{GeU, term};
270+ }
268271
269272 // x > C || x >= C === x >= C
270273 if (aOp == GtS && bOp == GeS) {
271274 return Constraint{GeS, term};
272275 }
276+ if (aOp == GtU && bOp == GeU) {
277+ return Constraint{GeU, term};
278+ }
273279
274280 // TODO: all the rest
275281
@@ -286,11 +292,17 @@ std::optional<Constraint> approximateOrAdjacentConstantPair(
286292 if (aOp == Eq && bOp == GeS && !aConstant.isSignedMax ()) {
287293 return Constraint{GeS, {aConstant}};
288294 }
295+ if (aOp == Eq && bOp == GeU && !aConstant.isUnsignedMax ()) {
296+ return Constraint{GeU, {aConstant}};
297+ }
289298
290299 // x > C || x >= C+1 === x > C, if C+1 does not overflow.
291300 if (aOp == GtS && bOp == GeS && !aConstant.isSignedMax ()) {
292301 return Constraint{GtS, {aConstant}};
293302 }
303+ if (aOp == GtU && bOp == GeU && !aConstant.isUnsignedMax ()) {
304+ return Constraint{GtU, {aConstant}};
305+ }
294306
295307 // TODO: all the rest
296308
@@ -494,15 +506,110 @@ void LocalConstraint::flip() {
494506}
495507
496508void BasicBlockConstraintMap::set (Index index, const Constraint& c) {
509+ set (index, AndedConstraintSet{c});
510+ }
511+
512+ void BasicBlockConstraintMap::set (Index index,
513+ const AndedConstraintSet& constraints) {
497514 // We should not set values in unreachable code.
498515 assert (!unreachable);
499516
500517 // Clear the old state.
501518 eraseStaleRefs (index);
502519 map.erase (index);
503520
504- // Apply the constraint.
505- approximateAnd (index, c);
521+ // Apply the constraints, if there are any.
522+ if (constraints.provesNothing ()) {
523+ setProvesNothing (index);
524+ } else {
525+ for (auto & c : constraints) {
526+ approximateAnd (index, c);
527+ }
528+ }
529+ }
530+
531+ void BasicBlockConstraintMap::set (Index index, Expression* value) {
532+ using namespace Match ;
533+ using namespace Abstract ;
534+
535+ // Apply a constraint to a value, x = C.
536+ if (Properties::isSingleConstantExpression (value)) {
537+ auto c = Properties::getLiteral (value);
538+ set (index, Constraint{Abstract::Eq, {c}});
539+ return ;
540+ }
541+
542+ // Apply a constraint to a local, x = y.
543+ if (auto * get = value->dynCast <LocalGet>()) {
544+ set (index, Constraint{Abstract::Eq, {get->index }});
545+ return ;
546+ }
547+
548+ // Apply an increment of a local, x = y + 1.
549+ Index y;
550+ if (matches (value, binary (Abstract::Add, local (&y), ival (1 )))) {
551+ // The local y must have old constraints that we know how to increment.
552+ auto old = get (y);
553+
554+ // Iterate over the old constraints and increment each one.
555+ auto success = true ;
556+ for (auto & c : old) {
557+ auto * N = std::get_if<Literal>(&c.term );
558+ if (!N) {
559+ // A non-constant term, which we don't know how to increment.
560+ success = false ;
561+ break ;
562+ }
563+
564+ switch (c.op ) {
565+ // x == N, x++ => x == N+1.
566+ case Eq:
567+ *N = N->add (Literal::makeFromInt32 (1 , N->type ));
568+ continue ;
569+ // x >= N, x++ => x > N
570+ case GeS:
571+ c.op = GtS;
572+ continue ;
573+ case GeU:
574+ c.op = GtU;
575+ continue ;
576+ // x < N, x++ => x <= N
577+ case LtS:
578+ c.op = LeS;
579+ continue ;
580+ case LtU:
581+ c.op = LeU;
582+ continue ;
583+ // x <= N, x++ => x <= N+1 if no overflow
584+ case LeS:
585+ if (N->isSignedMax ()) {
586+ success = false ;
587+ break ;
588+ }
589+ *N = N->add (Literal::makeFromInt32 (1 , N->type ));
590+ continue ;
591+ case LeU:
592+ if (N->isUnsignedMax ()) {
593+ success = false ;
594+ break ;
595+ }
596+ *N = N->add (Literal::makeFromInt32 (1 , N->type ));
597+ continue ;
598+ default :
599+ // Something we don't recognize.
600+ success = false ;
601+ break ;
602+ }
603+ }
604+
605+ if (success) {
606+ set (index, old);
607+ return ;
608+ }
609+ }
610+
611+ // We know and can prove nothing.
612+ setProvesNothing (index);
506613}
507614
508615void BasicBlockConstraintMap::setProvesNothing (Index index) {
0 commit comments