Method mkInput

ir/value.cpp:214–271

}

StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
  if (auto agg = ty.getAsAggregateType()) {
    vector<StateValue> vals;
    for (unsigned i = 0, e = agg->numElementsConst(); i < e; ++i) {
      if (agg->isPadding(i))
        continue;
      auto name = getSMTName(child + i);
      vals.emplace_back(mkInput(s, agg->getChild(i), child + i));
    }
    return agg->aggregateVals(vals);
  }

  expr val;
  if (hasAttribute(ParamAttrs::ByVal)) {
    unsigned bid;
    expr size = expr::mkUInt(attrs.blockSize, bits_size_t);
    val = Pointer(s.getMemory(),
                  get_global(s, smt_name, &size, attrs.align, false, false,bid))
          .setAttrs(attrs)
          .setIsBasedOnArg()
          .release();
    bool is_const = hasAttribute(ParamAttrs::NoWrite) ||
                    !s.getFn().getFnAttrs().mem.canWrite(MemoryAccess::Args);
    s.getMemory().markByVal(bid, is_const);
  } else {
    auto name = getSMTName(child);
    val = ty.mkInput(s, name.c_str(), attrs);
  }

  auto undef_mask = getUndefVar(ty, child);
  if (config::disable_undef_input || attrs.poisonImpliesUB()) {
    s.addUB(undef_mask == 0);
  } else if (s.isAsmMode()) {
    // do nothing; there's no undef in assembly
  } else {
    auto [undef, var] = ty.mkUndefInput(s, attrs);
    if (undef_mask.bits() == 1)
      val = expr::mkIf(undef_mask == 0, val, undef);
    else
      val = (~undef_mask & val) | (undef_mask & undef);
    s.addUndefVar(std::move(var));
  }

  auto state_val = attrs.encode(s, {std::move(val), expr(true)}, ty, true);

  bool never_poison = config::disable_poison_input || attrs.poisonImpliesUB();
  expr np = expr::mkBoolVar(("np_" + getSMTName(child)).c_str());
  if (never_poison) {
    s.addUB(std::move(np));
  } else if (s.isAsmMode()) {
    // There's no poison in assembly
    state_val.non_poison = true;
  } else {
    state_val.non_poison &= np;
  }

  return state_val;
}