<commit_before>/**
 * DSVerifier - Digital Systems Verifier (Main)
 *
 * Federal University of Amazonas - UFAM
 *
 * Authors:       <NAME> <<EMAIL>>
 *
 * ------------------------------------------------------
 *
 * DSVerifier wrapper file for BMC's
 *
 * ------------------------------------------------------
*/

#include <iostream>
#include <stdlib.h>
#include <string>
#include <vector>
#include <cstdlib>
#include <complex>
#include <algorithm>
#include <cmath>
#include <exception>
#include <assert.h>

typedef bool _Bool;

void __DSVERIFIER_assume(_Bool expression){
	/* do nothing */
}

void __DSVERIFIER_assert(_Bool expression){
	if (expression == 0){
		 throw 0;
	}
}

#include "bmc/core/definitions.h"
#include "bmc/core/fixed-point.h"
#include "bmc/core/util.h"
#include "bmc/core/delta-operator.h"
#include "bmc/core/initialization.h"

/* eigen dependencies */
#include <unsupported/Eigen/Polynomials>
typedef Eigen::PolynomialSolver<double, Eigen::Dynamic>::RootType RootType;
typedef Eigen::PolynomialSolver<double, Eigen::Dynamic>::RootsType RootsType;

#include <fstream>
#include <boost/algorithm/string.hpp>

#define DSVERIFIER_VERSION 1.2

const char * properties [] = { "OVERFLOW", "LIMIT_CYCLE", "TIMING", "STABILITY", "MINIMUM_PHASE" };
const char * realizations [] = { "DFI", "DFII", "TDFII", "DDFI", "DDFII", "TDDFII" };
const char * bmcs [] = { "ESBMC", "CBMC" };

/* expected parameters */
unsigned int desired_x_size = 0;
std::string desired_filename;
std::string desired_property;
std::string desired_realization;
std::string desired_timeout;
std::string desired_bmc;
std::string desired_solver;
std::string desired_macro_parameters;
std::string desired_ds_id;

void help () {
	std::cout << std::endl;
	std::cout << "* * *           DSVerifier " << DSVERIFIER_VERSION << "          * * *" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "Usage:                       Purpose:" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "dsverifier [-h] [--help]           show help" << std::endl;
	std::cout << "dsverifier file.c ...              source file name" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "Options:" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "--realization <r>            set the realization for the digital system" << std::endl;
	std::cout << "                             (Available: DFI, DFII, TDFII, DDFI, DDFII, TDDFII, CDFI, CDFII, CTDFII, CDDFI, CDDFII, CTDDFII)" << std::endl;
	std::cout << "--property <p>               set the property to check in order to find violations" << std::endl;
	std::cout << "                             (Available: OVERFLOW, LIMIT_CYCLE, ZERO_INPUT_LIMIT_CYCLE, TIMING, STABILITY, and MINIMUM_PHASE)" << std::endl;
	std::cout << "--x-size <k>                 set the bound of verification" << std::endl;
	std::cout << "--bmc <b>                    set the BMC back-end for DSVerifier (ESBMC or CBMC, default is ESBMC)" << std::endl;
	std::cout << "--solver <s>                 use the specified solver in BMC back-end (e.g., boolector, z3, yices)" << std::endl;
	std::cout << "--timeout <t>                configure time limit, integer followed by {s,m,h} (for ESBMC only)" << std::endl;
	std::cout << "" << std::endl;
	exit(0);
}

void validate_selected_bmc(std::string data){
	int length = (sizeof(bmcs)/sizeof(*bmcs));
	for(int i=0; i<length; i++){
		if (bmcs[i] == data){
			desired_bmc = data;
			break;
		}
	}
	if (desired_bmc.size() == 0){
		std::cout << "invalid bmc: " << data << std::endl;
		exit(1);
	}
}

void validate_selected_realization(std::string data){
	int length = (sizeof(realizations)/sizeof(*realizations));
	for(int i=0; i<length; i++){
		if (realizations[i] == data){
			desired_realization = data;
			break;
		}
	}
	if (desired_realization.size() == 0){
		std::cout << "invalid realization: " << data << std::endl;
		exit(1);
	}
}

void validate_selected_property(std::string data){
	int length = (sizeof(properties)/sizeof(*properties));
	for(int i=0; i<length; i++){
		if (properties[i] == data){
			desired_property = data;
			break;
		}
	}
	if (desired_property.size() == 0){
		std::cout << "invalid property: " << data << std::endl;
		exit(1);
	}
}

void validate_filename(std::string file){
	std::string::size_type loc = file.find(".c", 0 );
	if( loc == std::string::npos ) {
		std::cout << file << ": failed to figure out type of file" << std::endl;
		exit(1);
	}
	desired_filename = file;
}

void show_required_argument_message(std::string parameter){
	std::cerr << parameter << " option requires one argument." << std::endl;
	exit(1);
}

void check_required_parameters(){
	if (desired_bmc.size() == 0){
		desired_bmc = "ESBMC";
	}
}

void bind_parameters(int argc, char* argv[]){
	if (argc == 1) {
		help();
		exit(1);
	}
	validate_filename(argv[1]);
	for (int i = 2; i < argc; ++i) {
		if (std::string(argv[i]) == "--help" || std::string(argv[i]) == "-h") {
			help();
		} else if (std::string(argv[i]) == "--realization") {
			if (i + 1 < argc) {
				validate_selected_realization(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		} else if (std::string(argv[i]) == "--property") {
			if (i + 1 < argc) {
				validate_selected_property(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		} else if (std::string(argv[i]) == "--x-size") {
			if (i + 1 < argc) {
				desired_x_size = std::atoi(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		} else if (std::string(argv[i]) == "--timeout") {
			if (i + 1 < argc) {
				desired_timeout = argv[++i];
			} else {
				show_required_argument_message(argv[i]);
			}
		}else if (std::string(argv[i]) == "--bmc") {
			if (i + 1 < argc) {
				validate_selected_bmc(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		}else if (std::string(argv[i]) == "--solver") {
			if (i + 1 < argc) {
				desired_solver = argv[++i];
			} else {
				show_required_argument_message(argv[i]);
			}
		} else {
			/* get macro parameters */
			std::string parameter = argv[i];
			std::string::size_type loc = parameter.find("-D", 0 );
			if( loc != std::string::npos ) {
				desired_macro_parameters += " " + parameter;
				/* check if there is an desired benchmark */
				std::string::size_type find_desired_ds_id = parameter.find("-DDS_ID=", 0 );
				if( find_desired_ds_id != std::string::npos ) {
					std::vector<std::string> parts;
					boost::split(parts, parameter, boost::is_any_of("="));
					desired_ds_id = "DS_ID==" + parts.at(1);
				}
			}else{
				std::cout << "invalid parameter: " << argv[i] << std::endl;
				exit(1);
			}
		}
	}
	check_required_parameters();
}

std::string execute_command_line(std::string command){
	FILE* pipe = popen(command.c_str(), "r");
	if (!pipe) return "ERROR";
	char buffer[128];
	std::string result = "";
	while(!feof(pipe)) {
		if(fgets(buffer, 128, pipe) != NULL){
			std::cout << buffer;
			result += buffer;
		}
	}
	pclose(pipe);
	return result;
}

std::string prepare_bmc_command_line(){
	std::string command_line;
	if (desired_bmc == "ESBMC"){
		command_line = "esbmc " + desired_filename + " --no-bounds-check --no-pointer-check --no-div-by-zero-check -DBMC=ESBMC";
		if (desired_timeout.size() > 0){
			command_line += " --timeout " + desired_timeout;
		}
	}else if (desired_bmc == "CBMC"){
		command_line = "cbmc --fixedbv " + desired_filename + " -DBMC=CBMC";
	}
	if (desired_solver.size() > 0){
		command_line += " --" + desired_solver;
	}
	if (desired_realization.size() > 0){
		command_line += " -DREALIZATION=" + desired_realization;
	}
	if (desired_property.size() > 0){
		command_line += " -DPROPERTY=" + desired_property;
	}
	if (desired_x_size > 0){
		command_line += " -DX_SIZE=" + std::to_string(desired_x_size);
	}
	command_line += desired_macro_parameters;
	return command_line;
}

digital_system ds;
implementation impl;

/* print array elements */
void cplus_print_fxp_array_elements(const char * name, fxp32_t * v, int n){
   printf("%s = {", name);
   int i;
   for(i=0; i < n; i++){
      printf(" %d ", v[i]);
   }
   printf("}\n");
}

/* print array elements */
void cplus_print_array_elements(const char * name, double * v, int n){
   printf("%s = {", name);
   int i;
   for(i=0; i < n; i++){
      printf(" %.32f ", v[i]);
   }
   printf("}\n");
}

int get_roots_from_polynomial(double polynomial[], int poly_size, std::vector<RootType> & roots){

	unsigned int size = poly_size;

	/* coefficients */
	std::vector<double> coefficients_vector;
	for (int i=0; i< poly_size; i++){
		coefficients_vector.push_back(polynomial[i]);
	}

	/* remove leading zeros */
	std::vector<double>::iterator it=coefficients_vector.begin();
	while(it != coefficients_vector.end()){
		if(*it != 0.0)
			break;
		it=coefficients_vector.erase(it);
	}

	size=coefficients_vector.size();

	/* check if there is any element left on the vector */
	if(!size){
		std::cout << std::endl << "No remaining elements in polynomial vector";
		throw std::runtime_error ("tla");
	}
	return 2;

	Eigen::VectorXd coefficients(coefficients_vector.size());<commit_msg>fixing in delta stability verification<commit_after>/**
 * DSVerifier - Digital Systems Verifier (Main)
 *
 * Federal University of Amazonas - UFAM
 *
 * Authors:       <NAME> <<EMAIL>>
 *
 * ------------------------------------------------------
 *
 * DSVerifier wrapper file for BMC's
 *
 * ------------------------------------------------------
*/

#include <iostream>
#include <stdlib.h>
#include <string>
#include <vector>
#include <cstdlib>
#include <complex>
#include <algorithm>
#include <cmath>
#include <exception>
#include <assert.h>

typedef bool _Bool;

void __DSVERIFIER_assume(_Bool expression){
	/* do nothing */
}

void __DSVERIFIER_assert(_Bool expression){
	if (expression == 0){
		 throw 0;
	}
}

#include "bmc/core/definitions.h"
#include "bmc/core/fixed-point.h"
#include "bmc/core/util.h"
#include "bmc/core/delta-operator.h"
#include "bmc/core/initialization.h"

/* eigen dependencies */
#include <unsupported/Eigen/Polynomials>
typedef Eigen::PolynomialSolver<double, Eigen::Dynamic>::RootType RootType;
typedef Eigen::PolynomialSolver<double, Eigen::Dynamic>::RootsType RootsType;

#include <fstream>
#include <boost/algorithm/string.hpp>

#define DSVERIFIER_VERSION 1.2

const char * properties [] = { "OVERFLOW", "LIMIT_CYCLE", "TIMING", "STABILITY", "MINIMUM_PHASE" };
const char * realizations [] = { "DFI", "DFII", "TDFII", "DDFI", "DDFII", "TDDFII" };
const char * bmcs [] = { "ESBMC", "CBMC" };

/* expected parameters */
unsigned int desired_x_size = 0;
std::string desired_filename;
std::string desired_property;
std::string desired_realization;
std::string desired_timeout;
std::string desired_bmc;
std::string desired_solver;
std::string desired_macro_parameters;
std::string desired_ds_id;

void help () {
	std::cout << std::endl;
	std::cout << "* * *           DSVerifier " << DSVERIFIER_VERSION << "          * * *" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "Usage:                       Purpose:" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "dsverifier [-h] [--help]           show help" << std::endl;
	std::cout << "dsverifier file.c ...              source file name" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "Options:" << std::endl;
	std::cout << "" << std::endl;
	std::cout << "--realization <r>            set the realization for the digital system" << std::endl;
	std::cout << "                             (Available: DFI, DFII, TDFII, DDFI, DDFII, TDDFII, CDFI, CDFII, CTDFII, CDDFI, CDDFII, CTDDFII)" << std::endl;
	std::cout << "--property <p>               set the property to check in order to find violations" << std::endl;
	std::cout << "                             (Available: OVERFLOW, LIMIT_CYCLE, ZERO_INPUT_LIMIT_CYCLE, TIMING, STABILITY, and MINIMUM_PHASE)" << std::endl;
	std::cout << "--x-size <k>                 set the bound of verification" << std::endl;
	std::cout << "--bmc <b>                    set the BMC back-end for DSVerifier (ESBMC or CBMC, default is ESBMC)" << std::endl;
	std::cout << "--solver <s>                 use the specified solver in BMC back-end (e.g., boolector, z3, yices)" << std::endl;
	std::cout << "--timeout <t>                configure time limit, integer followed by {s,m,h} (for ESBMC only)" << std::endl;
	std::cout << "" << std::endl;
	exit(0);
}

void validate_selected_bmc(std::string data){
	int length = (sizeof(bmcs)/sizeof(*bmcs));
	for(int i=0; i<length; i++){
		if (bmcs[i] == data){
			desired_bmc = data;
			break;
		}
	}
	if (desired_bmc.size() == 0){
		std::cout << "invalid bmc: " << data << std::endl;
		exit(1);
	}
}

void validate_selected_realization(std::string data){
	int length = (sizeof(realizations)/sizeof(*realizations));
	for(int i=0; i<length; i++){
		if (realizations[i] == data){
			desired_realization = data;
			break;
		}
	}
	if (desired_realization.size() == 0){
		std::cout << "invalid realization: " << data << std::endl;
		exit(1);
	}
}

void validate_selected_property(std::string data){
	int length = (sizeof(properties)/sizeof(*properties));
	for(int i=0; i<length; i++){
		if (properties[i] == data){
			desired_property = data;
			break;
		}
	}
	if (desired_property.size() == 0){
		std::cout << "invalid property: " << data << std::endl;
		exit(1);
	}
}

void validate_filename(std::string file){
	std::string::size_type loc = file.find(".c", 0 );
	if( loc == std::string::npos ) {
		std::cout << file << ": failed to figure out type of file" << std::endl;
		exit(1);
	}
	desired_filename = file;
}

void show_required_argument_message(std::string parameter){
	std::cerr << parameter << " option requires one argument." << std::endl;
	exit(1);
}

void check_required_parameters(){
	if (desired_bmc.size() == 0){
		desired_bmc = "ESBMC";
	}
}

void bind_parameters(int argc, char* argv[]){
	if (argc == 1) {
		help();
		exit(1);
	}
	validate_filename(argv[1]);
	for (int i = 2; i < argc; ++i) {
		if (std::string(argv[i]) == "--help" || std::string(argv[i]) == "-h") {
			help();
		} else if (std::string(argv[i]) == "--realization") {
			if (i + 1 < argc) {
				validate_selected_realization(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		} else if (std::string(argv[i]) == "--property") {
			if (i + 1 < argc) {
				validate_selected_property(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		} else if (std::string(argv[i]) == "--x-size") {
			if (i + 1 < argc) {
				desired_x_size = std::atoi(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		} else if (std::string(argv[i]) == "--timeout") {
			if (i + 1 < argc) {
				desired_timeout = argv[++i];
			} else {
				show_required_argument_message(argv[i]);
			}
		}else if (std::string(argv[i]) == "--bmc") {
			if (i + 1 < argc) {
				validate_selected_bmc(argv[++i]);
			} else {
				show_required_argument_message(argv[i]);
			}
		}else if (std::string(argv[i]) == "--solver") {
			if (i + 1 < argc) {
				desired_solver = argv[++i];
			} else {
				show_required_argument_message(argv[i]);
			}
		} else {
			/* get macro parameters */
			std::string parameter = argv[i];
			std::string::size_type loc = parameter.find("-D", 0 );
			if( loc != std::string::npos ) {
				desired_macro_parameters += " " + parameter;
				/* check if there is an desired benchmark */
				std::string::size_type find_desired_ds_id = parameter.find("-DDS_ID=", 0 );
				if( find_desired_ds_id != std::string::npos ) {
					std::vector<std::string> parts;
					boost::split(parts, parameter, boost::is_any_of("="));
					desired_ds_id = "DS_ID==" + parts.at(1);
				}
			}else{
				std::cout << "invalid parameter: " << argv[i] << std::endl;
				exit(1);
			}
		}
	}
	check_required_parameters();
}

std::string execute_command_line(std::string command){
	FILE* pipe = popen(command.c_str(), "r");
	if (!pipe) return "ERROR";
	char buffer[128];
	std::string result = "";
	while(!feof(pipe)) {
		if(fgets(buffer, 128, pipe) != NULL){
			std::cout << buffer;
			result += buffer;
		}
	}
	pclose(pipe);
	return result;
}

std::string prepare_bmc_command_line(){
	std::string command_line;
	if (desired_bmc == "ESBMC"){
		command_line = "esbmc " + desired_filename + " --no-bounds-check --no-pointer-check --no-div-by-zero-check -DBMC=ESBMC";
		if (desired_timeout.size() > 0){
			command_line += " --timeout " + desired_timeout;
		}
	}else if (desired_bmc == "CBMC"){
		command_line = "cbmc --fixedbv " + desired_filename + " -DBMC=CBMC";
	}
	if (desired_solver.size() > 0){
		command_line += " --" + desired_solver;
	}
	if (desired_realization.size() > 0){
		command_line += " -DREALIZATION=" + desired_realization;
	}
	if (desired_property.size() > 0){
		command_line += " -DPROPERTY=" + desired_property;
	}
	if (desired_x_size > 0){
		command_line += " -DX_SIZE=" + std::to_string(desired_x_size);
	}
	command_line += desired_macro_parameters;
	return command_line;
}

digital_system ds;
implementation impl;

/* print array elements */
void cplus_print_fxp_array_elements(const char * name, fxp32_t * v, int n){
   printf("%s = {", name);
   int i;
   for(i=0; i < n; i++){
      printf(" %d ", v[i]);
   }
   printf("}\n");
}

/* print array elements */
void cplus_print_array_elements(const char * name, double * v, int n){
   printf("%s = {", name);
   int i;
   for(i=0; i < n; i++){
      printf(" %.32f ", v[i]);
   }
   printf("}\n");
}

int get_roots_from_polynomial(double polynomial[], int poly_size, std::vector<RootType> & roots){

	unsigned int size = poly_size;

	/* coefficients */
	std::vector<double> coefficients_vector;
	for (int i=0; i< poly_size; i++){
		coefficients_vector.push_back(polynomial[i]);
	}

	/* remove leading zeros */
	std::vector<double>::iterator it=coefficients_vector.begin();
	while(it != coefficients_vector.end()){
		if(*it != 0.0)
			break;
		it=coefficients_vector.erase(it);
	}

	size=coefficients_vector.size();

	/* check if there is any element left on the vector */
	if(!size){
		std::cout << std::endl << "No remaining elements in polynomial vector";
		throw std::runtime_error ("tla");
	}

	Eigen::VectorXd coefficients(coefficients_vector.size());
{'fraction_non_alphanumeric': 0.19368478857770455, 'fraction_numerical': 0.005985722130697419, 'mean_word_length': 3.5940968718466197, 'pattern_counts': {'":': 2, '<': 325, '<?xml version=': 0, '>': 69, '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': '7098770', 'n_tokens_mistral': 6964, 'n_tokens_neox': 6468, 'n_words': 1439}