-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
23 changed files
with
716 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,63 @@ | ||
cmake_minimum_required(VERSION 3.24) | ||
|
||
project(abstract_interpreter_parser | ||
HOMEPAGE_URL "https://github.com/ytsao/lattice-gym" | ||
LANGUAGES CXX) | ||
|
||
# dependencies | ||
include(FetchContent) | ||
FetchContent_Declare( | ||
cpp_peglib | ||
GIT_REPOSITORY "https://github.com/ytsao/cpp-peglib" | ||
GIT_TAG 50ea4b05e9b1d599a06e1fb22e5658695cc1f24c | ||
) | ||
FetchContent_MakeAvailable(cpp_peglib) | ||
|
||
# preparing the library | ||
add_library(abstract_interpreter_parser INTERFACE) | ||
target_include_directories(abstract_interpreter_parser INTERFACE ${cpp_peglib_SOURCE_DIR}) | ||
target_compile_options(abstract_interpreter_parser INTERFACE | ||
$<$<AND:$<COMPILE_LANGUAGE:CXX>,$<CXX_COMPILER_ID:MSVC>>:/Zc:__cplusplus /utf-8 /fp:strict> | ||
"$<$<AND:$<COMPILE_LANGUAGE:CUDA>,$<CUDA_COMPILER_ID:NVIDIA>,$<CXX_COMPILER_ID:MSVC>>:SHELL:--compiler-options /Zc:__cplusplus>" | ||
"$<$<AND:$<COMPILE_LANGUAGE:CUDA>,$<CUDA_COMPILER_ID:NVIDIA>,$<CXX_COMPILER_ID:MSVC>>:SHELL:--compiler-options /utf-8>" | ||
"$<$<AND:$<COMPILE_LANGUAGE:CUDA>,$<CUDA_COMPILER_ID:NVIDIA>,$<CXX_COMPILER_ID:MSVC>>:SHELL:--compiler-options /fp:strict>" | ||
) | ||
target_compile_options(abstract_interpreter_parser INTERFACE | ||
"$<$<AND:$<COMPILE_LANGUAGE:CUDA>,$<CUDA_COMPILER_ID:NVIDIA>>:SHELL:-diag-suppress 611>" # Warning generated by the library cpp-peglib. | ||
) | ||
|
||
# example binary | ||
add_executable(example_parser example/abstract_interpreter/parser.cpp) | ||
target_link_libraries(example_parser PRIVATE abstract_interpreter_parser) | ||
|
||
# documents | ||
find_package(Doxygen REQUIRED doxygen) | ||
|
||
set(DOXYGEN_PROJECT_NAME "Abstract Interpreter Project Library") | ||
set(DOXYGEN_BUILTIN_STL_SUPPORT YES) | ||
set(DOXYGEN_CASE_SENSE_NAMES NO) | ||
set(DOXYGEN_CLASS_DIAGRAMS NO) | ||
set(DOXYGEN_DISTRIBUTE_GROUP_DOC YES) | ||
set(DOXYGEN_EXTRACT_ALL YES) | ||
set(DOXYGEN_EXTRACT_PRIVATE NO) | ||
set(DOXYGEN_FILE_PATTERNS *.hpp) | ||
set(DOXYGEN_GENERATE_TREEVIEW YES) | ||
set(DOXYGEN_HIDE_IN_BODY_DOCS YES) | ||
set(DOXYGEN_QUIET YES) | ||
set(DOXYGEN_RECURSIVE YES) | ||
set(DOXYGEN_SORT_BY_SCOPE_NAME YES) | ||
set(DOXYGEN_SORT_MEMBER_DOCS NO) | ||
set(DOXYGEN_SOURCE_BROWSER NO) | ||
set(DOXYGEN_STRIP_CODE_COMMENTS NO) | ||
set(DOXYGEN_USE_MATHJAX YES) | ||
set(DOXYGEN_EXTRA_PACKAGES stmaryrd) | ||
set(DOXYGEN_EXCLUDE_SYMBOLS = impl) | ||
set(DOXYGEN_ENABLE_PREPROCESSING YES) | ||
set(DOXYGEN_PREDEFINED __NVCC__) | ||
set(DOXYGEN_REFERENCED_BY_RELATION NO) | ||
set(DOXYGEN_REFERENCES_RELATION NO) | ||
|
||
doxygen_add_docs(doc_abstract_interpreter_parsing | ||
"include/" | ||
ALL | ||
COMMENT "Generate HTML documentation") |
10 changes: 10 additions & 0 deletions
10
abstract_interpreter/example/abstract_interpreter/parser.cpp
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
|
||
// (1) Include the header file | ||
#include "../../include/parser.hpp" | ||
|
||
int main(){ | ||
AbstractInterpreterParser AIParser; | ||
AIParser.parse(" (-1+2)*3"); | ||
// AIParser.parse("-1+(1+2)*3- -1"); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,104 @@ | ||
|
||
#ifndef ABSTRACT_INTERPRETER_PARSER_HPP | ||
#define ABSTRACT_INTERPRETER_PARSER_HPP | ||
|
||
|
||
#include "peglib.h" | ||
#include <assert.h> | ||
#include <iostream> | ||
|
||
// copyright 2024 Yi-Nung Tsao | ||
class AbstractInterpreterParser{ | ||
using SV = peg::SemanticValues; | ||
|
||
public: | ||
void parse(const std::string& input){ | ||
// peg::parser parser(R"( | ||
// Statements <- (VariableDecl / Assignment /Comment)+ | ||
|
||
// Identifier <- < [a-zA-Z_][a-zA-Z0-9_]* > | ||
// Integer <- < [+-]? [0-9]+ > | ||
// VariableDecl <- 'int' (Identifier)+ ('=' Integer)? ';' | ||
|
||
// Assignment <- Identifier '=' (Integer / Additive / Substractive / Multiplicative / Division ) ';' | ||
|
||
// Additive <- Multiplicative '+' Additive / Multiplicative | ||
// Substractive <- Multiplicative '-' Additive / Substractive / Multiplicative | ||
// Multiplicative <- Primary '*' Multiplicative / Primary | ||
// Division <- Primary '/' Primary | ||
// Primary <- '(' Additive ')' / Integer / Identifier | ||
|
||
// ~Comment <- '//' [^\n\r]* [ \n\r\t]* | ||
// %whitespace <- [ \n\r\t]* | ||
// )"); | ||
|
||
peg::parser parser(R"( | ||
Statements <- (VariableDecl / Assignment / Additive / Multiplicative)+ | ||
Identifier <- < [a-zA-Z_][a-zA-Z0-9_]* > | ||
Integer <- < [+-]? [0-9]+ > | ||
Arithemetics <- '+' / '-' / '*' / '/' / '%' | ||
BinaryOperators <- '==' / '!=' / '>' / '>=' / '<' / '<=' | ||
VariableDecl <- 'int' Identifier ('=' Integer)? ';' | ||
Assignment <- ( Identifier '=' Expression ) / ( Identifier'++' ) ';' | ||
Expression <- Additive / Substractive / Multiplicative / Division / Primary | ||
Additive <- Multiplicative '+' Additive / Multiplicative | ||
Substractive <- Multiplicative '-' Additive / Multiplicative | ||
Multiplicative <- Primary '*' Multiplicative / Primary | ||
Division <- Multiplicative '/' Identifier | ||
Primary <- '(' Additive ')' / Integer / Identifier | ||
# If-Else, While-Loop | ||
If_Else <- '' | ||
While_Loop <- '' | ||
%whitespace <- [ \n\r\t]* | ||
)"); | ||
|
||
assert(static_cast<bool>(parser) == true); | ||
|
||
// setup actions | ||
parser["Integer"] = [](const SV& sv){ | ||
return sv.token_to_number<int>(); | ||
}; | ||
parser["Additive"] = [](const SV &sv){ | ||
switch (sv.choice()) | ||
{ | ||
case 0: | ||
return std::any_cast<int>(sv[0]) + std::any_cast<int>(sv[1]); | ||
default: | ||
return std::any_cast<int>(sv[0]); | ||
} | ||
}; | ||
parser["Substractive"] = [](const SV &sv){ | ||
switch (sv.choice()) | ||
{ | ||
case 0: | ||
return std::any_cast<int>(sv[0]) - std::any_cast<int>(sv[1]); | ||
default: | ||
return std::any_cast<int>(sv[0]); | ||
} | ||
}; | ||
parser["Multiplicative"] = [](const SV &sv){ | ||
switch (sv.choice()) | ||
{ | ||
case 0: | ||
return std::any_cast<int>(sv[0]) * std::any_cast<int>(sv[1]); | ||
default: | ||
return std::any_cast<int>(sv[0]); | ||
} | ||
}; | ||
parser["Integer"] = [](const SV &sv){ | ||
return sv.token_to_number<int>(); | ||
}; | ||
|
||
parser.enable_packrat_parsing(); | ||
int val; | ||
parser.parse(input, val); | ||
|
||
std::cout << val << std::endl; | ||
} | ||
}; | ||
|
||
#endif |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpratation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Caclul arithmetique 1. */ | ||
/* On cherche ici a tester les fonctions arithmetiques des domaines */ | ||
/* abstraits. */ | ||
/*******************************************************************/ | ||
|
||
int a, b, c, d, e, f; | ||
|
||
void main() { | ||
|
||
a = 23; | ||
b = 5; | ||
|
||
c = a + b; | ||
d = a + c; | ||
e = d + c + f; | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpratation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Caclul arithmetique 1. */ | ||
/* On cherche ici a tester les fonctions arithmetiques des domaines */ | ||
/* abstraits. */ | ||
/*******************************************************************/ | ||
|
||
int a, b, c, d, e; | ||
|
||
void main() { | ||
|
||
/*!npk a between 10 and 100*/ | ||
/*!npk b between 0 and 47*/ | ||
|
||
c = a + b; | ||
d = a * c; | ||
e = d - c; | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
|
||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpretation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Caclul arithmetique 2. Expressions non lineaires. */ | ||
/* On cherche ici à les fonctions arithmétiques des domaines */ | ||
/* abstraits. */ | ||
/*******************************************************************/ | ||
|
||
int x,y,z; | ||
|
||
void main() { | ||
|
||
/*!npk x between 0 and 1 */ | ||
/*!npk y between 4 and 5 */ | ||
|
||
z = 2*x*x - 3*y + 6; | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
|
||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpretation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficultes que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Caclul arithmetique 3. Division. */ | ||
/* On cherche ici a tester les fonctions arithmetiques des domaine */ | ||
/* abstraits. Attention a la maniere de gerer les divisions par 0 */ | ||
/*******************************************************************/ | ||
|
||
int x,y,z,t; | ||
|
||
void main() { | ||
|
||
/*!npk x between 2 and 3 */ | ||
/*!npk y between 4 and 5 */ | ||
|
||
t = x-x; | ||
z = (3*y*y+x)/t; | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
/*******************************************************************/ | ||
/* Cas d'études pour le projet du cours d'interprétation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Une boucle pas si simple. */ | ||
/* N'oubliez pas que sur la plupart des architectures, les entiers */ | ||
/* sont codes sur 32 bits */ | ||
/*******************************************************************/ | ||
|
||
int x; | ||
int i; | ||
|
||
void main() | ||
{ | ||
x = 2147483640; | ||
i = 1000; | ||
x = x+i; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpretation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Branchement conditionnel 0. Valeur absolue. */ | ||
/* On cherche ici a tester les fonctions de transfert liees aux */ | ||
/* test abstraits. On doit pouvoir prouver que y est positif en */ | ||
/* en sortie du programme. */ | ||
/*******************************************************************/ | ||
|
||
int x,y; | ||
|
||
void main() { | ||
|
||
/*!npk x between 1 and 7 */ | ||
x=x-2; | ||
|
||
if (x < 0) | ||
y=-x; | ||
else | ||
y = x; | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpretation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Branchement conditionnel 1. */ | ||
/* On cherche ici a tester les fonctions de transfert liees aux */ | ||
/* test abstraits. */ | ||
/*******************************************************************/ | ||
|
||
int i,j; | ||
int x,y,z; | ||
|
||
void main() { | ||
|
||
/*!npk x between 1 and 5 */ | ||
|
||
z = 1; | ||
j = 1; | ||
|
||
if (i < 0) | ||
j = 15/i; | ||
|
||
if (x > 0) | ||
{ | ||
y = 1/x; | ||
z = x; | ||
} | ||
|
||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,31 @@ | ||
/*******************************************************************/ | ||
/* Cas d'etudes pour le projet du cours d'interpretation abstraite */ | ||
/* Ecrit par Olivier Bouissou ([email protected]) */ | ||
/* Le but de ces cas d'etudes est de vous permettre de tester */ | ||
/* votre projet sur des exemples de programmes contenant chacun */ | ||
/* une difficulte que vous devriez rencontrer. */ | ||
/*******************************************************************/ | ||
/* Branchement conditionnel 2. Expression dans les tests. */ | ||
/* On cherche ici a tester les fonctions de transfert liees aux */ | ||
/* test abstraits. On doit avoir, a la fin, t=1. */ | ||
/*******************************************************************/ | ||
|
||
|
||
int x,y,z,t; | ||
|
||
void main() { | ||
|
||
/*!npk x between 1 and 5 */ | ||
/*!npk y between 2 and 10 */ | ||
|
||
|
||
if ( x < y) | ||
z=x*x; | ||
else | ||
z=y*y; | ||
|
||
if (z<=x*y) | ||
t=1; | ||
else | ||
t=0; | ||
} |
Oops, something went wrong.