<commit_before>/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2020  <NAME> <<EMAIL>>
 *
 *  Permission to use, copy, modify, and/or distribute this software for any
 *  purpose with or without fee is hereby granted, provided that the above
 *  copyright notice and this permission notice appear in all copies.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *
 */

#include "kernel/yosys.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include "kernel/rtlil.h"
#include "kernel/register.h"
#include <cstdio>
#include <algorithm>

#if defined(_WIN32)
#  define WIFEXITED(x) 1
#  define WIFSIGNALED(x) 0
#  define WIFSTOPPED(x) 0
#  define WEXITSTATUS(x) ((x) & 0xff)
#  define WTERMSIG(x) SIGTERM
#else
#  include <sys/wait.h>
#endif

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

struct QbfSolutionType {
	std::vector<std::string> stdout_lines;
	dict<std::string, std::string> hole_to_value;
	bool sat;
	bool unknown; //true if neither 'sat' nor 'unsat'
	bool success; //true if exit code 0

	QbfSolutionType() : sat(false), unknown(true), success(false) {}
};

struct QbfSolveOptions {
	bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs;
	bool sat, unsat, show_smtbmc;
	std::string specialize_soln_file;
	std::string write_soln_soln_file;
	std::string dump_final_smt2_file;
	size_t argidx;
	QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
			nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false),
			show_smtbmc(false), argidx(0) {};
};

void recover_solution(QbfSolutionType &sol) {
	YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
	YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
	YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
#ifndef NDEBUG
	YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
	YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
#endif
	YS_REGEX_MATCH_TYPE m;
	bool sat_regex_found = false;
	bool unsat_regex_found = false;
	dict<std::string, bool> hole_value_recovered;
	for (const std::string &x : sol.stdout_lines) {
		if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
			std::string loc = m[1].str();
			std::string val = m[2].str();
#ifndef NDEBUG
			log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
			log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
#endif
			sol.hole_to_value[loc] = val;
		}
		else if (YS_REGEX_NS::regex_search(x, sat_regex))
			sat_regex_found = true;
		else if (YS_REGEX_NS::regex_search(x, unsat_regex))
			unsat_regex_found = true;
	}
#ifndef NDEBUG
	log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
	log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
#endif
}

dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) {
	dict<std::string, std::string> hole_loc_to_name;
	for (auto cell : module->cells()) {
		std::string cell_src = cell->get_src_attribute();
		auto pos = sol.hole_to_value.find(cell_src);
		if (pos != sol.hole_to_value.end()) {
#ifndef NDEBUG
			log_assert(cell->type.in("$anyconst", "$anyseq"));
			log_assert(cell->getPort(ID::Y).is_wire());
#endif
			hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str();
		}
	}

	return hole_loc_to_name;
}

void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) {
	std::ofstream fout(file.c_str());
	if (!fout)
		log_cmd_error("could not open solution file for writing.\n");

	dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
	for(auto &x : sol.hole_to_value)
		fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl;
}

void specialize_from_file(RTLIL::Module *module, const std::string &file) {
	YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$");
	YS_REGEX_MATCH_TYPE m;
	pool<RTLIL::Cell *> anyconsts_to_remove;
	dict<std::string, std::string> hole_name_to_value;
	std::ifstream fin(file.c_str());<commit_msg>qbfsat: Make hole name recovery more robust. Allow multiple cell types to share the same source location as long as only one `$anyconst` or `$anyseq` has that location.<commit_after>/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2020  <NAME> <<EMAIL>>
 *
 *  Permission to use, copy, modify, and/or distribute this software for any
 *  purpose with or without fee is hereby granted, provided that the above
 *  copyright notice and this permission notice appear in all copies.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *
 */

#include "kernel/yosys.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include "kernel/rtlil.h"
#include "kernel/register.h"
#include <cstdio>
#include <algorithm>

#if defined(_WIN32)
#  define WIFEXITED(x) 1
#  define WIFSIGNALED(x) 0
#  define WIFSTOPPED(x) 0
#  define WEXITSTATUS(x) ((x) & 0xff)
#  define WTERMSIG(x) SIGTERM
#else
#  include <sys/wait.h>
#endif

USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

struct QbfSolutionType {
	std::vector<std::string> stdout_lines;
	dict<std::string, std::string> hole_to_value;
	bool sat;
	bool unknown; //true if neither 'sat' nor 'unsat'
	bool success; //true if exit code 0

	QbfSolutionType() : sat(false), unknown(true), success(false) {}
};

struct QbfSolveOptions {
	bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs;
	bool sat, unsat, show_smtbmc;
	std::string specialize_soln_file;
	std::string write_soln_soln_file;
	std::string dump_final_smt2_file;
	size_t argidx;
	QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
			nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false),
			show_smtbmc(false), argidx(0) {};
};

void recover_solution(QbfSolutionType &sol) {
	YS_REGEX_TYPE sat_regex = YS_REGEX_COMPILE("Status: PASSED");
	YS_REGEX_TYPE unsat_regex = YS_REGEX_COMPILE("Solver Error.*model is not available");
	YS_REGEX_TYPE hole_value_regex = YS_REGEX_COMPILE_WITH_SUBS("Value for anyconst in [a-zA-Z0-9_]* \\(([^:]*:[^\\)]*)\\): (.*)");
#ifndef NDEBUG
	YS_REGEX_TYPE hole_loc_regex = YS_REGEX_COMPILE("[^:]*:[0-9]+.[0-9]+-[0-9]+.[0-9]+");
	YS_REGEX_TYPE hole_val_regex = YS_REGEX_COMPILE("[0-9]+");
#endif
	YS_REGEX_MATCH_TYPE m;
	bool sat_regex_found = false;
	bool unsat_regex_found = false;
	dict<std::string, bool> hole_value_recovered;
	for (const std::string &x : sol.stdout_lines) {
		if(YS_REGEX_NS::regex_search(x, m, hole_value_regex)) {
			std::string loc = m[1].str();
			std::string val = m[2].str();
#ifndef NDEBUG
			log_assert(YS_REGEX_NS::regex_search(loc, hole_loc_regex));
			log_assert(YS_REGEX_NS::regex_search(val, hole_val_regex));
#endif
			sol.hole_to_value[loc] = val;
		}
		else if (YS_REGEX_NS::regex_search(x, sat_regex))
			sat_regex_found = true;
		else if (YS_REGEX_NS::regex_search(x, unsat_regex))
			unsat_regex_found = true;
	}
#ifndef NDEBUG
	log_assert(!sol.unknown && sol.sat? sat_regex_found : true);
	log_assert(!sol.unknown && !sol.sat? unsat_regex_found : true);
#endif
}

dict<std::string, std::string> get_hole_loc_name_map(RTLIL::Module *module, const QbfSolutionType &sol) {
	dict<std::string, std::string> hole_loc_to_name;
	for (auto cell : module->cells()) {
		std::string cell_src = cell->get_src_attribute();
		auto pos = sol.hole_to_value.find(cell_src);
		if (pos != sol.hole_to_value.end() && cell->type.in("$anyconst", "$anyseq")) {
			log_assert(hole_loc_to_name.find(pos->first) == hole_loc_to_name.end());
			hole_loc_to_name[pos->first] = cell->getPort(ID::Y).as_wire()->name.str();
		}
	}

	return hole_loc_to_name;
}

void write_solution(RTLIL::Module *module, const QbfSolutionType &sol, const std::string &file) {
	std::ofstream fout(file.c_str());
	if (!fout)
		log_cmd_error("could not open solution file for writing.\n");

	dict<std::string, std::string> hole_loc_to_name = get_hole_loc_name_map(module, sol);
	for(auto &x : sol.hole_to_value)
		fout << hole_loc_to_name[x.first] << "=" << x.second << std::endl;
}

void specialize_from_file(RTLIL::Module *module, const std::string &file) {
	YS_REGEX_TYPE hole_assn_regex = YS_REGEX_COMPILE_WITH_SUBS("^(.*)=([01]+)$");
	YS_REGEX_MATCH_TYPE m;
	pool<RTLIL::Cell *> anyconsts_to_remove;
	dict<std::string, std::string> hole_name_to_value;
	std::ifstream fin(file.c_str());
{'fraction_non_alphanumeric': 0.13742473856554346, 'fraction_numerical': 0.006549065173761488, 'mean_word_length': 5.75320970042796, 'pattern_counts': {'":': 0, '<': 47, '<?xml version=': 0, '>': 45, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1030097', 'n_tokens_mistral': 3709, 'n_tokens_neox': 3520, 'n_words': 804}