From c429aef60f60cf405cf9e35e019446b37c430617 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Sat, 22 Feb 2025 17:14:13 +1300
Subject: [PATCH] docs/rosette: More intro of SMT-LIB backend
As the intro paragraph (now) says:
> This section will introduce the SMT-LIB functional backend and what changes are needed...
The example is intended to be read without prior knowledge of the SMT-LIB backend, but the previous version glossed over a lot and instead focused on *just* what was changed.
This version should now be easier to follow without prior knowledge, while still being able to learn enough about the `Smt` version to adapt it to a different s-expression target that isn't Rosette.
Also adds a few `literalinclude`s of smtlib.cc, which is now copied to `docs/source/generated` along with producing the rosette diff on the fly (which now also has up to 20 lines of context, enabling the full `Module::write()` diff to be literal included).
---
Makefile | 14 +-
.../code_examples/functional/rosette.diff | 372 ------------------
.../extending_yosys/functional_ir.rst | 149 ++++---
3 files changed, 98 insertions(+), 437 deletions(-)
delete mode 100644 docs/source/code_examples/functional/rosette.diff
diff --git a/Makefile b/Makefile
index 6f5fec6a2..73dd2e335 100644
--- a/Makefile
+++ b/Makefile
@@ -996,6 +996,18 @@ docs/source/cell/word_add.rst: $(TARGETS) $(EXTRA_TARGETS)
docs/source/generated/cells.json: docs/source/generated $(TARGETS) $(EXTRA_TARGETS)
$(Q) ./$(PROGRAM_PREFIX)yosys -p 'help -dump-cells-json $@'
+docs/source/generated/%.cc: backends/%.cc
+ $(Q) mkdir -p $(@D)
+ $(Q) cp $< $@
+
+# diff returns exit code 1 if the files are different, but it's not an error
+docs/source/generated/functional/rosette.diff: backends/functional/smtlib.cc backends/functional/smtlib_rosette.cc
+ $(Q) mkdir -p $(@D)
+ $(Q) diff -U 20 $^ > $@ || exit 0
+
+PHONY: docs/gen/functional_ir
+docs/gen/functional_ir: docs/source/generated/functional/smtlib.cc docs/source/generated/functional/rosette.diff
+
PHONY: docs/gen docs/usage docs/reqs
docs/gen: $(TARGETS)
$(Q) $(MAKE) -C docs gen
@@ -1031,7 +1043,7 @@ docs/reqs:
$(Q) $(MAKE) -C docs reqs
.PHONY: docs/prep
-docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage
+docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage docs/gen/functional_ir
DOC_TARGET ?= html
docs: docs/prep
diff --git a/docs/source/code_examples/functional/rosette.diff b/docs/source/code_examples/functional/rosette.diff
deleted file mode 100644
index 35c7936d1..000000000
--- a/docs/source/code_examples/functional/rosette.diff
+++ /dev/null
@@ -1,372 +0,0 @@
-diff --git a/backends/functional/smtlib.cc b/backends/functional/smtlib_rosette.cc
-index 3eacf407c..c9e737d19 100644
---- a/backends/functional/smtlib.cc
-+++ b/backends/functional/smtlib_rosette.cc
-@@ -29,80 +29,86 @@ PRIVATE_NAMESPACE_BEGIN
- using SExprUtil::list;
-
- const char *reserved_keywords[] = {
-- // reserved keywords from the smtlib spec
-- "BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "match", "par",
-- "assert", "check-sat", "check-sat-assuming", "declare-const", "declare-datatype", "declare-datatypes",
-- "declare-fun", "declare-sort", "define-fun", "define-fun-rec", "define-funs-rec", "define-sort",
-- "exit", "get-assertions", "symbol", "sort", "get-assignment", "get-info", "get-model",
-- "get-option", "get-proof", "get-unsat-assumptions", "get-unsat-core", "get-value",
-- "pop", "push", "reset", "reset-assertions", "set-info", "set-logic", "set-option",
-+ // reserved keywords from the racket spec
-+ "struct", "lambda", "values", "extract", "concat", "bv", "let", "define", "cons", "list", "read", "write",
-+ "stream", "error", "raise", "exit", "for", "begin", "when", "unless", "module", "require", "provide", "apply",
-+ "if", "cond", "even", "odd", "any", "and", "or", "match", "command-line", "ffi-lib", "thread", "kill", "sync",
-+ "future", "touch", "subprocess", "make-custodian", "custodian-shutdown-all", "current-custodian", "make", "tcp",
-+ "connect", "prepare", "malloc", "free", "_fun", "_cprocedure", "build", "path", "file", "peek", "bytes",
-+ "flush", "with", "lexer", "parser", "syntax", "interface", "send", "make-object", "new", "instantiate",
-+ "define-generics", "set",
-
- // reserved for our own purposes
-- "pair", "Pair", "first", "second",
-- "inputs", "state",
-+ "inputs", "state", "name",
- nullptr
- };
-
--struct SmtScope : public Functional::Scope<int> {
-- SmtScope() {
-+struct SmtrScope : public Functional::Scope<int> {
-+ SmtrScope() {
- for(const char **p = reserved_keywords; *p != nullptr; p++)
- reserve(*p);
- }
- bool is_character_legal(char c, int index) override {
-- return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("~!@$%^&*_-+=<>.?/", c));
-+ return isascii(c) && (isalpha(c) || (isdigit(c) && index > 0) || strchr("@$%^&_+=.", c));
- }
- };
-
--struct SmtSort {
-+struct SmtrSort {
- Functional::Sort sort;
-- SmtSort(Functional::Sort sort) : sort(sort) {}
-+ SmtrSort(Functional::Sort sort) : sort(sort) {}
- SExpr to_sexpr() const {
- if(sort.is_memory()) {
-- return list("Array", list("_", "BitVec", sort.addr_width()), list("_", "BitVec", sort.data_width()));
-+ return list("list", list("bitvector", sort.addr_width()), list("bitvector", sort.data_width()));
- } else if(sort.is_signal()) {
-- return list("_", "BitVec", sort.width());
-+ return list("bitvector", sort.width());
- } else {
- log_error("unknown sort");
- }
- }
- };
-
--class SmtStruct {
-+class SmtrStruct {
- struct Field {
-- SmtSort sort;
-+ SmtrSort sort;
- std::string accessor;
-+ std::string name;
- };
- idict<IdString> field_names;
- vector<Field> fields;
-- SmtScope &scope;
-+ SmtrScope &global_scope;
-+ SmtrScope local_scope;
- public:
- std::string name;
-- SmtStruct(std::string name, SmtScope &scope) : scope(scope), name(name) {}
-- void insert(IdString field_name, SmtSort sort) {
-+ SmtrStruct(std::string name, SmtrScope &scope) : global_scope(scope), local_scope(), name(name) {}
-+ void insert(IdString field_name, SmtrSort sort) {
- field_names(field_name);
-- auto accessor = scope.unique_name("\\" + name + "_" + RTLIL::unescape_id(field_name));
-- fields.emplace_back(Field{sort, accessor});
-+ auto base_name = local_scope.unique_name(field_name);
-+ auto accessor = name + "-" + base_name;
-+ global_scope.reserve(accessor);
-+ fields.emplace_back(Field{sort, accessor, base_name});
- }
- void write_definition(SExprWriter &w) {
-- w.open(list("declare-datatype", name));
-- w.open(list());
-- w.open(list(name));
-- for(const auto &field : fields)
-- w << list(field.accessor, field.sort.to_sexpr());
-- w.close(3);
-+ vector<SExpr> field_list;
-+ for(const auto &field : fields) {
-+ field_list.emplace_back(field.name);
-+ }
-+ w.push();
-+ w.open(list("struct", name, field_list, "#:transparent"));
-+ if (field_names.size()) {
-+ for (const auto &field : fields) {
-+ auto bv_type = field.sort.to_sexpr();
-+ w.comment(field.name + " " + bv_type.to_string());
-+ }
-+ }
-+ w.pop();
- }
- template<typename Fn> void write_value(SExprWriter &w, Fn fn) {
-- if(field_names.empty()) {
-- // Zero-argument constructors in SMTLIB must not be called as functions.
-- w << name;
-- } else {
-- w.open(list(name));
-- for(auto field_name : field_names) {
-- w << fn(field_name);
-- w.comment(RTLIL::unescape_id(field_name), true);
-- }
-- w.close();
-+ w.open(list(name));
-+ for(auto field_name : field_names) {
-+ w << fn(field_name);
-+ w.comment(RTLIL::unescape_id(field_name), true);
- }
-+ w.close();
- }
- SExpr access(SExpr record, IdString name) {
- size_t i = field_names.at(name);
-@@ -117,28 +123,28 @@ std::string smt_const(RTLIL::Const const &c) {
- return s;
- }
-
--struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
-+struct SmtrPrintVisitor : public Functional::AbstractVisitor<SExpr> {
- using Node = Functional::Node;
- std::function<SExpr(Node)> n;
-- SmtStruct &input_struct;
-- SmtStruct &state_struct;
-+ SmtrStruct &input_struct;
-+ SmtrStruct &state_struct;
-
-- SmtPrintVisitor(SmtStruct &input_struct, SmtStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {}
-+ SmtrPrintVisitor(SmtrStruct &input_struct, SmtrStruct &state_struct) : input_struct(input_struct), state_struct(state_struct) {}
-
- SExpr from_bool(SExpr &&arg) {
-- return list("ite", std::move(arg), "#b1", "#b0");
-+ return list("bool->bitvector", std::move(arg));
- }
- SExpr to_bool(SExpr &&arg) {
-- return list("=", std::move(arg), "#b1");
-+ return list("bitvector->bool", std::move(arg));
- }
-- SExpr extract(SExpr &&arg, int offset, int out_width = 1) {
-- return list(list("_", "extract", offset + out_width - 1, offset), std::move(arg));
-+ SExpr to_list(SExpr &&arg) {
-+ return list("bitvector->bits", std::move(arg));
- }
-
- SExpr buf(Node, Node a) override { return n(a); }
-- SExpr slice(Node, Node a, int offset, int out_width) override { return extract(n(a), offset, out_width); }
-- SExpr zero_extend(Node, Node a, int out_width) override { return list(list("_", "zero_extend", out_width - a.width()), n(a)); }
-- SExpr sign_extend(Node, Node a, int out_width) override { return list(list("_", "sign_extend", out_width - a.width()), n(a)); }
-+ SExpr slice(Node, Node a, int offset, int out_width) override { return list("extract", offset + out_width - 1, offset, n(a)); }
-+ SExpr zero_extend(Node, Node a, int out_width) override { return list("zero-extend", n(a), list("bitvector", out_width)); }
-+ SExpr sign_extend(Node, Node a, int out_width) override { return list("sign-extend", n(a), list("bitvector", out_width)); }
- SExpr concat(Node, Node a, Node b) override { return list("concat", n(b), n(a)); }
- SExpr add(Node, Node a, Node b) override { return list("bvadd", n(a), n(b)); }
- SExpr sub(Node, Node a, Node b) override { return list("bvsub", n(a), n(b)); }
-@@ -150,16 +156,11 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
- SExpr bitwise_xor(Node, Node a, Node b) override { return list("bvxor", n(a), n(b)); }
- SExpr bitwise_not(Node, Node a) override { return list("bvnot", n(a)); }
- SExpr unary_minus(Node, Node a) override { return list("bvneg", n(a)); }
-- SExpr reduce_and(Node, Node a) override { return from_bool(list("=", n(a), smt_const(RTLIL::Const(State::S1, a.width())))); }
-- SExpr reduce_or(Node, Node a) override { return from_bool(list("distinct", n(a), smt_const(RTLIL::Const(State::S0, a.width())))); }
-- SExpr reduce_xor(Node, Node a) override {
-- vector<SExpr> s { "bvxor" };
-- for(int i = 0; i < a.width(); i++)
-- s.push_back(extract(n(a), i));
-- return s;
-- }
-- SExpr equal(Node, Node a, Node b) override { return from_bool(list("=", n(a), n(b))); }
-- SExpr not_equal(Node, Node a, Node b) override { return from_bool(list("distinct", n(a), n(b))); }
-+ SExpr reduce_and(Node, Node a) override { return list("apply", "bvand", to_list(n(a))); }
-+ SExpr reduce_or(Node, Node a) override { return list("apply", "bvor", to_list(n(a))); }
-+ SExpr reduce_xor(Node, Node a) override { return list("apply", "bvxor", to_list(n(a))); }
-+ SExpr equal(Node, Node a, Node b) override { return from_bool(list("bveq", n(a), n(b))); }
-+ SExpr not_equal(Node, Node a, Node b) override { return from_bool(list("not", list("bveq", n(a), n(b)))); }
- SExpr signed_greater_than(Node, Node a, Node b) override { return from_bool(list("bvsgt", n(a), n(b))); }
- SExpr signed_greater_equal(Node, Node a, Node b) override { return from_bool(list("bvsge", n(a), n(b))); }
- SExpr unsigned_greater_than(Node, Node a, Node b) override { return from_bool(list("bvugt", n(a), n(b))); }
-@@ -167,32 +168,32 @@ struct SmtPrintVisitor : public Functional::AbstractVisitor<SExpr> {
-
- SExpr extend(SExpr &&a, int in_width, int out_width) {
- if(in_width < out_width)
-- return list(list("_", "zero_extend", out_width - in_width), std::move(a));
-+ return list("zero-extend", std::move(a), list("bitvector", out_width));
- else
- return std::move(a);
- }
- SExpr logical_shift_left(Node, Node a, Node b) override { return list("bvshl", n(a), extend(n(b), b.width(), a.width())); }
- SExpr logical_shift_right(Node, Node a, Node b) override { return list("bvlshr", n(a), extend(n(b), b.width(), a.width())); }
- SExpr arithmetic_shift_right(Node, Node a, Node b) override { return list("bvashr", n(a), extend(n(b), b.width(), a.width())); }
-- SExpr mux(Node, Node a, Node b, Node s) override { return list("ite", to_bool(n(s)), n(b), n(a)); }
-- SExpr constant(Node, RTLIL::Const const &value) override { return smt_const(value); }
-- SExpr memory_read(Node, Node mem, Node addr) override { return list("select", n(mem), n(addr)); }
-- SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list("store", n(mem), n(addr), n(data)); }
-+ SExpr mux(Node, Node a, Node b, Node s) override { return list("if", to_bool(n(s)), n(b), n(a)); }
-+ SExpr constant(Node, RTLIL::Const const& value) override { return list("bv", smt_const(value), value.size()); }
-+ SExpr memory_read(Node, Node mem, Node addr) override { return list("list-ref-bv", n(mem), n(addr)); }
-+ SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list("list-set-bv", n(mem), n(addr), n(data)); }
-
- SExpr input(Node, IdString name, IdString kind) override { log_assert(kind == ID($input)); return input_struct.access("inputs", name); }
- SExpr state(Node, IdString name, IdString kind) override { log_assert(kind == ID($state)); return state_struct.access("state", name); }
- };
-
--struct SmtModule {
-+struct SmtrModule {
- Functional::IR ir;
-- SmtScope scope;
-+ SmtrScope scope;
- std::string name;
-
-- SmtStruct input_struct;
-- SmtStruct output_struct;
-- SmtStruct state_struct;
-+ SmtrStruct input_struct;
-+ SmtrStruct output_struct;
-+ SmtrStruct state_struct;
-
-- SmtModule(Module *module)
-+ SmtrModule(Module *module)
- : ir(Functional::IR::from_module(module))
- , scope()
- , name(scope.unique_name(module->name))
-@@ -200,7 +201,7 @@ struct SmtModule {
- , output_struct(scope.unique_name(module->name.str() + "_Outputs"), scope)
- , state_struct(scope.unique_name(module->name.str() + "_State"), scope)
- {
-- scope.reserve(name + "-initial");
-+ scope.reserve(name + "_initial");
- for (auto input : ir.inputs())
- input_struct.insert(input->name, input->sort);
- for (auto output : ir.outputs())
-@@ -212,14 +213,11 @@ struct SmtModule {
- void write_eval(SExprWriter &w)
- {
- w.push();
-- w.open(list("define-fun", name,
-- list(list("inputs", input_struct.name),
-- list("state", state_struct.name)),
-- list("Pair", output_struct.name, state_struct.name)));
-+ w.open(list("define", list(name, "inputs", "state")));
- auto inlined = [&](Functional::Node n) {
- return n.fn() == Functional::Fn::constant;
- };
-- SmtPrintVisitor visitor(input_struct, state_struct);
-+ SmtrPrintVisitor visitor(input_struct, state_struct);
- auto node_to_sexpr = [&](Functional::Node n) -> SExpr {
- if(inlined(n))
- return n.visit(visitor);
-@@ -230,9 +228,9 @@ struct SmtModule {
- for(auto n : ir)
- if(!inlined(n)) {
- w.open(list("let", list(list(node_to_sexpr(n), n.visit(visitor)))), false);
-- w.comment(SmtSort(n.sort()).to_sexpr().to_string(), true);
-+ w.comment(SmtrSort(n.sort()).to_sexpr().to_string(), true);
- }
-- w.open(list("pair"));
-+ w.open(list("cons"));
- output_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.output(name).value()); });
- state_struct.write_value(w, [&](IdString name) { return node_to_sexpr(ir.state(name).next_value()); });
- w.pop();
-@@ -240,19 +238,23 @@ struct SmtModule {
-
- void write_initial(SExprWriter &w)
- {
-- std::string initial = name + "-initial";
-- w << list("declare-const", initial, state_struct.name);
-+ w.push();
-+ auto initial = name + "_initial";
-+ w.open(list("define", initial));
-+ w.open(list(state_struct.name));
- for (auto state : ir.states()) {
-- if(state->sort.is_signal())
-- w << list("assert", list("=", state_struct.access(initial, state->name), smt_const(state->initial_value_signal())));
-- else if(state->sort.is_memory()) {
-+ if (state->sort.is_signal())
-+ w << list("bv", smt_const(state->initial_value_signal()), state->sort.width());
-+ else if (state->sort.is_memory()) {
- const auto &contents = state->initial_value_memory();
-+ w.open(list("list"));
- for(int i = 0; i < 1<<state->sort.addr_width(); i++) {
-- auto addr = smt_const(RTLIL::Const(i, state->sort.addr_width()));
-- w << list("assert", list("=", list("select", state_struct.access(initial, state->name), addr), smt_const(contents[i])));
-+ w << list("bv", smt_const(contents[i]), state->sort.data_width());
- }
-+ w.close();
- }
- }
-+ w.pop();
- }
-
- void write(std::ostream &out)
-@@ -263,33 +265,53 @@ struct SmtModule {
- output_struct.write_definition(w);
- state_struct.write_definition(w);
-
-- w << list("declare-datatypes",
-- list(list("Pair", 2)),
-- list(list("par", list("X", "Y"), list(list("pair", list("first", "X"), list("second", "Y"))))));
--
- write_eval(w);
- write_initial(w);
- }
- };
-
--struct FunctionalSmtBackend : public Backend {
-- FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from Functional IR") {}
-+struct FunctionalSmtrBackend : public Backend {
-+ FunctionalSmtrBackend() : Backend("functional_rosette", "Generate Rosette compatible Racket from Functional IR") {}
-
-- void help() override { log("\nFunctional SMT Backend.\n\n"); }
-+ void help() override {
-+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
-+ log("\n");
-+ log(" write_functional_rosette [options] [filename]\n");
-+ log("\n");
-+ log("Functional Rosette Backend.\n");
-+ log("\n");
-+ log(" -provides\n");
-+ log(" include 'provide' statement(s) for loading output as a module\n");
-+ log("\n");
-+ }
-
- void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
- {
-- log_header(design, "Executing Functional SMT Backend.\n");
-+ auto provides = false;
-+
-+ log_header(design, "Executing Functional Rosette Backend.\n");
-
-- size_t argidx = 1;
-- extra_args(f, filename, args, argidx, design);
-+ size_t argidx;
-+ for (argidx = 1; argidx < args.size(); argidx++)
-+ {
-+ if (args[argidx] == "-provides")
-+ provides = true;
-+ else
-+ break;
-+ }
-+ extra_args(f, filename, args, argidx);
-+
-+ *f << "#lang rosette/safe\n";
-+ if (provides) {
-+ *f << "(provide (all-defined-out))\n";
-+ }
-
- for (auto module : design->selected_modules()) {
- log("Processing module `%s`.\n", module->name.c_str());
-- SmtModule smt(module);
-- smt.write(*f);
-+ SmtrModule smtr(module);
-+ smtr.write(*f);
- }
- }
--} FunctionalSmtBackend;
-+} FunctionalSmtrBackend;
-
- PRIVATE_NAMESPACE_END
diff --git a/docs/source/yosys_internals/extending_yosys/functional_ir.rst b/docs/source/yosys_internals/extending_yosys/functional_ir.rst
index 81d987f0e..42eabc0b1 100644
--- a/docs/source/yosys_internals/extending_yosys/functional_ir.rst
+++ b/docs/source/yosys_internals/extending_yosys/functional_ir.rst
@@ -147,9 +147,9 @@ S-expressions can be constructed with ``SExpr::list``, for example ``SExpr expr
Example: Adapting SMT-LIB backend for Rosette
---------------------------------------------
-This section will walk through the process of adapting the SMT-LIB functional
-backend (`write_functional_smt2`) to work with another s-expression target,
-`Rosette`_ (`write_functional_rosette`).
+This section will introduce the SMT-LIB functional backend
+(`write_functional_smt2`) and what changes are needed to work with another
+s-expression target, `Rosette`_ (`write_functional_rosette`).
.. _Rosette: http://emina.github.io/rosette/
@@ -177,12 +177,19 @@ Scope
~~~~~
As described above, the ``Functional::Scope`` class is derived in order to avoid
-collisions between identifiers in the generated output. We switch out ``Smt``
-in the class name for ``Smtr`` for ``smtlib_rosette``; which will happen through
-the rest of the code too. We also update the ``is_character_legal`` method to
-reject ascii characters which are not allowed in Racket variable names.
+collisions between identifiers in the generated output. In the SMT-LIB version
+the ``SmtScope`` class implements ``Scope<int>``; provides a constructor that
+iterates over a list of reserved keywords, calling ``reserve`` on each; and
+defines the ``is_character_legal`` method to reject any characters which are not
+allowed in SMT-LIB variable names to then be replaced with underscores in the
+output.
-.. literalinclude:: /code_examples/functional/rosette.diff
+In the Rosette version we switch out ``Smt`` in the class name for ``Smtr`` to
+mean ``smtlib_rosette``; this will happen through the rest of the code too. We
+also update list of legal ascii characters in the ``is_character_legal`` method
+to only those allowed in Racket variable names.
+
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of ``Scope`` class
:start-at: -struct SmtScope : public Functional::Scope<int> {
@@ -218,13 +225,13 @@ and racket specifications to save on space in this document.
Sort
~~~~
-The ``Sort`` class is a wrapper for the ``Functional::Sort`` class, providing
-the additional functionality of mapping variable declarations to s-expressions
-with the ``to_sexpr()`` method. The main change from ``SmtSort`` to
-``SmtrSort`` is a syntactical one with signals represented as ``bitvector``\
-s, and memories as ``list``\ s of signals.
+Next up in `write_functional_smt2` we see the ``Sort`` class. This is a wrapper
+for the ``Functional::Sort`` class, providing the additional functionality of
+mapping variable declarations to s-expressions with the ``to_sexpr()`` method.
+The main change from ``SmtSort`` to ``SmtrSort`` is a syntactical one with
+signals represented as ``bitvector``\ s, and memories as ``list``\ s of signals.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of ``Sort`` wrapper
:start-at: SExpr to_sexpr() const {
@@ -233,37 +240,56 @@ s, and memories as ``list``\ s of signals.
Struct
~~~~~~
-The SMT-LIB backend uses a class, ``SmtStruct``, to help with describing the
-input, output, and state data structs. Where each struct in the SMT-LIB output
-is a new ``datatype`` with each element having its type declared using the
-`Sort`_ above, in Rosette we use the native ``struct`` with each field only
-being referred to by name. For ease of use, we include comments for each field
-to indicate the expected type.
+The ``Functional::IR`` class tracks the set of inputs, the set of outputs, and
+the set of "state" variables. The SMT-LIB backend maps each of these sets into
+its own ``SmtStruct``, with each variable getting a corresponding field in the
+struct and a specified `Sort`_. `write_functional_smt2` then defines each of
+these structs as a new ``datatype``, with each element being strongly-typed.
-.. literalinclude:: /code_examples/functional/rosette.diff
+In Rosette, rather than defining new datatypes for our structs, we use the
+native ``struct``. We also only declare each field by name because Racket is
+not as strongly-typed. For ease of use, we provide the expected type for each
+field as comments.
+
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of ``write_definition`` method
:start-at: void write_definition
:end-before: template<typename Fn> void write_value
-Struct fields in Rosette are accessed as ``<struct_name>-<field_name>``, where
-field names only need to be unique within the struct, while accessors are unique
-within the module. We thus modify the class constructor and ``insert`` method
-to support this; providing one scope that is local to the struct
-(``local_scope``) and one which is shared across the whole module
-(``global_scope``).
+Each field is added to the ``SmtStruct`` with the ``insert`` method, which also
+reserves a unique name (or accessor) within the `Scope`_. These accessors
+combine the struct name and field name and are globally unique, being used in
+the ``access`` method for reading values from the input/current state.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/smtlib.cc
+ :language: c++
+ :caption: ``Struct::access()`` method
+ :start-at: SExpr access(
+ :end-before: };
+
+In Rosette, struct fields are accessed as ``<struct_name>-<field_name>`` so
+including the struct name in the field name would be redundant. For
+`write_functional_rosette` we instead choose to make field names unique only
+within the struct, while accessors are unique across the whole module. We thus
+modify the class constructor and ``insert`` method to support this; providing
+one scope that is local to the struct (``local_scope``) and one which is shared
+across the whole module (``global_scope``), leaving the ``access`` method
+unchanged.
+
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of struct constructor
:start-at: SmtStruct(std::string name, SmtScope &scope)
:end-before: void write_definition
-For writing outputs/next state (the ``write_value`` method), the only change is
-to remove the check for zero-argument constructors since this is not necessary
-with Rosette ``struct``\ s.
+Finally, ``SmtStruct`` also provides a ``write_value`` template method which
+calls a provided function on each element in the struct. This is used later for
+assigning values to the output/next state pair. The only change here is to
+remove the check for zero-argument constructors since this is not necessary with
+Rosette ``struct``\ s.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of ``write_value`` method
:start-at: template<typename Fn> void write_value
@@ -273,11 +299,13 @@ PrintVisitor
~~~~~~~~~~~~
The ``PrintVisitor`` implements the abstract ``Functional::AbstractVisitor``
-class for converting FunctionalIR functions into s-expressions, including
-reading inputs/current state. For most functions, the Rosette output is very
-similar to the corresponding SMT-LIB function with minor adjustments for syntax.
+class, described above in `What is FunctionalIR`_, with a return type of
+``SExpr``. This class converts FunctionalIR functions into s-expressions,
+including reading inputs/current state with the ``access`` method from the
+`Struct`_. For most functions, the Rosette output is very similar to the
+corresponding SMT-LIB function with minor adjustments for syntax.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: portion of ``Functional::AbstractVisitor`` implementation diff showing similarities
:start-at: SExpr logical_shift_left
@@ -286,7 +314,7 @@ similar to the corresponding SMT-LIB function with minor adjustments for syntax.
However there are some differences in the two formats with regards to how
booleans are handled, with Rosette providing built-in functions for conversion.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: portion of ``Functional::AbstractVisitor`` implementation diff showing differences
:start-at: SExpr from_bool
@@ -295,14 +323,21 @@ booleans are handled, with Rosette providing built-in functions for conversion.
Module
~~~~~~
-The ``Functional::IR`` is wrapped in the ``Module`` class, with the mapping from
-RTLIL module to FunctionalIR happening in the constructor. Each of the three
-structs; inputs, outputs, and state; are then created from the corresponding
-lists in the IR. The only change here is rename the initial state to use ``_``
-instead of ``-``, since the ``-`` in Rosette can be used to access struct
-fields.
+The ``Functional::IR`` is wrapped in the ``SmtModule`` class, with the mapping
+from RTLIL module to FunctionalIR happening in the constructor. Each of the
+three ``SmtStruct``\ s; inputs, outputs, and state; are created, with each value
+in the corresponding lists in the IR being ``insert``\ ed.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/smtlib.cc
+ :language: c++
+ :caption: ``SmtModule`` constructor
+ :start-at: SmtModule(Module
+ :end-at: }
+
+Since Racket uses the ``-`` to access struct fields, the ``SmtrModule`` instead
+uses an underscore for the name of the initial state.
+
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of ``Module`` constructor
:start-at: scope.reserve(name
@@ -316,25 +351,11 @@ current_state) -> (outputs, next_state)`` with ``write_eval``, and declaring the
initial state with ``write_initial``. The only change for the ``SmtrModule`` is
that the ``pair`` declaration isn't needed.
-.. inlined diff to show the complete function
-.. code-block:: diff
+.. literalinclude:: /generated/functional/rosette.diff
+ :language: diff
:caption: diff of ``Module::write()`` method
-
- void write(std::ostream &out)
- {
- SExprWriter w(out);
-
- input_struct.write_definition(w);
- output_struct.write_definition(w);
- state_struct.write_definition(w);
-
- - w << list("declare-datatypes",
- - list(list("Pair", 2)),
- - list(list("par", list("X", "Y"), list(list("pair", list("first", "X"), list("second", "Y"))))));
- -
- write_eval(w);
- write_initial(w);
- }
+ :start-at: void write(std::ostream &out)
+ :end-at: }
For the ``write_eval`` method, the main differences are syntactical. First we
change the function declaration line for the Rosette style which drops the
@@ -371,7 +392,7 @@ variable, ``[name]_initial``, can then be used in the ``[name]`` function call;
allowing the Rosette code to be used in the generation of the ``next_state``,
whereas the SMT-LIB code can only verify that a given ``next_state`` is correct.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: diff of ``Module::write_initial()`` method
:start-at: void write_initial
@@ -396,7 +417,7 @@ an additional line declaring that everything in the file should be exported for
use; allowing the file to be treated as a Racket package with structs and
mapping function available for use externally.
-.. literalinclude:: /code_examples/functional/rosette.diff
+.. literalinclude:: /generated/functional/rosette.diff
:language: diff
:caption: relevant portion of diff of ``Backend::execute()`` method
:start-at: lang rosette/safe