ExportSMTLIB.cpp Source File (original) (raw)

22 #include "llvm/ADT/ScopedHashTable.h"

23 #include "llvm/ADT/StringRef.h"

24 #include "llvm/Support/Format.h"

25 #include "llvm/Support/raw_ostream.h"

27 using namespace mlir;

28 using namespace smt;

30 using ValueMap = llvm::ScopedHashTable<mlir::Value, std::string>;

32 #define DEBUG_TYPE "export-smtlib"

34 namespace {

40 mlir::raw_indented_ostream &> {

44 stream << "Bool";

45 }

48 stream << "Int";

49 }

52 stream << "(_ BitVec " << type.getWidth() << ")";

53 }

56 stream << "(Array ";

57 dispatchSMTTypeVisitor(type.getDomainType(), stream);

58 stream << " ";

59 dispatchSMTTypeVisitor(type.getRangeType(), stream);

60 stream << ")";

61 }

64 stream << "(";

65 StringLiteral nextToken = "";

67 for (Type domainTy : type.getDomainTypes()) {

68 stream << nextToken;

69 dispatchSMTTypeVisitor(domainTy, stream);

70 nextToken = " ";

71 }

73 stream << ") ";

74 dispatchSMTTypeVisitor(type.getRangeType(), stream);

75 }

78 if (!type.getSortParams().empty())

79 stream << "(";

81 stream << type.getIdentifier().getValue();

82 for (Type paramTy : type.getSortParams()) {

83 stream << " ";

84 dispatchSMTTypeVisitor(paramTy, stream);

85 }

87 if (!type.getSortParams().empty())

88 stream << ")";

89 }

91 private:

94 };

98 struct VisitorInfo {

100 : stream(stream), valueMap(valueMap) {}

102 unsigned indentLevel, unsigned openParens)

103 : stream(stream), valueMap(valueMap), indentLevel(indentLevel),

104 openParens(openParens) {}

105

106

108

110

111 unsigned indentLevel = 0;

112

113 unsigned openParens = 0;

114 };

115

116

117

118 struct ExpressionVisitor

120 VisitorInfo &> {

121 using Base =

123 using Base::visitSMTOp;

124

127

128 LogicalResult dispatchSMTOpVisitor(Operation *op, VisitorInfo &info) {

130 "expression op must have exactly one result value");

131

132

133

134

135

136

137

138

141 std::string str;

142 llvm::raw_string_ostream sstream(str);

144

145 VisitorInfo newInfo(indentedStream, info.valueMap, info.indentLevel,

146 info.openParens);

147 if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))

148 return failure();

149

150 info.valueMap.insert(res, str);

151 return success();

152 }

153

154

155

156

157 auto name = names.newName("tmp");

158 info.valueMap.insert(res, name.str());

159 info.stream << "(let ((" << name << " ";

160

161 VisitorInfo newInfo(info.stream, info.valueMap,

162 info.indentLevel + 8 + name.size(), 0);

163 if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))

164 return failure();

165

166 info.stream << "))\n";

167

168 if (options.indentLetBody) {

169

170 info.indentLevel += 5;

171 }

172 ++info.openParens;

173 info.stream.indent(info.indentLevel);

174

175 return success();

176 }

177

178

179

180

181

182 template

183 LogicalResult printBinaryOp(Op op, StringRef name, VisitorInfo &info) {

184 info.stream << "(" << name << " " << info.valueMap.lookup(op.getLhs())

185 << " " << info.valueMap.lookup(op.getRhs()) << ")";

186 return success();

187 }

188

189 template

190 LogicalResult printVariadicOp(Op op, StringRef name, VisitorInfo &info) {

191 info.stream << "(" << name;

193 info.stream << " " << info.valueMap.lookup(val);

194 info.stream << ")";

195 return success();

196 }

197

198 LogicalResult visitSMTOp(BVNegOp op, VisitorInfo &info) {

199 info.stream << "(bvneg " << info.valueMap.lookup(op.getInput()) << ")";

200 return success();

201 }

202

203 LogicalResult visitSMTOp(BVNotOp op, VisitorInfo &info) {

204 info.stream << "(bvnot " << info.valueMap.lookup(op.getInput()) << ")";

205 return success();

206 }

207

208 #define HANDLE_OP(OPTYPE, NAME, KIND) \

209 LogicalResult visitSMTOp(OPTYPE op, VisitorInfo &info) { \

210 return print##KIND##Op(op, NAME, info); \

211 }

212

213 HANDLE_OP(BVAddOp, "bvadd", Binary);

214 HANDLE_OP(BVMulOp, "bvmul", Binary);

215 HANDLE_OP(BVURemOp, "bvurem", Binary);

216 HANDLE_OP(BVSRemOp, "bvsrem", Binary);

217 HANDLE_OP(BVSModOp, "bvsmod", Binary);

218 HANDLE_OP(BVShlOp, "bvshl", Binary);

219 HANDLE_OP(BVLShrOp, "bvlshr", Binary);

220 HANDLE_OP(BVAShrOp, "bvashr", Binary);

221 HANDLE_OP(BVUDivOp, "bvudiv", Binary);

222 HANDLE_OP(BVSDivOp, "bvsdiv", Binary);

223 HANDLE_OP(BVAndOp, "bvand", Binary);

224 HANDLE_OP(BVOrOp, "bvor", Binary);

225 HANDLE_OP(BVXOrOp, "bvxor", Binary);

226 HANDLE_OP(ConcatOp, "concat", Binary);

227

228 LogicalResult visitSMTOp(ExtractOp op, VisitorInfo &info) {

229 info.stream << "((_ extract "

230 << (op.getLowBit() + op.getType().getWidth() - 1) << " "

231 << op.getLowBit() << ") " << info.valueMap.lookup(op.getInput())

232 << ")";

233 return success();

234 }

235

236 LogicalResult visitSMTOp(RepeatOp op, VisitorInfo &info) {

237 info.stream << "((_ repeat " << op.getCount() << ") "

238 << info.valueMap.lookup(op.getInput()) << ")";

239 return success();

240 }

241

242 LogicalResult visitSMTOp(BVCmpOp op, VisitorInfo &info) {

243 return printBinaryOp(op, "bv" + stringifyBVCmpPredicate(op.getPred()).str(),

244 info);

245 }

246

247

248

249

250

253 HANDLE_OP(IntSubOp, "-", Binary);

254 HANDLE_OP(IntDivOp, "div", Binary);

255 HANDLE_OP(IntModOp, "mod", Binary);

256

257 LogicalResult visitSMTOp(IntCmpOp op, VisitorInfo &info) {

258 switch (op.getPred()) {

259 case IntPredicate::ge:

260 return printBinaryOp(op, ">=", info);

261 case IntPredicate::le:

262 return printBinaryOp(op, "<=", info);

263 case IntPredicate::gt:

264 return printBinaryOp(op, ">", info);

265 case IntPredicate::lt:

266 return printBinaryOp(op, "<", info);

267 }

268 return failure();

269 }

270

271

272

273

274

277

278 LogicalResult visitSMTOp(IteOp op, VisitorInfo &info) {

279 info.stream << "(ite " << info.valueMap.lookup(op.getCond()) << " "

280 << info.valueMap.lookup(op.getThenValue()) << " "

281 << info.valueMap.lookup(op.getElseValue()) << ")";

282 return success();

283 }

284

285 LogicalResult visitSMTOp(ApplyFuncOp op, VisitorInfo &info) {

286 info.stream << "(" << info.valueMap.lookup(op.getFunc());

287 for (Value arg : op.getArgs())

288 info.stream << " " << info.valueMap.lookup(arg);

289 info.stream << ")";

290 return success();

291 }

292

293 template

294 LogicalResult quantifierHelper(OpTy op, StringRef operatorString,

295 VisitorInfo &info) {

296 auto weight = op.getWeight();

297 auto patterns = op.getPatterns();

298

299 if (op.getNoPattern())

300 return op.emitError() << "no-pattern attribute not supported yet";

301

302 llvm::ScopedHashTableScope<Value, std::string> scope(info.valueMap);

303 info.stream << "(" << operatorString << " (";

304 StringLiteral delimiter = "";

305

307

308 for (auto [i, arg] : llvm::enumerate(op.getBody().getArguments())) {

309

310 StringRef prefix =

311 op.getBoundVarNames()

312 ? cast(op.getBoundVarNames()->getValue()[i])

313 .getValue()

314 : "tmp";

315 StringRef name = names.newName(prefix);

316 argNames.push_back(name);

317

318 info.valueMap.insert(arg, name.str());

319

320

321 info.stream << delimiter << "(" << name << " ";

322 typeVisitor.dispatchSMTTypeVisitor(arg.getType(), info.stream);

323 info.stream << ")";

324 delimiter = " ";

325 }

326

327 info.stream << ")\n";

328

329

330

331

333 Value yieldedValue = op.getBody().front().getTerminator()->getOperand(0);

334 worklist.push_back(yieldedValue);

335 unsigned indentExt = operatorString.size() + 2;

336 VisitorInfo newInfo(info.stream, info.valueMap,

337 info.indentLevel + indentExt, 0);

338 if (weight != 0 || patterns .empty())

339 newInfo.stream.indent(newInfo.indentLevel);

340 else

341 newInfo.stream.indent(info.indentLevel);

342

343 if (weight != 0 || patterns .empty())

344 info.stream << "( ! ";

345

346 if (failed(printExpression(worklist, newInfo)))

347 return failure();

348

349 info.stream << info.valueMap.lookup(yieldedValue);

350

351 for (unsigned j = 0; j < newInfo.openParens; ++j)

352 info.stream << ")";

353

354 if (weight != 0)

355 info.stream << " :weight " << weight;

357 bool first = true;

358 info.stream << "\n:pattern (";

360

361 if (!first)

362 info.stream << " ";

363

364

366 info.valueMap.insert(arg, argNames[i].str());

367

369

370

371 for (auto yieldedValue : p.front().getTerminator()->getOperands()) {

372

373 worklist.push_back(yieldedValue);

374 unsigned indentExt = operatorString.size() + 2;

375

376 VisitorInfo newInfo2(info.stream, info.valueMap,

377 info.indentLevel + indentExt, 0);

378

379 info.stream.indent(0);

380

381 if (failed(printExpression(worklist, newInfo2)))

382 return failure();

383

384 info.stream << info.valueMap.lookup(yieldedValue);

385 for (unsigned j = 0; j < newInfo2.openParens; ++j)

386 info.stream << ")";

387 }

388

389 first = false;

390 }

391 info.stream << ")";

392 }

393

394 if (weight != 0 || patterns .empty())

395 info.stream << ")";

396

397 info.stream << ")";

398

399 return success();

400 }

401

402 LogicalResult visitSMTOp(ForallOp op, VisitorInfo &info) {

403 return quantifierHelper(op, "forall", info);

404 }

405

406 LogicalResult visitSMTOp(ExistsOp op, VisitorInfo &info) {

407 return quantifierHelper(op, "exists", info);

408 }

409

410 LogicalResult visitSMTOp(NotOp op, VisitorInfo &info) {

411 info.stream << "(not " << info.valueMap.lookup(op.getInput()) << ")";

412 return success();

413 }

414

418 HANDLE_OP(ImpliesOp, "=>", Binary);

419

420

421

422

423

424 LogicalResult visitSMTOp(ArrayStoreOp op, VisitorInfo &info) {

425 info.stream << "(store " << info.valueMap.lookup(op.getArray()) << " "

426 << info.valueMap.lookup(op.getIndex()) << " "

427 << info.valueMap.lookup(op.getValue()) << ")";

428 return success();

429 }

430

431 LogicalResult visitSMTOp(ArraySelectOp op, VisitorInfo &info) {

432 info.stream << "(select " << info.valueMap.lookup(op.getArray()) << " "

433 << info.valueMap.lookup(op.getIndex()) << ")";

434 return success();

435 }

436

437 LogicalResult visitSMTOp(ArrayBroadcastOp op, VisitorInfo &info) {

438 info.stream << "((as const ";

439 typeVisitor.dispatchSMTTypeVisitor(op.getType(), info.stream);

440 info.stream << ") " << info.valueMap.lookup(op.getValue()) << ")";

441 return success();

442 }

443

444 LogicalResult visitUnhandledSMTOp(Operation *op, VisitorInfo &info) {

445 return success();

446 }

447

448 #undef HANDLE_OP

449

450

451

453 VisitorInfo &info) {

454 while (!worklist.empty()) {

455 Value curr = worklist.back();

456

457

458 if (info.valueMap.count(curr)) {

459 worklist.pop_back();

460 continue;

461 }

462

463

464

465 bool allAvailable = true;

467 assert(defOp != nullptr &&

468 "block arguments must already be in the valueMap");

469

471 if (!info.valueMap.count(val)) {

472 worklist.push_back(val);

473 allAvailable = false;

474 }

475 }

476

477 if (!allAvailable)

478 continue;

479

480 if (failed(dispatchSMTOpVisitor(curr.getDefiningOp(), info)))

481 return failure();

482

483 worklist.pop_back();

484 }

485

486 return success();

487 }

488

489 private:

490

492 TypeVisitor typeVisitor;

494 };

495

496

497

498 struct StatementVisitor

500 mlir::raw_indented_ostream &, ValueMap &> {

503

506 exprVisitor(options, names) {}

507

510 valueMap.insert(op.getResult(), op.getValue().getValueAsString());

511 return success();

512 }

513

514 LogicalResult visitSMTOp(BoolConstantOp op,

517 valueMap.insert(op.getResult(), op.getValue() ? "true" : "false");

518 return success();

519 }

520

524 op.getValue().toStringSigned(str);

525 valueMap.insert(op.getResult(), str.str().str());

526 return success();

527 }

528

531 StringRef name =

532 names.newName(op.getNamePrefix() ? *op.getNamePrefix() : "tmp");

533 valueMap.insert(op.getResult(), name.str());

534 stream << "("

535 << (isa(op.getType()) ? "declare-fun "

536 : "declare-const ")

537 << name << " ";

538 typeVisitor.dispatchSMTTypeVisitor(op.getType(), stream);

539 stream << ")\n";

540 return success();

541 }

542

545 llvm::ScopedHashTableScope<Value, std::string> scope1(valueMap);

547 worklist.push_back(op.getInput());

548 stream << "(assert ";

549 VisitorInfo info(stream, valueMap, 8, 0);

550 if (failed(exprVisitor.printExpression(worklist, info)))

551 return failure();

552 stream << valueMap.lookup(op.getInput());

553 for (unsigned i = 0; i < info.openParens + 1; ++i)

554 stream << ")";

555 stream << "\n";

557 return success();

558 }

559

562 stream << "(reset)\n";

563 return success();

564 }

565

568 stream << "(push " << op.getCount() << ")\n";

569 return success();

570 }

571

574 stream << "(pop " << op.getCount() << ")\n";

575 return success();

576 }

577

580 if (op->getNumResults() != 0)

581 return op.emitError() << "must not have any result values";

582

583 if (op.getSatRegion().front().getOperations().size() != 1)

584 return op->emitError() << "'sat' region must be empty";

585 if (op.getUnknownRegion().front().getOperations().size() != 1)

586 return op->emitError() << "'unknown' region must be empty";

587 if (op.getUnsatRegion().front().getOperations().size() != 1)

588 return op->emitError() << "'unsat' region must be empty";

589

590 stream << "(check-sat)\n";

591 return success();

592 }

593

596 stream << "(set-logic " << op.getLogic() << ")\n";

597 return success();

598 }

599

600 LogicalResult visitUnhandledSMTOp(Operation *op,

603

604 if (isa<smt::Int2BVOp, BV2IntOp>(op))

605 return op->emitError("operation not supported for SMTLIB emission");

606

607 return success();

608 }

609

610 private:

611

613 TypeVisitor typeVisitor;

615 ExpressionVisitor exprVisitor;

616 };

617

618 }

619

620

621

622

623

624

627 if (!solver.getInputs().empty() || solver->getNumResults() != 0)

628 return solver->emitError()

629 << "solver scopes with inputs or results are not supported";

630

631 Block *block = solver.getBody();

632

633

636 if (!isa(op->getDialect()))

638 << "solver must not contain any non-SMT operations";

639

641 auto sortTy = dyn_cast(resTy);

642 if (!sortTy)

643 continue;

644

645 unsigned arity = sortTy.getSortParams().size();

646 if (declaredSorts.contains(sortTy.getIdentifier())) {

647 if (declaredSorts[sortTy.getIdentifier()] != arity)

648 return op->emitError("uninterpreted sorts with same identifier but "

649 "different arity found");

650

651 continue;

652 }

653

654 declaredSorts[sortTy.getIdentifier()] = arity;

655 stream << "(declare-sort " << sortTy.getIdentifier().getValue() << " "

656 << arity << ")\n";

657 }

659 });

660 if (result.wasInterrupted())

661 return failure();

662

664 llvm::ScopedHashTableScope<Value, std::string> scope0(valueMap);

666 StatementVisitor visitor(options, names);

667

668

669

670 result = block->walk([&](Operation *op) {

671 if (failed(visitor.dispatchSMTOpVisitor(op, stream, valueMap)))

674 });

675 if (result.wasInterrupted())

676 return failure();

677

678 stream << "(reset)\n";

679 return success();

680 }

681

685 return module->emitError("must have exactly one region");

687 return module->emitError("op region must have exactly one block");

688

690 unsigned solverIdx = 0;

691 auto result = module->walk([&](SolverOp solver) {

692 ios << "; solver scope " << solverIdx << "\n";

695 ++solverIdx;

697 });

698

699 return failure(result.wasInterrupted());

700 }

701

702

703

704

705

707 static llvm:🆑:opt inlineSingleUseValues(

708 "smtlibexport-inline-single-use-values",

709 llvm:🆑:desc("Inline expressions that are used only once rather than "

710 "generating a let-binding"),

711 llvm:🆑:init(false));

712

713 auto getOptions = [] {

716 return opts;

717 };

718

720 "export-smtlib", "export SMT-LIB",

721 [=](Operation *module, raw_ostream &output) {

723 },

725

726

727 registry.insert<mlir::func::FuncDialect, arith::ArithDialect,

728 smt::SMTDialect>();

729 });

730 }

static llvm::ManagedStatic< PassManagerOptions > options

static LogicalResult emit(SolverOp solver, const SMTEmissionOptions &options, mlir::raw_indented_ostream &stream)

Emit the SMT operations in the given 'solver' to the 'stream'.

#define HANDLE_OP(OPTYPE, NAME, KIND)

llvm::ScopedHashTable< mlir::Value, std::string > ValueMap

Block represents an ordered list of Operations.

RetT walk(FnT &&callback)

Walk all nested operations, blocks (including this block) or regions, depending on the type of callba...

The DialectRegistry maps a dialect namespace to a constructor for the matching dialect.

A namespace that is used to store existing names and generate new names in some scope within the IR.

llvm::StringRef newName(const llvm::Twine &name)

Return a unique name, derived from the input name, and add the new name to the internal namespace.

This provides public APIs that all operations should have.

Operation is the basic unit of execution within MLIR.

Dialect * getDialect()

Return the dialect this operation is associated with, or nullptr if the associated dialect is not loa...

OpResult getResult(unsigned idx)

Get the 'idx'th result of this operation.

std::enable_if_t< llvm::function_traits< std::decay_t< FnT > >::num_args==1, RetT > walk(FnT &&callback)

Walk the operation by calling the callback for each nested operation (including this one),...

unsigned getNumRegions()

Returns the number of regions held by this operation.

InFlightDiagnostic emitError(const Twine &message={})

Emit an error about fatal conditions with this operation, reporting up to any diagnostic handlers tha...

Region & getRegion(unsigned index)

Returns the region held by this operation at position 'index'.

result_type_range getResultTypes()

operand_range getOperands()

Returns an iterator on the underlying Value's.

unsigned getNumResults()

Return the number of results held by this operation.

bool hasOneBlock()

Return true if this region has exactly one block.

Instances of the Type class are uniqued, have an immutable identifier and an optional mutable compone...

This class represents an instance of an SSA value in the MLIR system, representing a computable value...

bool hasOneUse() const

Returns true if this value has exactly one use.

Operation * getDefiningOp() const

If this value is the result of an operation, return the operation that defines it.

A utility result that is used to signal how to proceed with an ongoing walk:

static WalkResult advance()

static WalkResult interrupt()

raw_ostream subclass that simplifies indention a sequence of code.

raw_indented_ostream & indent()

Increases the indent and returning this raw_indented_ostream.

This helps visit SMT nodes.

This helps visit SMT types.

constexpr void enumerate(std::tuple< Tys... > &tuple, CallbackT &&callback)

void registerExportSMTLIBTranslation()

LogicalResult exportSMTLIB(Operation *module, llvm::raw_ostream &os, const SMTEmissionOptions &options=SMTEmissionOptions())

Run the ExportSMTLIB pass.

Include the generated interface declarations.

const FrozenRewritePatternSet & patterns

Emission options for the ExportSMTLIB pass.

bool inlineSingleUseValues

Eliminates variable at the specified position using Fourier-Motzkin variable elimination.