extend State::isImplied to take context into account

cf AliveToolkit#1149

Author: nunoplopes

ir/memory.cpp

@@ -1028,7 +1028,7 @@ Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, const expr &bytes,
     expr offset   = p.getOffset();
     uint64_t bid;
     if (shortbid.isUInt(bid) &&
-        (!isAsmMode() || state->isImplied(p.isInbounds(true)))) {
+        (!isAsmMode() || state->isImplied(p.isInbounds(true), true))) {
       if (!is_local.isFalse() && bid < sz_local)
         check_alias(this_alias, true, bid, offset);
       if (!is_local.isTrue() && bid < sz_nonlocal)

ir/pointer.cpp

@@ -651,7 +651,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
     expr is_log = ptr.isLogical();
     expr inbounds = is_asm ? ptr.isInbounds(true) : expr(true);
 
-    if (is_asm && !inbounds.isTrue() && m.state->isImplied(inbounds))
+    if (is_asm && !inbounds.isTrue() && m.state->isImplied(inbounds, domain))
       inbounds = true;
 
     optional<expr> log_expr, phy_expr;

ir/state.cpp

@@ -1376,12 +1376,13 @@ void State::finishInitializer() {
   }
 }
 
-bool State::isImplied(const expr &e) {
+bool State::isImplied(const expr &e, const expr &e_domain) {
   if (domain.UB.contains(e))
     return true;
 
-  if (check_expr(domain().notImplies(e), "UB inference", true).isUnsat()) {
-    domain.UB.add(e);
+  if (check_expr((e_domain && domain()).notImplies(e), "UB inference", true)
+        .isUnsat()) {
+    domain.UB.add(e_domain.implies(e));
     return true;
   }
   return false;

ir/state.h

@@ -335,7 +335,7 @@ class State {
   bool isInitializationPhase() const { return is_initialization_phase; }
   void finishInitializer();
 
-  bool isImplied(const smt::expr &e);
+  bool isImplied(const smt::expr &e, const smt::expr &domain);
 
   auto& getFn() const { return f; }
   auto& getMemory() const { return memory; }