diff --git a/CMakeLists.txt b/CMakeLists.txt index 0f62152230f..fea650dbac1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -69,7 +69,6 @@ set_target_properties( langapi linking miniBDD - mmcc pointer-analysis solvers test-bigint diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8e87949943c..4022889e456 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -91,7 +91,6 @@ add_subdirectory(jsil) add_subdirectory(json) add_subdirectory(langapi) add_subdirectory(linking) -add_subdirectory(memory-models) add_subdirectory(pointer-analysis) add_subdirectory(solvers) add_subdirectory(util) diff --git a/src/Makefile b/src/Makefile index 8797575357c..a75535d49bc 100644 --- a/src/Makefile +++ b/src/Makefile @@ -14,7 +14,6 @@ DIRS = analyses \ json \ langapi \ linking \ - memory-models \ pointer-analysis \ solvers \ util \ diff --git a/src/memory-models/CMakeLists.txt b/src/memory-models/CMakeLists.txt deleted file mode 100644 index 9cb6152a86f..00000000000 --- a/src/memory-models/CMakeLists.txt +++ /dev/null @@ -1,13 +0,0 @@ -generic_bison(mm) -generic_flex(mm) - -file(GLOB_RECURSE sources "*.cpp" "*.h") -add_library(mmcc - ${sources} - ${BISON_parser_OUTPUTS} - ${FLEX_scanner_OUTPUTS} -) - -generic_includes(mmcc) - -target_link_libraries(mmcc util) diff --git a/src/memory-models/Makefile b/src/memory-models/Makefile deleted file mode 100644 index 3b8587611c8..00000000000 --- a/src/memory-models/Makefile +++ /dev/null @@ -1,48 +0,0 @@ -SRC = mm2cpp.cpp \ - mm_lex.yy.cpp \ - mm_parser.cpp \ - mm_y.tab.cpp \ - mmcc_main.cpp \ - mmcc_parse_options.cpp \ - # Empty last line - -OBJ += ../big-int/big-int$(LIBEXT) \ - ../ansi-c/ansi-c$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../util/util$(LIBEXT) - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = memory_models$(LIBEXT) \ - mm_y.tab.h mm_y.tab.cpp mm_lex.yy.cpp mm_y.tab.cpp.output mm_y.output - -all: mmcc$(EXEEXT) - -############################################################################### - -mm_y.tab.cpp: parser.y - $(YACC) $(YFLAGS) $$flags -pyymm -d parser.y -o $@ - -mm_y.tab.h: mm_y.tab.cpp - if [ -e mm_y.tab.hpp ] ; then mv mm_y.tab.hpp mm_y.tab.h ; else \ - mv mm_y.tab.cpp.h mm_y.tab.h ; fi - -mm_lex.yy.cpp: scanner.l - $(LEX) -Pyymm -o$@ scanner.l - -# extra dependencies -mm_y.tab$(OBJEXT): mm_y.tab.cpp mm_y.tab.h -mm_lex.yy$(OBJEXT): mm_y.tab.cpp mm_lex.yy.cpp mm_y.tab.h - -############################################################################### - -generated_files: mm_y.tab.cpp mm_lex.yy.cpp mm_y.tab.h - -############################################################################### - -mmcc$(EXEEXT): $(OBJ) - $(LINKBIN) diff --git a/src/memory-models/README.md b/src/memory-models/README.md deleted file mode 100644 index 5eadb681177..00000000000 --- a/src/memory-models/README.md +++ /dev/null @@ -1,6 +0,0 @@ -\ingroup module_hidden -\defgroup memory-models memory-models - -# Folder memory-models - -`memory-models` contains tools related to weak memory models. diff --git a/src/memory-models/cat-files/pso2.cat b/src/memory-models/cat-files/pso2.cat deleted file mode 100644 index 05eeb477196..00000000000 --- a/src/memory-models/cat-files/pso2.cat +++ /dev/null @@ -1,9 +0,0 @@ -"PSO" - -let fr = rf^-1;co -let com = rf | co | fr -acyclic po-loc | com as sc-per-location - -let ppo = po \ (W*R | W*W) -acyclic ppo | rfe | co | fr as pso - diff --git a/src/memory-models/cat-files/rmo2.cat b/src/memory-models/cat-files/rmo2.cat deleted file mode 100644 index 55fa4b9972d..00000000000 --- a/src/memory-models/cat-files/rmo2.cat +++ /dev/null @@ -1,15 +0,0 @@ -"RMO" - -let fr = rf^-1;co -let po-loc-llh = po-loc \ R*R -let com = rf | co | fr -acyclic po-loc-llh | com as sc-per-loc-llh -(*note: - RMO allows load-load hazard therefore we need a weaker version of - sc-per-location*) - -let dp = addr | data | ctrl -let ppo = dp -acyclic ppo | rfe | co | fr as rmo -(*note: - this forbids thin-air cycles*) diff --git a/src/memory-models/cat-files/tso2.cat b/src/memory-models/cat-files/tso2.cat deleted file mode 100644 index edaa0276af7..00000000000 --- a/src/memory-models/cat-files/tso2.cat +++ /dev/null @@ -1,14 +0,0 @@ -"TSO" - -let fr = rf^-1;co -let com = rf | co | fr -let po-loc = po & loc - -acyclic po-loc | com as sc-per-location - -let ppo = po \ W*R -let rfe = rf & ext - -acyclic ppo | rfe | co | fr as tso -(*note: - this forbids thin-air cycles*) diff --git a/src/memory-models/grammar.txt b/src/memory-models/grammar.txt deleted file mode 100644 index 11866fb73b5..00000000000 --- a/src/memory-models/grammar.txt +++ /dev/null @@ -1,100 +0,0 @@ -Identifiers ------------ - -letter ::= a … z ∣ A … Z - -digit ::= 0 … 9 - -id ::= letter { letter ∣ digit ∣ _ ∣ . ∣ - } - -predefined identifiers: - - . id (identity relation) - . po (program order) - . addr (address dependency) - . data (data dependency) - . ctrl (ctrl dependency) - . loc (relation between events having the same location) - . ext (relation between events on different threads) - . rf (read-from) - . co (coherence) - . W (set of writes) - . R (set of reads) - . F (set of fences) - . I (set of init writes) - -Expressions ------------ - -expr ::= 0 - ∣ id - ∣ expr * ∣ expr + ∣ expr ? ∣ expr ^-1 - ∣ expr | expr ∣ expr ; expr ∣ expr \ expr ∣ expr & expr - ∣ expr ++ expr # add elt to set - ∣ expr expr # function application - ∣ fun pat -> expr - ∣ let binding { and binding } in expr - ∣ let rec binding { and binding } in expr - ∣ ( expr ) ∣ begin expr end - | 'id #tag - ∣ '{' '}' | '{' expr { , expr } '}' # explicit set - ∣ () | ( expr { , expr } ) # tuples - | match expr with {} -> expr || id ++ id -> expr end # set matching - | match expr with - 'id -> expr { || 'id -> expr } [ _ -> expr ] # tag matching - -pat ::= - ∣ id - | ( params ) - -params ::= є - ∣ id { , id } - -binding ::= valbinding ∣ funbinding - -valbinding ::= pat = expr - -funbinding ::= id pat = expr - -instruction ::= let binding { and binding } - ∣ let rec binding { and binding } - ∣ [ flag ] check expr [ as id] - ∣ procedure id ( params ) = { instruction } END - ∣ call id expr [ as id ] - ∣ show expr as id - ∣ show id { , id } - ∣ unshow id { , id } - ∣ include string - - ∣ with id from expr # choice ?? - ∣ forall id in expr do { instruction } end # for loop - ∣ enum id = 'id { || 'id } # enum definition - -check ::= acyclic ∣ irreflexive ∣ empty - ∣ ~acyclic ∣ ~irreflexive ∣ ~empty - -Events, scopes and regions (Bell constructs ) --------------------------- - -The following are bell specific (ignored by cat) - -event_sets ::= events TYPE[TAGS1,..,TAGSN] - - Define legal instruction (events) annotations where: - - TYPE is R,W,F or RMW. - - TAGSi is a set of tags. - -The following definitions have additional, specific, bell interpretation. -enum regions = 'tag1 || ... || 'tagN - -enum scopes = 'tag1 || ... || 'tagN - -let wider(s) = ... - The wider function defines the scope hierarchy by its parent function that - associate the tag (of enum scopes) of the parent to the tag of a scope - -let narrower = .. - The narrower function defines the scope hierarchy by its children function. - Notice that narrower may return a set of tags. - - diff --git a/src/memory-models/mm2cpp.cpp b/src/memory-models/mm2cpp.cpp deleted file mode 100644 index 6ef3fe3bffc..00000000000 --- a/src/memory-models/mm2cpp.cpp +++ /dev/null @@ -1,212 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "mm2cpp.h" - -#include -#include - -#include -#include - -class mm2cppt -{ -public: - explicit mm2cppt(std::ostream &_out):out(_out) - { - } - - irep_idt model_name; - void operator()(const irept &); - -protected: - std::ostream &out; - typedef std::map let_valuest; - let_valuest let_values; - - static std::string text2c(const irep_idt &src); - void instruction2cpp(const codet &code, unsigned indent); - void check_acyclic(const exprt &, unsigned indent); -}; - -std::string mm2cppt::text2c(const irep_idt &src) -{ - std::string result; - result.reserve(src.size()); - - for(const auto ch : id2string(src)) - { - if(isalnum(ch)) - result+=ch; - else - result+='_'; - } - - return result; -} - -void mm2cppt::check_acyclic(const exprt &expr, unsigned indent) -{ - if(expr.id()==ID_symbol) - { - const irep_idt &identifier = to_symbol_expr(expr).get_identifier(); - let_valuest::const_iterator v_it=let_values.find(identifier); - if(v_it!=let_values.end()) - check_acyclic(v_it->second, indent); - else if(identifier=="po") - { - } - else if(identifier=="rf") - { - } - else if(identifier=="co") - { - } - else if(identifier=="loc") - { - } - else if(identifier=="int") - { - } - else if(identifier=="ext") - { - } - else if(identifier=="id") - { - } - else if(identifier=="R") - { - } - else if(identifier=="W") - { - } - else if(identifier=="F") - { - } - else if(identifier=="B") - { - } - else if(identifier=="RMW") - { - } - else if(identifier=="rmw") - { - } - else if(identifier=="IW") - { - } - else if(identifier=="FW") - { - } - else if(identifier=="M") - { - } - else if(identifier=="addr") - { - } - else if(identifier=="data") - { - } - else if(identifier=="ctrl") - { - } - else - { - throw expr.source_location().as_string()+ - ": unknown identifier `"+id2string(identifier)+"'"; - } - } - else if(expr.id()==ID_union) - { - assert(expr.operands().size()==2); - check_acyclic(expr.op0(), indent); - check_acyclic(expr.op1(), indent); - } - else - throw "acyclic cannot do "+expr.id_string(); -} - -void mm2cppt::instruction2cpp(const codet &code, unsigned indent) -{ - const irep_idt &statement=code.get_statement(); - - if(statement==ID_block) - { - forall_operands(it, code) - { - instruction2cpp(to_code(*it), indent+2); - } - } - else if(statement==ID_let) - { - assert(code.operands().size()==1); - const exprt &binding_list=code.op0(); - forall_operands(it, binding_list) - { - if(it->id()=="valbinding") - { - assert(it->operands().size()==2); - if(it->op0().id()==ID_symbol) - { - irep_idt identifier = to_symbol_expr(it->op0()).get_identifier(); - let_values[identifier]=it->op1(); - } - else - throw "cannot do tuple valbinding"; - } - else if(it->id()=="funbinding") - { - throw "cannot do funbinding"; - } - else - throw "unknown let binding"; - } - } - else if(statement=="check") - { - assert(code.operands().size()==3); - if(code.op0().id()=="acyclic") - { - check_acyclic(code.op1(), indent); - } - else - { - throw "can only do 'acyclic'"; - } - } -} - -void mm2cppt::operator()(const irept &instruction) -{ - out << "// Generated by mmcc\n"; - out << "// Model: " << model_name << '\n'; - out << '\n'; - - out << "class memory_model_" << text2c(model_name) << "t\n"; - out << "{\n"; - out << "public:\n"; - out << " void operator()();\n"; - out << "};\n"; - out << '\n'; - - out << "void memory_model_" << text2c(model_name) << "t::operator()()\n"; - out << "{\n"; - instruction2cpp(to_code(static_cast(instruction)), 0); - out << "}\n"; - out << '\n'; -} - -void mm2cpp( - const irep_idt &model_name, - const irept &instruction, - std::ostream &out) -{ - mm2cppt mm2cpp(out); - mm2cpp.model_name=model_name; - mm2cpp(instruction); -} diff --git a/src/memory-models/mm2cpp.h b/src/memory-models/mm2cpp.h deleted file mode 100644 index 99d43d15ccb..00000000000 --- a/src/memory-models/mm2cpp.h +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_MEMORY_MODELS_MM2CPP_H -#define CPROVER_MEMORY_MODELS_MM2CPP_H - -#include - -void mm2cpp( - const irep_idt &, - const irept &, - std::ostream &); - -#endif // CPROVER_MEMORY_MODELS_MM2CPP_H diff --git a/src/memory-models/mm_parser.cpp b/src/memory-models/mm_parser.cpp deleted file mode 100644 index 15b0aee55d3..00000000000 --- a/src/memory-models/mm_parser.cpp +++ /dev/null @@ -1,12 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#include "mm_parser.h" - -mm_parsert mm_parser; diff --git a/src/memory-models/mm_parser.h b/src/memory-models/mm_parser.h deleted file mode 100644 index 847e31687cf..00000000000 --- a/src/memory-models/mm_parser.h +++ /dev/null @@ -1,38 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - - -#ifndef CPROVER_MEMORY_MODELS_MM_PARSER_H -#define CPROVER_MEMORY_MODELS_MM_PARSER_H - -#include -#include - -int yymmparse(); - -class mm_parsert:public parsert -{ -public: - irep_idt model_name; - irept instruction; - - virtual bool parse() - { - return yymmparse()!=0; - } - - virtual void clear() - { - model_name.clear(); - instruction.clear(); - } -}; - -extern mm_parsert mm_parser; - -#endif // CPROVER_MEMORY_MODELS_MM_PARSER_H diff --git a/src/memory-models/mmcc_main.cpp b/src/memory-models/mmcc_main.cpp deleted file mode 100644 index 4430059e556..00000000000 --- a/src/memory-models/mmcc_main.cpp +++ /dev/null @@ -1,29 +0,0 @@ -/*******************************************************************\ - -Module: mmcc Main Module - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// mmcc Main Module - -#include "mmcc_parse_options.h" - -#include - -#ifdef _MSC_VER -int wmain(int argc, const wchar_t **argv_wide) -{ - auto vec=narrow_argv(argc, argv_wide); - auto narrow=to_c_str_array(std::begin(vec), std::end(vec)); - auto argv=narrow.data(); -#else -int main(int argc, const char **argv) -{ -#endif - mmcc_parse_optionst parse_options(argc, argv); - - return parse_options.main(); -} diff --git a/src/memory-models/mmcc_parse_options.cpp b/src/memory-models/mmcc_parse_options.cpp deleted file mode 100644 index 2bd312f5bab..00000000000 --- a/src/memory-models/mmcc_parse_options.cpp +++ /dev/null @@ -1,111 +0,0 @@ -/*******************************************************************\ - -Module: mmcc Command Line Option Processing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// mmcc Command Line Option Processing - -#include "mmcc_parse_options.h" - -#include -#include - -#include -#include - -#include "mm_parser.h" -#include "mm2cpp.h" - -mmcc_parse_optionst::mmcc_parse_optionst(int argc, const char **argv): - parse_options_baset(MMCC_OPTIONS, argc, argv) -{ -} - -/// invoke main modules -int mmcc_parse_optionst::doit() -{ - if(cmdline.isset("version")) - { - std::cout << CBMC_VERSION << '\n'; - return 0; - } - - try - { - if(cmdline.args.size()==1) - { - std::ifstream in(cmdline.args[0].c_str()); - - if(!in) - { - std::cerr << "failed to open `" << cmdline.args[0] << "'\n"; - return 2; - } - - return convert(in, cmdline.args[0]); - } - else if(cmdline.args.empty()) - { - return convert(std::cin, "stdin"); - } - else - { - usage_error(); - return 1; - } - } - catch(const char *error) - { - std::cerr << error << '\n'; - return 10; - } - catch(const std::string &error) - { - std::cerr << error << '\n'; - return 10; - } - - return 0; -} - -int mmcc_parse_optionst::convert( - std::istream &in, - const std::string &file) -{ - console_message_handlert message_handler; - - mm_parser.set_message_handler(message_handler); - mm_parser.in=∈ - mm_parser.set_file(file); - - if(mm_parser.parse()) - { - std::cerr << "parse error, giving up\n"; - return 3; - } - - mm2cpp(mm_parser.model_name, mm_parser.instruction, std::cout); - - return 0; -} - -/// display command line help -void mmcc_parse_optionst::help() -{ - // clang-format off - std::cout << '\n' << banner_string("MMCC", CBMC_VERSION) << '\n' - << - " Copyright (C) 2015-2015\n" - "\n" - "Usage: Purpose:\n" - "\n" - " mmcc [-?] [-h] [--help] show help\n" - " mmcc file.cat convert given source file\n" - " mmcc convert from stdin\n" - "\n"; - // clang-format on -} diff --git a/src/memory-models/mmcc_parse_options.h b/src/memory-models/mmcc_parse_options.h deleted file mode 100644 index 357ae91df20..00000000000 --- a/src/memory-models/mmcc_parse_options.h +++ /dev/null @@ -1,34 +0,0 @@ -/*******************************************************************\ - -Module: mmcc Command Line Option Processing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// mmcc Command Line Option Processing - -#ifndef CPROVER_MEMORY_MODELS_MMCC_PARSE_OPTIONS_H -#define CPROVER_MEMORY_MODELS_MMCC_PARSE_OPTIONS_H - -#include - -#include - -#define MMCC_OPTIONS \ - "" - -class mmcc_parse_optionst:public parse_options_baset -{ -public: - virtual int doit(); - virtual void help(); - - mmcc_parse_optionst(int argc, const char **argv); - -protected: - int convert(std::istream &, const std::string &); -}; - -#endif // CPROVER_MEMORY_MODELS_MMCC_PARSE_OPTIONS_H diff --git a/src/memory-models/module_dependencies.txt b/src/memory-models/module_dependencies.txt deleted file mode 100644 index b6eeb0c5f01..00000000000 --- a/src/memory-models/module_dependencies.txt +++ /dev/null @@ -1,3 +0,0 @@ -memory-models -langapi # should go away -util diff --git a/src/memory-models/parser.y b/src/memory-models/parser.y deleted file mode 100644 index 69ce183a7a3..00000000000 --- a/src/memory-models/parser.y +++ /dev/null @@ -1,603 +0,0 @@ -%{ - -#define PARSER mm_parser -#define YYSTYPE unsigned -#define YYSTYPE_IS_TRIVIAL 1 - -#include "mm_parser.h" - -int yymmlex(); -extern char *yymmtext; -int yymmerror(const std::string &error); - -#include "mm_y.tab.h" - -#define mto(x, y) stack(x).move_to_operands(stack(y)) - -/*** token declaration **************************************************/ -%} - -%token TOK_INVERSE "^-1" -%token TOK_MAPS_TO "->" -%token TOK_PLUSPLUS "++" -%token TOK_OROR "||" -%token TOK_LET "let" -%token TOK_AND "and" -%token TOK_IN "in" -%token TOK_DO "do" -%token TOK_MATCH "match" -%token TOK_WITH "with" -%token TOK_FROM "from" -%token TOK_ACYCLIC "acyclic" -%token TOK_IRRELFEXIVE "irreflexive" -%token TOK_EMPTY "empty" -%token TOK_FUN "fun" -%token TOK_REC "rec" -%token TOK_BEGIN "begin" -%token TOK_END "end" -%token TOK_FLAG "flag" -%token TOK_SHOW "show" -%token TOK_UNSHOW "unshow" -%token TOK_PROCEDURE "procedure" -%token TOK_ENUM "enum" -%token TOK_FORALL "forall" -%token TOK_AS "as" -%token TOK_CALL "call" -%token TOK_INCLUDE "include" -%token TOK_SET_INTERSECTION "∩" -%token TOK_SET_UNION "∪" -%token TOK_CROSS_PRODUCT "⨯" -%token TOK_EMPTY_SET "∅" - -%token TOK_IDENTIFIER -%token TOK_TAG_IDENTIFIER -%token TOK_NUMBER -%token TOK_STRING - -%left '*' "⨯" -%right ',' -%left prec_let -%left prec_fun -%left prec_app -%right '|' "∪" -%right "++" -%right ';' -%left '\\' -%right '&' "∩" -%nonassoc '~' '+' '?' -%nonassoc "^-1" - -%start grammar - -%{ -/************************************************************************/ -/*** rules **************************************************************/ -/************************************************************************/ -%} -%% - -grammar : model_name instruction_list - { - PARSER.model_name=stack($1).id(); - PARSER.instruction=stack($2); - } - ; - -model_name: - TOK_IDENTIFIER - { - $$=$1; - stack($$).id(yymmtext); - } - | TOK_STRING - { - $$=$1; - std::string s; - const char *p=yymmtext+1; - while(*p!=0 && *p!='"') { s+=*p; p++; } - stack($$).id(s); - } - ; - -simple_expr: - TOK_NUMBER - { - $$=$1; - stack($$).id(ID_constant); - stack($$).set(ID_value, yymmtext); - } - | identifier - | tag_identifier - | "begin" expr "end" - { - $$=$2; - } - | '{' expr_list_opt '}' - { - $$=$1; - stack($$).id(ID_set); - mto($$, $2); - } - | '(' expr ')' - { - $$=$2; - } - | '(' tuple ')' - { - $$=$1; - stack($$).id("tuple"); - mto($$, $2); - } - | '(' ')' - { - // only used for procedure calls - $$=$1; - stack($$).id("empty_tuple"); - } - | '_' - { - $$=$1; - stack($$).id("universe"); - } - ; - -expr: simple_expr - | expr '*' - { - $$=$2; - stack($$).id("reflexive_transitive_closure"); - mto($$, $1); - } - | expr '+' - { - $$=$2; - stack($$).id("transitive_closure"); - mto($$, $1); - } - | expr '*' simple_expr - { - // The simple_expr in the rule above is to avoid a conflict - // between a*b and a*, say followed by LET - $$=$2; - stack($$).id("cartesian_product"); - mto($$, $1); - mto($$, $3); - } - | expr "⨯" simple_expr - { - // The simple_expr in the rule above could be expr, - // as there is no ambiguity with the reflexive transitive closure. - $$=$2; - stack($$).id("cartesian_product"); - mto($$, $1); - mto($$, $3); - } - | expr '?' - { - $$=$2; - stack($$).id("reflexive_closure"); - mto($$, $1); - } - | '~' expr - { - $$=$1; - stack($$).id("complement"); - mto($$, $1); - } - | expr "^-1" - { - $$=$2; - stack($$).id("inverse"); - mto($$, $1); - } - | expr '|' expr - { - $$=$2; - stack($$).id("union"); - mto($$, $1); - mto($$, $3); - } - | expr "∪" expr - { - $$=$2; - stack($$).id("union"); - mto($$, $1); - mto($$, $3); - } - | expr ';' expr - { - $$=$2; - stack($$).id("sequence"); - mto($$, $1); - mto($$, $3); - } - | expr '\\' expr - { - $$=$2; - stack($$).id("set_minus"); - mto($$, $1); - mto($$, $3); - } - | expr '&' expr - { - $$=$2; - stack($$).id("intersection"); - mto($$, $1); - mto($$, $3); - } - | expr "∩" expr - { - $$=$2; - stack($$).id("intersection"); - mto($$, $1); - mto($$, $3); - } - | expr "++" expr - { - $$=$2; - stack($$).id("plusplus"); - mto($$, $1); - mto($$, $3); - } - | identifier simple_expr_sequence %prec prec_app - { - newstack($$); - stack($$).id(ID_function_call); - mto($$, $1); - mto($$, $2); - } - | "fun" pat "->" expr %prec prec_fun - { - $$=$1; - stack($$).id(ID_function); - mto($$, $2); - mto($$, $4); - } - | "let" pat_bind_list "in" expr %prec prec_let - { - $$=$1; - stack($$).id(ID_let); - mto($$, $2); - mto($$, $4); - } - | "let" "rec" pat_bind_list "in" expr %prec prec_let - { - $$=$1; - stack($$).id(ID_let); - mto($$, $3); - mto($$, $5); - } - | "match" expr "with" alt_opt tag_match_list "end" - { - $$=$1; - stack($$).id("match"); - mto($$, $2); - mto($$, $5); - } - ; - -alt_opt : /* nothing */ - | "||"; - ; - -flag_opt: /* nothing */ - { - newstack($$); - stack($$)=exprt(ID_nil); - } - | "flag" - { - $$=$1; - stack($$).id("flag"); - } - ; - -tag_match: expr "->" expr - { - $$=$2; - mto($$, $1); - mto($$, $3); - } - ; - -tag_match_list: - tag_match - { - newstack($$); - mto($$, $1); - } - | tag_match_list "||" tag_match - { - $$=$1; - mto($$, $3); - } - ; - -pat_bind_list: - pat_bind - { - newstack($$); - mto($$, $1); - } - | pat_bind_list "and" pat_bind - { - $$=$1; - mto($$, $3); - } - ; - -simple_expr_sequence: - simple_expr - { - newstack($$); - mto($$, $1); - } - | simple_expr_sequence simple_expr - { - $$=$1; - mto($$, $1); - } - ; - -tuple: - expr ',' expr - { - newstack($$); - mto($$, $1); - } - | tuple ',' expr - { - $$=$1; - mto($$, $1); - } - ; - -expr_list: - expr - { - newstack($$); - mto($$, $1); - } - | expr_list ',' expr - { - $$=$1; - mto($$, $1); - } - ; - -expr_list_opt: /* nothing */ - { - newstack($$); - } - | expr_list - ; - -pat : identifier - | '(' identifier_list_opt ')' - { - $$=$2; - } - ; - -identifier_list: - identifier - { - newstack($$); - mto($$, $1); - } - | identifier_list ',' identifier - { - $$=$1; - mto($$, $2); - } - ; - -identifier_list_opt: /* nothing */ - { - newstack($$); - } - | identifier_list - ; - -pat_bind: identifier '=' expr - { - $$=$2; - stack($$).id("valbinding"); - mto($$, $1); - mto($$, $3); - } - | identifier '(' identifier_list_opt ')' '=' expr - { - $$=$2; - stack($$).id("funbinding"); - mto($$, $1); - mto($$, $3); - mto($$, $6); - } - | identifier identifier '=' expr - { - $$=$3; - stack($$).id("funbinding"); - mto($$, $1); - mto($$, $2); - mto($$, $4); - } - ; - -instruction: - "let" pat_bind_list - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, ID_let); - mto($$, $2); - } - | "let" "rec" pat_bind_list - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, ID_let); - mto($$, $3); - } - | flag_opt check expr as_opt - { - newstack($$); - stack($$).id(ID_code); - stack($$).set(ID_statement, "check"); - mto($$, $2); - mto($$, $3); - mto($$, $4); - } - | "procedure" identifier '(' identifier_list_opt ')' '=' instruction_list "end" - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, "procedure"); - mto($$, $2); - mto($$, $4); - mto($$, $7); - } - | "call" identifier expr as_opt - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, "call"); - mto($$, $2); - mto($$, $3); - } - | "show" expr_list as_opt - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, "show"); - mto($$, $2); - mto($$, $3); - } - | "unshow" expr_list - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, "unshow"); - mto($$, $2); - } - | "with" identifier "from" expr - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, ID_with); - mto($$, $2); - mto($$, $4); - } - | "forall" identifier "in" expr "do" instruction_list "end" - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, ID_forall); - mto($$, $2); - mto($$, $4); - mto($$, $6); - } - | "enum" identifier '=' enum_constant_list - { - $$=$1; - stack($$).id(ID_code); - stack($$).set(ID_statement, ID_c_enum); - mto($$, $2); - mto($$, $4); - } - | "include" TOK_STRING - { - $$=$1; - } - ; - -instruction_list: - /* nothing */ - { - newstack($$); - stack($$).id(ID_code); - stack($$).set(ID_statement, ID_block); - } - | instruction_list instruction - { - $$=$1; - mto($$, $2); - } - ; - -enum_constant_list: - tag_identifier - { - newstack($$); - mto($$, $1); - } - | enum_constant_list "||" tag_identifier - { - $$=$1; - mto($$, $3); - } - ; - -as_opt : /* nothing */ - { - newstack($$); - } - | "as" identifier - { - newstack($$); - stack($$).id("as"); - mto($$, $2); - } - ; - -identifier: - TOK_IDENTIFIER - { - $$=$1; - stack($$).set(ID_identifier, yymmtext); - stack($$).id(ID_symbol); - } - ; - -tag_identifier: - TOK_TAG_IDENTIFIER - { - $$=$1; - stack($$).set(ID_identifier, yymmtext); - stack($$).id(ID_symbol); - } - ; - -check : "acyclic" - { - $$=$1; - stack($$).id("acyclic"); - } - | "irreflexive" - { - $$=$1; - stack($$).id("irreflexive"); - } - | "empty" - { - $$=$1; - stack($$).id("empty"); - } - | '~' "acyclic" - { - $$=$1; - stack($$).id("not_acyclic"); - } - | '~' "irreflexive" - { - $$=$1; - stack($$).id("not_irreflexive"); - } - | '~' "empty" - { - $$=$1; - stack($$).id("not_empty"); - } - ; - -%% diff --git a/src/memory-models/scanner.l b/src/memory-models/scanner.l deleted file mode 100644 index 9ae9bfea51f..00000000000 --- a/src/memory-models/scanner.l +++ /dev/null @@ -1,106 +0,0 @@ -%option 8bit nodefault -%option nounput -%option noinput - -%{ -#ifdef _WIN32 -#define YY_NO_UNISTD_H -static int isatty(int) { return 0; } -#endif - -#define YYSTYPE unsigned -#define PARSER mm_parser - -#include "mm_parser.h" -#include "mm_y.tab.h" - -#define loc() \ - { newstack(yymmlval); PARSER.set_source_location(stack(yymmlval)); } - -unsigned comment_nesting; - -#include -#include -#include - -%} - -%x GRAMMAR -%s COMMENT - -nl (\r\n|\r|\n) -ws (" "|\t|\r|\n) -letter [a-z]|[A-Z] -digit [0-9] -number {digit}+ -identifier {letter}({letter}|{digit}|"_"|"."|"-"|"'")* -tagidentifier "'"{letter}({letter}|{digit}|"_"|"."|"-"|"'")* -string ["][^"\n]*["] -cppcomment "//".*\n - -%% - -.|\n { BEGIN(GRAMMAR); yyless(0); } - -{ -"(*" { comment_nesting=1; BEGIN(COMMENT); } -{cppcomment} { /* ignore */ } -{string} { loc(); return TOK_STRING; } -"^-1" { loc(); return TOK_INVERSE; } -"->" { loc(); return TOK_MAPS_TO; } -"++" { loc(); return TOK_PLUSPLUS; } -"||" { loc(); return TOK_OROR; } -"flag" { loc(); return TOK_FLAG; } -"let" { loc(); return TOK_LET; } -"in" { loc(); return TOK_IN; } -"do" { loc(); return TOK_DO; } -"match" { loc(); return TOK_MATCH; } -"with" { loc(); return TOK_WITH; } -"from" { loc(); return TOK_FROM; } -"acyclic" { loc(); return TOK_ACYCLIC; } -"irreflexive" { loc(); return TOK_IRRELFEXIVE; } -"empty" { loc(); return TOK_EMPTY; } -"include" { loc(); return TOK_INCLUDE; } -"fun" { loc(); return TOK_FUN; } -"rec" { loc(); return TOK_REC; } -"begin" { loc(); return TOK_BEGIN; } -"call" { loc(); return TOK_CALL; } -"end" { loc(); return TOK_END; } -"show" { loc(); return TOK_SHOW; } -"unshow" { loc(); return TOK_UNSHOW; } -"procedure" { loc(); return TOK_PROCEDURE; } -"enum" { loc(); return TOK_ENUM; } -"forall" { loc(); return TOK_FORALL; } -"as" { loc(); return TOK_AS; } -"and" { loc(); return TOK_AND; } -"∩" { loc(); return TOK_SET_INTERSECTION; } -"∪" { loc(); return TOK_SET_UNION; } -"⨯" { loc(); return TOK_CROSS_PRODUCT; } -"∅" { loc(); return TOK_EMPTY_SET; } -{identifier} { loc(); return TOK_IDENTIFIER; } -{tagidentifier} { loc(); return TOK_TAG_IDENTIFIER; } -{number} { loc(); return TOK_NUMBER; } - -{nl} { /* ignore */ } -{ws} { /* ignore */ } -. { loc(); return yytext[0]; } -<> { yyterminate(); /* done! */ } -} - -{ -"*)" { comment_nesting--; - if(comment_nesting==0) BEGIN(GRAMMAR); } -"(*" { comment_nesting++; } -\n|. { /* ignore */ } -} - -%% - -int yywrap() { return 1; } - -int yymmerror(const std::string &error) -{ - mm_parser.parse_error(error, yytext); - return 0; -} - diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index f4590506acc..42a1d7c447f 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -460,7 +460,6 @@ IREP_ID_ONE(static_object) IREP_ID_ONE(stack_object) IREP_ID_TWO(C_is_failed_symbol, #is_failed_symbol) IREP_ID_TWO(C_failed_symbol, #failed_symbol) -IREP_ID_ONE(set) IREP_ID_ONE(friend) IREP_ID_TWO(C_friends, #friends) IREP_ID_ONE(explicit)