diff --git a/include/verilated_random.cpp b/include/verilated_random.cpp index 6087683b1..59548dc0a 100644 --- a/include/verilated_random.cpp +++ b/include/verilated_random.cpp @@ -29,6 +29,7 @@ #include #include #include +#include // Diversity (scalar rand vars): tie each free bit to a random target via a // boolean assumption literal, then force the bits with (check-sat-assuming). @@ -265,6 +266,125 @@ private: } }; +//====================================================================== +// Solver reply protocol + +enum class VlSolverStatus : uint8_t { SAT, UNSAT, UNKNOWN, FAIL }; + +static bool isSolverError(const std::string& reply) { return reply.compare(0, 6, "(error") == 0; } + +// One non-blank reply line, trimmed; false once the solver stops answering +static bool readLine(std::istream& is, std::string& liner) { + while (std::getline(is, liner)) { + const size_t first = liner.find_first_not_of(" \t\r"); + if (first == std::string::npos) continue; + const size_t last = liner.find_last_not_of(" \t\r"); + liner = liner.substr(first, last - first + 1); + return true; + } + return false; +} + +static bool scanParenDepth(const std::string& str, int& depthr, bool& inStringr) { + for (const char c : str) { + if (inStringr) { + if (c == '"') inStringr = false; + } else if (c == '"') { + inStringr = true; + } else if (c == '(') { + ++depthr; + } else if (c == ')') { + if (depthr == 0) return false; + --depthr; + } + } + return true; +} + +// Append lines until the error s-expression started in liner is paren-balanced +static void finishErrorReply(std::istream& is, std::string& liner) { + int depth = 0; + bool inString = false; + if (!scanParenDepth(liner, depth, inString)) return; + while (depth > 0) { + std::string chunk; + if (!readLine(is, chunk)) return; + liner += ' '; + liner += chunk; + if (!scanParenDepth(chunk, depth, inString)) return; + } +} + +static void warnSolverReply(const std::string& reply) { + static bool s_warned = false; + if (s_warned) return; + s_warned = true; + const std::string msg + = "Solver did not answer with a status, so randomize() returns 0; warned once: " + reply; + VL_WARN_MT(__FILE__, __LINE__, "randomize", msg.c_str()); +} + +// Read one solver status; only a print-success echo may precede it +static VlSolverStatus readStatus(std::istream& is) { + std::string line; + while (readLine(is, line)) { + if (line == "success") continue; + if (line == "sat") return VlSolverStatus::SAT; + if (line == "unsat") return VlSolverStatus::UNSAT; + if (line == "unknown") { + static bool s_warnedUnknown = false; + if (!s_warnedUnknown) { + s_warnedUnknown = true; + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Solver returned unknown (timed out or incomplete), so randomize() " + "may return 0; warned once"); + } + return VlSolverStatus::UNKNOWN; + } + // Consume the whole error, so the next read starts on a reply boundary + if (isSolverError(line)) finishErrorReply(is, line); + warnSolverReply(line); + return VlSolverStatus::FAIL; + } + return VlSolverStatus::FAIL; +} + +// Read one complete paren-balanced s-expression, which may span lines +static bool readSExpr(std::istream& is, std::string& outr) { + outr.clear(); + std::string pre; + int depth = 0; + bool inString = false; + char c = 0; + while (is.get(c)) { + if (depth == 0) { + if (c == '(') { + if (!pre.empty()) break; + outr += c; + depth = 1; + } else if (c == '\n') { + if (pre == "success") pre.clear(); + if (!pre.empty()) break; + } else if (c != ' ' && c != '\t' && c != '\r') { + pre += c; + } + continue; + } + outr += c; + if (inString) { + if (c == '"') inString = false; + } else if (c == '"') { + inString = true; + } else if (c == '(') { + ++depth; + } else if (c == ')') { + assert(depth > 0); + if (--depth == 0) return true; + } + } + return false; +} + static VlRProcess& getSolver() { static VlRProcess s_solver; static bool s_done = false; @@ -287,9 +407,7 @@ static VlRProcess& getSolver() { s_solver << "(set-logic QF_ABV)\n"; s_solver << "(check-sat)\n"; s_solver << "(reset)\n"; - std::string s; - getline(s_solver, s); - if (s == "sat") return s_solver; + if (readStatus(s_solver) == VlSolverStatus::SAT) return s_solver; std::stringstream msg; msg << "Unable to communicate with SAT solver, please check its installation or specify a " @@ -299,8 +417,6 @@ static VlRProcess& getSolver() { msg << '\n'; const std::string str = msg.str(); VL_WARN_MT("", 0, "randomize", str.c_str()); - - while (getline(s_solver, s)) {} return s_solver; } @@ -370,33 +486,57 @@ void VlRandomVar::emitConcreteValue(std::ostream& s) const { } } int VlRandomVar::totalWidth() const { return m_width; } -static bool parseSMTNum(int obits, WDataOutP owp, const std::string& val) { - int i; - for (i = 0; val[i] && val[i] != '#'; ++i) {} - if (val[i++] != '#') return false; +// True if val is "#b/#o/#x/#h" followed by digits legal for that base +static bool validSMTNum(const std::string& val) { + size_t i = val.find('#'); + if (i == std::string::npos || ++i >= val.size()) return false; + int base; switch (val[i++]) { - case 'b': _vl_vsss_based(owp, obits, 1, &val[i], 0, val.size() - i); break; - case 'o': _vl_vsss_based(owp, obits, 3, &val[i], 0, val.size() - i); break; + case 'b': base = 2; break; + case 'o': base = 8; break; case 'h': // FALLTHRU - case 'x': _vl_vsss_based(owp, obits, 4, &val[i], 0, val.size() - i); break; - default: - VL_WARN_MT(__FILE__, __LINE__, "randomize", - "Internal: Unable to parse solver's randomized number"); - return false; + case 'x': base = 16; break; + default: return false; + } + const size_t end = val.find_last_not_of(" \t\r"); + if (end < i) return false; + for (; i <= end; ++i) { + const char c = val[i]; + int digit; + if (c >= '0' && c <= '9') { + digit = c - '0'; + } else if (c >= 'a' && c <= 'f') { + digit = c - 'a' + 10; + } else if (c >= 'A' && c <= 'F') { + digit = c - 'A' + 10; + } else { + return false; + } + if (digit >= base) return false; } return true; } -bool VlRandomVar::set(const std::string& idx, const std::string& val) const { + +// val must have passed validSMTNum +static void parseSMTNum(int obits, WDataOutP owp, const std::string& val) { + size_t i = val.find('#') + 1; + switch (val[i++]) { + case 'b': _vl_vsss_based(owp, obits, 1, &val[i], 0, val.size() - i); break; + case 'o': _vl_vsss_based(owp, obits, 3, &val[i], 0, val.size() - i); break; + default: _vl_vsss_based(owp, obits, 4, &val[i], 0, val.size() - i); break; + } +} +void VlRandomVar::set(const std::string& idx, const std::string& val) const { VlWide qowp; VL_SET_WQ(qowp, 0ULL); WDataOutP owp = qowp; const int obits = width(); VlWide qiwp; VL_SET_WQ(qiwp, 0ULL); - if (!idx.empty() && !parseSMTNum(64, qiwp, idx)) return false; + if (!idx.empty()) parseSMTNum(64, qiwp, idx); const int nidx = qiwp[0]; if (obits > VL_QUADSIZE) owp = WDataOutP::external(reinterpret_cast(datap(nidx))); - if (!parseSMTNum(obits, owp, val)) return false; + parseSMTNum(obits, owp, val); if (obits <= VL_BYTESIZE) { CData* const p = static_cast(datap(nidx)); @@ -413,7 +553,6 @@ bool VlRandomVar::set(const std::string& idx, const std::string& val) const { } else { _vl_clean_inplace_w(obits, owp); } - return true; } void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) { @@ -601,24 +740,29 @@ bool VlRandomizer::nextFlat(VlRNG& rngr, const std::vector& uniqueE relaxSoftConstraints(os); os << "(check-sat)\n"; - const bool sat = parseSolution(os); + const VlSolverStatus status = readStatus(os); - if (!sat) { + if (status != VlSolverStatus::SAT) { os << "(reset)\n"; + if (status != VlSolverStatus::UNSAT) return false; // If randc vars have used values, this may be cycle exhaustion - retry if (hasRandc && !m_randcUsedValues.empty() && attempt == 0) { m_randcUsedValues.clear(); continue; // Retry without exclusions } // Skip the unsat-core path in check-only: it re-declares vars - // without pinning, so parseSolution would clobber user state with - // the solver's free assignment. + // without pinning, so the solver's free assignment would clobber + // user state. if (m_checkOnly) return false; // Genuine unsat: report via unsat-core reportUnsatSetup(os, uniqueExprs); os << "(reset)\n"; return false; } + if (!applyModel(os)) { + os << "(reset)\n"; + return false; + } if (!m_checkOnly) { solveDiversity(rngr, os); @@ -669,58 +813,55 @@ void VlRandomizer::solveDiversityPins(VlRNG& rngr, std::iostream& os) { if (!dropped[k]) os << " a" << k; } os << "))\n"; - if (parseSolution(os)) return; + const VlSolverStatus status = readStatus(os); + if (status == VlSolverStatus::SAT) { + applyModel(os); + return; + } + // Unknown or failure: the base solution already written stands + if (status != VlSolverStatus::UNSAT) return; // get-unsat-assumptions only echoes still-active literals, // so the first in-range index is a live conflicting bit. const std::vector core = readUnsatAssumptions(os); + bool droppedOne = false; for (const int idx : core) { if (idx < npins) { dropped[idx] = true; + droppedOne = true; break; } } + if (!droppedOne) return; } } void VlRandomizer::solveDiversityXor(VlRNG& rngr, std::iostream& os) { - bool sat = true; - for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; ++i) { + for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL; ++i) { os << "(assert "; randomConstraint(os, rngr, _VL_SOLVER_HASH_LEN); os << ")\n"; os << "\n(check-sat)\n"; - sat = parseSolution(os); + if (readStatus(os) != VlSolverStatus::SAT) break; + if (!applyModel(os)) break; } } -// False once the solver is gone, so no reply loop can spin forever -static bool readNonBlankLine(std::istream& is, std::string& liner) { - do { - if (!std::getline(is, liner)) return false; - } while (liner.empty()); - return true; -} - -bool VlRandomizer::checkSat(std::iostream& os) { - std::string result; - if (!readNonBlankLine(os, result)) return false; - return result == "sat"; -} - +// Re-add softs highest-priority first, dropping incompatible ones. void VlRandomizer::relaxSoftConstraints(std::iostream& os) { - // Re-add softs highest-priority first, dropping incompatible ones. - const size_t nSoft = m_softConstraints.size(); - if (nSoft == 0) return; + if (m_softConstraints.empty()) return; os << "(push 1)\n"; for (const auto& s : m_softConstraints) os << "(assert (= #b1 " << s << "))\n"; os << "(check-sat)\n"; - if (checkSat(os)) return; + const VlSolverStatus status = readStatus(os); + if (status == VlSolverStatus::SAT || status == VlSolverStatus::FAIL) return; os << "(pop 1)\n"; for (auto it = m_softConstraints.rbegin(); it != m_softConstraints.rend(); ++it) { os << "(push 1)\n"; os << "(assert (= #b1 " << *it << "))\n"; os << "(check-sat)\n"; - if (!checkSat(os)) os << "(pop 1)\n"; + const VlSolverStatus probe = readStatus(os); + if (probe == VlSolverStatus::FAIL) return; + if (probe != VlSolverStatus::SAT) os << "(pop 1)\n"; } } @@ -729,7 +870,8 @@ static std::vector scanIntRuns(const std::string& reply) { std::vector idxs; std::string num; for (const char c : reply) { - if (std::isdigit(static_cast(c))) { + // Cap the run so a garbled reply cannot overflow std::stoi + if (std::isdigit(static_cast(c)) && num.size() < 9) { num += c; } else if (!num.empty()) { idxs.push_back(std::stoi(num)); @@ -742,10 +884,14 @@ static std::vector scanIntRuns(const std::string& reply) { std::vector VlRandomizer::readUnsatAssumptions(std::iostream& os) { os << "(get-unsat-assumptions)\n"; - std::string line; - if (!readNonBlankLine(os, line)) return {}; + std::string reply; + if (!readSExpr(os, reply)) return {}; + if (isSolverError(reply)) { + warnSolverReply(reply); + return {}; + } // The response lists only "a" literals; collect each full integer run. - return scanIntRuns(line); + return scanIntRuns(reply); } // Re-solve with named asserts so an unsat core can name the failing constraints @@ -757,15 +903,17 @@ void VlRandomizer::reportUnsatSetup(std::iostream& os, emitDeclares(os, false); emitAsserts(os, uniqueExprs, true); os << "(check-sat)\n"; - std::string status; - if (!readNonBlankLine(os, status)) return; - if (status == "unsat") reportUnsatCore(os); + if (readStatus(os) == VlSolverStatus::UNSAT) reportUnsatCore(os); } void VlRandomizer::reportUnsatCore(std::iostream& os) { os << "(get-unsat-core)\n"; std::string reply; - std::getline(os, reply); + if (!readSExpr(os, reply)) return; + if (isSolverError(reply)) { + warnSolverReply(reply); + return; + } const std::vector numbers = scanIntRuns(reply); if (Verilated::threadContextp()->warnUnsatConstr()) { for (const int n : numbers) { @@ -796,23 +944,16 @@ void VlRandomizer::reportUnsatCore(std::iostream& os) { } } -bool VlRandomizer::parseSolution(std::iostream& os) { - std::string sat; - if (!readNonBlankLine(os, sat)) return false; - if (sat == "unsat") return false; - if (sat != "sat") { - std::stringstream msg; - msg << "Internal: Solver error: " << sat; - const std::string str = msg.str(); - VL_WARN_MT(__FILE__, __LINE__, "randomize", str.c_str()); - return false; - } - +bool VlRandomizer::applyModel(std::iostream& os) { + size_t requested = 0; std::stringstream getValueStr; for (const auto& var : m_vars) { if (var.second->dimension() > 0) { auto arrVarsp = std::make_shared(m_arr_vars); var.second->setArrayInfo(arrVarsp); + requested += var.second->countMatchingElements(m_arr_vars, var.second->name()); + } else { + ++requested; } var.second->emitGetValue(getValueStr); } @@ -822,15 +963,26 @@ bool VlRandomizer::parseSolution(std::iostream& os) { return true; } os << "(get-value (" << getValueStr.str() << "))\n"; - // Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE)) - char c; - if (!(os >> c) || c != '(') { - VL_WARN_MT(__FILE__, __LINE__, "randomize", - "Internal: Unable to parse solver's response: invalid S-expression"); + std::string reply; + if (!readSExpr(os, reply)) return false; + if (isSolverError(reply)) { + warnSolverReply(reply); return false; } + std::istringstream is{reply}; + return parseModel(is, requested); +} + +bool VlRandomizer::parseModel(std::istream& is, size_t requested) { + // Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE)) + char c = 0; + is >> c; // The '(' opening the readSExpr-balanced reply + // Stage writes; commit only after the whole reply parses so failure keeps prior values + std::vector> staged; + // Every requested term must come back exactly once, whether or not it is written + std::set answered; while (true) { - if (!(os >> c)) return false; + if (VL_UNCOVERABLE(!(is >> c))) return false; // Balanced reply breaks at ')' first if (c == ')') break; if (c != '(') { VL_WARN_MT(__FILE__, __LINE__, "randomize", @@ -841,16 +993,27 @@ bool VlRandomizer::parseSolution(std::iostream& os) { std::string idx; std::string value; std::vector indices; - os >> name; + is >> name; indices.clear(); if (name == "(select") { - const std::string selectExpr = readUntilBalanced(os); + const std::string selectExpr = readUntilBalanced(is); name = parseNestedSelect(selectExpr, indices); } - std::getline(os, value, ')'); + std::getline(is, value, ')'); const auto it = m_vars.find(name); - if (it == m_vars.end()) continue; + if (it == m_vars.end()) { + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Internal: Unable to parse solver's response: unknown variable"); + return false; + } const VlRandomVar& varr = *it->second; + std::string key = name; + for (const auto& index : indices) key += index; + if (!answered.insert(key).second) { + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Internal: Unable to parse solver's response: repeated variable"); + return false; + } if (!varr.randModeIdxNone()) { // Static rand vars have their rand_mode in a class-package shared queue, // not the per-instance one. @@ -870,6 +1033,11 @@ bool VlRandomizer::parseSolution(std::iostream& os) { continue; } std::string trimmed_hex = hex_index.substr(start + 2); + if (!validSMTNum(hex_index)) { + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Internal: Unable to parse solver's response: invalid array index"); + return false; + } if (trimmed_hex.size() <= 8) { // Small numbers: <= 32 bits // Convert to decimal and output directly @@ -896,8 +1064,22 @@ bool VlRandomizer::parseSolution(std::iostream& os) { "indexed_name not found in m_arr_vars"); } } - varr.set(idx, value); + // Reject before any commit, so a bad value later in the reply cannot + // leave earlier ones written + if (!validSMTNum(value)) { + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Internal: Unable to parse solver's response: invalid value"); + return false; + } + staged.emplace_back(&varr, idx, value); } + if (answered.size() != requested) { + VL_WARN_MT(__FILE__, __LINE__, "randomize", + "Internal: Unable to parse solver's response: incomplete model"); + return false; + } + for (const auto& entry : staged) + std::get<0>(entry)->set(std::get<1>(entry), std::get<2>(entry)); return true; } @@ -1050,11 +1232,13 @@ bool VlRandomizer::solvePhases(VlRNG& rngr, const std::vector& solvedValuesr) { + std::string reply; + if (!readSExpr(os, reply)) return false; + if (isSolverError(reply)) { + warnSolverReply(reply); + return false; + } + std::istringstream is{reply}; + return parsePhaseValues(is, solvedValuesr); +} + bool VlRandomizer::parsePhaseValues(std::istream& is, std::map& solvedValuesr) { // Parse ((name value) ...): one paren-depth counter drives every match. diff --git a/include/verilated_random.h b/include/verilated_random.h index c37ae92c2..54abb2d0e 100644 --- a/include/verilated_random.h +++ b/include/verilated_random.h @@ -79,7 +79,7 @@ public: virtual void* datap(int /*idx*/) const { return m_datap; } std::uint32_t randModeIdx() const { return m_randModeIdx; } bool randModeIdxNone() const { return randModeIdx() == std::numeric_limits::max(); } - bool set(const std::string& idx, const std::string& val) const; + void set(const std::string& idx, const std::string& val) const; virtual void emitGetValue(std::ostream& s) const; virtual void emitExtract(std::ostream& s, int i) const; virtual void emitType(std::ostream& s) const; @@ -257,8 +257,9 @@ class VlRandomizer VL_NOT_FINAL { // PRIVATE METHODS void randomConstraint(std::ostream& os, VlRNG& rngr, int bits); - bool parseSolution(std::iostream& os); - bool checkSat(std::iostream& os); + // Fetch the model and write it into the registered variables. + bool applyModel(std::iostream& os); + bool parseModel(std::istream& is, size_t requested); // Assert the maximal compatible soft-constraint set onto the open session. void relaxSoftConstraints(std::iostream& os); // Indices of the "a" literals named by (get-unsat-assumptions). @@ -287,6 +288,7 @@ class VlRandomizer VL_NOT_FINAL { bool solvePhaseValues(std::iostream& os, VlRNG& rngr, const std::vector& layerVars, std::map& solvedValuesr); + bool readPhaseValues(std::iostream& os, std::map& solvedValuesr); bool parsePhaseValues(std::istream& is, std::map& solvedValuesr); public: diff --git a/test_regress/t/randomize_solver_tamper.py b/test_regress/t/randomize_solver_tamper.py index 1f3fb5398..6db7fc7e3 100755 --- a/test_regress/t/randomize_solver_tamper.py +++ b/test_regress/t/randomize_solver_tamper.py @@ -7,19 +7,67 @@ # SPDX-FileCopyrightText: 2026 Wilson Snyder # SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 # -# Forwards the SMT-LIB conversation to a real solver, then kills it. +# Forwards the SMT-LIB conversation to a real solver, tampering the replies. # # Input arguments from environment variables: -# TAMPER: none | die_at | die_status_at | mute_at | garbage_at -# die_at - kill the solver and exit, closing every pipe end -# die_status_at - same, counting sat/unsat status lines instead of models -# mute_at - close the reply pipe but keep this wrapper running -# garbage_at - replace every Nth model reply with a non-S-expression line +# TAMPER: bad_base | bad_digits | bad_index | bad_value | bare_hash | binary +# | core_junk | crlf | die_at | die_status_at | dup_model | err_assume +# | err_core | err_multiline | err_once | err_phase | err_reply +# | err_trunc | err_unbal | err_unbal_cont | garbage_assume | garbage_at +# | garbage_model | garbage_status | high_digit | indent | low_digit +# | model_trunc | multiline | mute_at | no_digits | none | octal +# | oor_assume | phase_model | phase_trunc | short_model | success +# | unknown_once | unknown_twice | unknown_var | unsupported_once +# | upper_hex +# bad_base - replace the Nth model reply with a base character that is not b, o, x or h +# bad_digits - replace the Nth model reply with one value holding digits outside its base +# bad_index - replace the first array model reply with a bad select index +# bad_value - replace the Nth model reply with one well-formed value lacking a base +# bare_hash - replace the Nth model reply with one value that is only "#" +# binary - replace the Nth model reply with binary values +# core_junk - prepend garbage to the core reply and close the pipe +# crlf - end every line with CRLF +# die_at - kill the solver at the Nth model reply and exit, closing every pipe end +# die_status_at - kill the solver at the Nth status line and exit, closing every pipe end +# dup_model - replace the Nth model reply with one answering a variable twice +# err_assume - replace the first unsat-assumptions reply with (error ...) +# err_core - replace the first unsat-core reply with (error ...) +# err_multiline - answer the Nth status with an (error ...) split over two lines +# err_once - answer the Nth status with one (error ...) line +# err_phase - replace the first phase value reply with (error ...) +# err_reply - replace the Nth S-expression reply with (error ...) +# err_trunc - answer the Nth status with an unterminated (error and close the pipe +# err_unbal - answer the Nth status with an error closing an extra paren +# err_unbal_cont - answer the Nth status with an error, the extra paren on a continuation line +# garbage_assume - answer the unsat assumptions with a non-S-expression word +# garbage_at - replace every Nth model reply with a non-S-expression line +# garbage_model - replace the Nth model reply with a partly valid one +# garbage_status - replace the Nth status with a word that is not a status +# high_digit - replace the Nth model reply with a digit valid only in a wider base +# indent - prepend whitespace to every reply line +# low_digit - replace the Nth model reply with a character below any digit or letter +# model_trunc - answer the Nth model with an unterminated reply and close the pipe +# multiline - split every S-expression reply one token per line +# mute_at - close the reply pipe at the Nth model reply but keep this wrapper running +# no_digits - replace the Nth model reply with a value whose base has no digits +# none - forward every reply unchanged +# octal - replace the Nth model reply with octal values +# oor_assume - answer the unsat assumptions with an out-of-range literal +# phase_model - replace the final phased model reply with (error ...) +# phase_trunc - answer an unterminated phase value reply and close the pipe +# short_model - replace the Nth model reply with one omitting a requested variable +# success - echo a print-success line before every reply +# unknown_once - answer the Nth status with unknown +# unknown_twice - answer two statuses with unknown +# unknown_var - replace the Nth model reply with one naming a variable never requested +# unsupported_once - answer the Nth status with unsupported +# upper_hex - replace the Nth model reply with uppercase hex digits # TAMPER_AT: reply index to act on (default 3) # pylint: disable=C0103,C0114,consider-using-with import os +import re import shutil import subprocess import sys @@ -28,6 +76,23 @@ import time mode = os.environ.get("TAMPER", "none") at = int(os.environ.get("TAMPER_AT", "3")) +# Modes acting on the TAMPER_AT'th status line rather than the Nth model reply +STATUS_MODES = ("die_status_at", "err_multiline", "err_once", "err_trunc", "err_unbal", + "err_unbal_cont", "garbage_status", "unknown_once", "unknown_twice", + "unsupported_once") +# Modes acting on the TAMPER_AT'th S-expression reply of any kind +REPLY_MODES = ("err_reply", ) +# Modes acting on the first array model reply, which arrives as (select ...) terms +SELECT_MODES = ("bad_index", ) +# phase_model acts on the final phased model; the others on any phase value reply +PHASE_MODES = ("err_phase", "phase_model", "phase_trunc") +# Modes acting on an unsat-assumptions reply, which lists a literals +ASSUME_MODES = ("err_assume", "garbage_assume", "oor_assume") +# Modes acting on an unsat-core reply, which lists cons names +CORE_MODES = ("core_junk", "err_core") +# Modes rewriting every line, so they never consume the index +STREAM_MODES = ("crlf", "indent", "multiline", "success") + def real_solver(): """Return argv for the first SMT solver found in PATH""" @@ -40,23 +105,247 @@ def real_solver(): proc = subprocess.Popen(real_solver(), stdin=sys.stdin, stdout=subprocess.PIPE, text=True) + +def emit(text): + """Write one reply line downstream, unbuffered""" + sys.stdout.write(text + ("\r\n" if mode == "crlf" else "\n")) + sys.stdout.flush() + + +def forward(text, at_start): + """Pass a real reply through, applying the whole-stream rewrites""" + # Solvers echo success per command, so never inside a wrapped S-expression + if mode == "success" and at_start: + emit("success") + if mode == "multiline" and text.startswith("(") and not text.startswith("(error"): + for tok in text.split(): + emit(tok) + elif mode == "indent": + emit(" \t" + text) + else: + emit(text) + + +def scan_depth(text, left, in_string): + """Paren depth of text, ignoring parens inside SMT string literals""" + for char in text: + if in_string: + in_string = char != '"' + elif char == '"': + in_string = True + elif char == "(": + left += 1 + elif char == ")": + left -= 1 + return left, in_string + + +def read_full(first): + """Return the complete S-expression reply that starts at first""" + chunks = [first] + left, in_string = scan_depth(first, 0, False) + while left > 0: + cont = proc.stdout.readline() + if not cont: + break + chunks.append(cont.rstrip("\n")) + left, in_string = scan_depth(cont, left, in_string) + return chunks + + +def swallow(first): + """Drop the rest of a real S-expression reply that was replaced""" + read_full(first) + + replies = 0 -acting = False +done = False +depth = 0 # Paren depth of the reply being forwarded, so wrapped ones stay intact +inside = False # Inside an SMT string literal, where parens do not nest for line in proc.stdout: line = line.rstrip("\n") - counted = line in ("sat", "unsat", - "unknown") if mode == "die_status_at" else line.startswith("((") + at_reply_start = depth == 0 + depth, inside = scan_depth(line, depth, inside) + is_status = line in ("sat", "unsat", "unknown") + if mode in STATUS_MODES: + counted = is_status + elif mode in REPLY_MODES: + # Only a first line opens a reply; a wrapped continuation is not a new one + counted = at_reply_start and line.startswith("(") + elif mode in SELECT_MODES: + counted = at_reply_start and line.startswith("(((select") + elif mode in PHASE_MODES: + counted = at_reply_start and line.startswith("((x") + elif mode in ASSUME_MODES: + counted = at_reply_start and re.match(r"\(a\d", line) is not None + elif mode in CORE_MODES: + counted = at_reply_start and line.startswith("(cons") + else: + counted = at_reply_start and line.startswith("((") if counted: replies += 1 - acting = counted and replies >= at - if acting and mode == "garbage_at": - line = "junk" - replies = 0 - sys.stdout.write(line + "\n") - sys.stdout.flush() + acting = counted and replies >= at and not done and mode not in STREAM_MODES if not acting: + forward(line, at_reply_start) continue + + done = True + + if mode == "bad_base": + emit("((a #z01) (b #x12))") + swallow(line) + continue + if mode == "bad_digits": + emit("((a #x0b) (b #xgg))") + swallow(line) + continue + if mode == "bad_index": + emit("(((select q #xgg) #x15) ((select q #x00000001) #x15)" + " ((select q #x00000002) #x15))") + swallow(line) + continue + # A well-formed reply whose second value is unusable: the first must not + # reach the variable either + if mode == "bad_value": + emit("((a #x0b) (b bogus))") + swallow(line) + continue + if mode == "bare_hash": + emit("((a #x0b) (b #))") + swallow(line) + continue + if mode == "binary": + emit("((a #b00001011) (b #b00010010))") + swallow(line) + continue + if mode == "core_junk": + emit("junk((cons0))") + proc.kill() + proc.wait() + sys.exit(0) + if mode == "dup_model": + emit("((a #x0b) (a #x0c) (b #x05))") + swallow(line) + continue + if mode == "err_assume": + emit('(error "injected assumptions error")') + swallow(line) + continue + if mode == "err_core": + emit('(error "injected core error")') + swallow(line) + continue + if mode == "err_multiline": + emit('(error "injected') + emit('multiline error")') + continue + if mode == "err_once": + emit('(error "injected command rejected")') + continue + # The first phase value reply always precedes the final phased model + if mode == "err_phase": + emit('(error "injected phase value error")') + swallow(line) + continue + if mode == "err_reply": + emit('(error "injected reply error")') + swallow(line) + continue + if mode == "err_trunc": + emit('(error "unterminated') + proc.kill() + proc.wait() + sys.exit(0) + if mode == "err_unbal": + emit('(error "unbalanced"))') + continue + if mode == "err_unbal_cont": + emit('(error "unbalanced"') + emit('))') + continue + if mode == "garbage_assume": + emit("junk") + swallow(line) + continue + # garbage_at repeats, so it re-arms instead of latching + if mode == "garbage_at": + replies = 0 + done = False + emit("junk") + continue + if mode == "garbage_model": + emit("((a #x0b) junk)") + swallow(line) + continue + if mode == "garbage_status": + emit("flurble") + continue + if mode == "high_digit": + emit("((a #x0b) (b #b2))") + swallow(line) + continue + if mode == "low_digit": + emit("((a #x0b) (b #x!))") + swallow(line) + continue + if mode == "model_trunc": + emit("((a #x0b)") + proc.kill() + proc.wait() + sys.exit(0) + if mode == "no_digits": + emit("((a #x0b) (b #x))") + swallow(line) + continue + if mode == "octal": + emit("((a #o13) (b #o12))") + swallow(line) + continue + if mode == "oor_assume": + emit("(a99999999999999)") + swallow(line) + continue + # Only the final phase queries every variable, so only that reply names y + if mode == "phase_model": + replies = 0 # Re-arm until the final phase is seen + done = False + parts = read_full(line) + if "(y " in " ".join(parts): + emit('(error "injected phased model error")') + else: + for part in parts: + forward(part, part is parts[0]) + continue + if mode == "phase_trunc": + emit("((x") + proc.kill() + proc.wait() + sys.exit(0) + if mode == "short_model": + emit("((a #x0b))") + swallow(line) + continue + if mode == "unknown_once": + emit("unknown") + continue + if mode == "unknown_twice": + emit("unknown") + done = replies >= at + 1 + continue + if mode == "unknown_var": + emit("((zzz #x01) (b #x12))") + swallow(line) + continue + if mode == "unsupported_once": + emit("unsupported") + continue + if mode == "upper_hex": + emit("((a #xAB) (b #x12))") + swallow(line) + continue + forward(line, at_reply_start) + if mode in ("die_at", "die_status_at"): proc.kill() proc.wait() diff --git a/test_regress/t/t_randomize_solver_reply.py b/test_regress/t/t_randomize_solver_reply.py new file mode 100755 index 000000000..20de56971 --- /dev/null +++ b/test_regress/t/t_randomize_solver_reply.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# This program is free software; you can redistribute it and/or modify it +# under the terms of either the GNU Lesser General Public License Version 3 +# or the Perl Artistic License Version 2.0 +# SPDX-FileCopyrightText: 2026 Wilson Snyder +# SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0 + +import vltest_bootstrap + +test.scenarios('vlt') + +if not test.have_solver: + test.skip("No constraint solver installed") + +test.compile() + +# 16 randomize calls; each entry names the reply the solver mangles +runs = [ + ('bad_base', 1, 15), # a base character that is not b, o, x or h + ('bad_digits', 1, 15), # digits outside the stated base are not a number + ('bad_index', 1, 15), # a malformed array select index + ('bad_value', 1, 15), # a value with no base must not commit the earlier one + ('bare_hash', 1, 15), # a value that is only "#" + ('binary', 1, 16), # binary values + ('core_junk', 1, 4), # garbage opens the core reply, then the pipe closes + ('crlf', 1, 16), # CRLF line endings + ('dup_model', 1, 15), # the same variable answered twice + ('err_assume', 1, 16), # error in place of the unsat assumptions + ('err_core', 1, 16), # error in place of the unsat core + ('err_multiline', 2, 15), # solver rejects a command with an error spanning two lines + ('err_once', 2, 15), # solver rejects a command instead of answering + ('err_phase', 1, 15), # error in place of an intermediate phase value reply + ('err_reply', 1, 15), # error in place of an S-expression reply + ('err_trunc', 2, 0), # unterminated error, then the pipe closes + ('err_unbal', 2, 15), # a rejection error closing more parens than it opens + ('err_unbal_cont', 2, 15), # a rejection error with the extra paren on a continuation line + ('garbage_assume', 1, 16), # a bare word in place of the unsat assumptions + ('garbage_model', 1, 15), # half-valid model must not reach the variables + ('garbage_status', 2, 15), # a word that is not a status + ('garbage_status', 8, 15), # a phased check-sat that does not answer with a status + ('high_digit', 1, 15), # a digit legal for some base but not the stated one + ('indent', 1, 16), # leading whitespace before every reply + ('low_digit', 1, 15), # a character below any digit or letter + ('model_trunc', 1, 0), # unterminated model, then the pipe closes + ('multiline', 1, 16), # S-expression split one token per line + ('no_digits', 1, 15), # a base marker with no digits after it + ('octal', 1, 16), # octal values + ('oor_assume', 1, 16), # unsat assumptions naming only an out-of-range literal + ('phase_model', 1, 15), # error in place of the final phased model + ('phase_trunc', 1, 2), # unterminated phase value reply, then the pipe closes + ('short_model', 1, 15), # a model missing a requested variable is not a model + ('success', 1, 16), # print-success echo ahead of every reply + ('unknown_once', 2, 15), # unknown answers one check-sat + ('unknown_twice', 2, 15), # a second unknown must not warn again + ('unknown_var', 1, 15), # a variable that was never requested + ('unsupported_once', 2, 15), # command not supported, so no status ever comes + ('upper_hex', 1, 16), # uppercase hex digits +] + +for mode, at, npass in runs: + logfile = test.obj_dir + '/sim_' + mode + '_' + str(at) + '.log' + test.execute(logfile=logfile, + run_env='VERILATOR_SOLVER="' + test.t_dir + '/randomize_solver_tamper.py" ' + + 'TAMPER=' + mode + ' TAMPER_AT=' + str(at)) + test.file_grep(logfile, r'NPASS=(\d+)', npass) + +test.passes() diff --git a/test_regress/t/t_randomize_solver_reply.v b/test_regress/t/t_randomize_solver_reply.v new file mode 100644 index 000000000..85db5fb9d --- /dev/null +++ b/test_regress/t/t_randomize_solver_reply.v @@ -0,0 +1,86 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed under the Creative Commons Public Domain. +// SPDX-FileCopyrightText: 2026 PlanV GmbH +// SPDX-License-Identifier: CC0-1.0 + +// verilog_format: off +`define stop $stop +`define checkd(gotv,expv) do if ((gotv) !== (expv)) begin $write("%%Error: %s:%0d: got=%0d exp=%0d\n", `__FILE__,`__LINE__, (gotv), (expv)); `stop; end while(0); +// verilog_format: on + +// Model and diversity assumption replies +class Packet; + rand bit [7:0] a; + rand bit [7:0] b; + constraint c { + a > 8'd10; + b < 8'd200; + a != b; + } +endclass + +// Soft constraint relaxation replies +class Softy; + rand bit [7:0] s; + constraint sc { + soft s == 8'd42; + s > 8'd100; + } +endclass + +// Phased solve...before replies +class Phased; + rand bit [3:0] x; + rand bit [3:0] y; + constraint order_c {solve x before y;} + constraint rel_c {y > x;} +endclass + +// Array element replies, which arrive as (select ...) terms +class Arr; + rand bit [7:0] q[3]; + constraint ac {foreach (q[i]) q[i] > 8'd20;} +endclass + +// Unsatisfiable, so the unsat core is queried +class Unsat; + rand bit [7:0] u; + constraint uc { + u > 8'd200; + u < 8'd100; + } +endclass + +module t; + initial begin + automatic Packet p = new; + automatic Softy s = new; + automatic Phased ph = new; + automatic Arr ar = new; + automatic Unsat un = new; + automatic int npass = 0; + automatic int rc; + for (int i = 0; i < 4; ++i) begin + // Below the constraint, so any model the runtime applies overwrites it + p.a = 8'd5; + rc = p.randomize(); + // A randomize that failed must leave the variable alone + if (rc != 0) npass++; + else `checkd(p.a, 8'd5); + rc = s.randomize(); + if (rc != 0) npass++; + rc = ph.randomize(); + if (rc != 0) npass++; + ar.q[0] = 8'd7; + rc = ar.randomize(); + if (rc != 0) npass++; + else `checkd(ar.q[0], 8'd7); + rc = un.randomize(); + `checkd(rc, 0); // zero-ok: constraints are unsatisfiable + end + $write("NPASS=%0d\n", npass); + $write("*-* All Finished *-*\n"); + $finish; + end +endmodule