Skip to content

Commit

Permalink
Merge pull request #17 from sillydan1/feature/cpp-parsers
Browse files Browse the repository at this point in the history
Feature/cpp parsers
  • Loading branch information
sillydan1 committed Mar 19, 2023
2 parents d804286 + 19c8f69 commit 4e80daa
Show file tree
Hide file tree
Showing 52 changed files with 1,313 additions and 1,531 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/cmake.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ jobs:
- name: Initialize Submodules
uses: snickerbockers/submodules-init@v4
- name: Install dependencies
run: sudo apt-get install -y flex bison make
run: sudo apt-get install -y flex bison make flexc++ bisonc++ libbison-dev libfl-dev cmake
- name: Create Build Environment
run: cmake -E make_directory ${{github.workspace}}/build
- name: Configure CMake
Expand Down
4 changes: 3 additions & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -36,11 +36,13 @@ cmake-build-*
.idea
build
bin
Debug/
Release/
Testing/

# editor things
.emacs*
.DS_Store
compile_commands.json
Debug/
.cache/

10 changes: 10 additions & 0 deletions .vscode/launch.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,16 @@
{
"version": "0.2.0",
"configurations": [
{
"name": "Launch demo x:=0_ms",
"type": "codelldb",
"request": "launch",
"program": "${workspaceFolder}/Debug/expr_demo",
"args": [
"-e", "x:=0_ms"
],
"cwd": "${workspaceFolder}/Debug"
},
{
"name": "Launch interpreter x := 0_ms;",
"type": "cppdbg",
Expand Down
65 changes: 32 additions & 33 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,8 @@
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.
cmake_minimum_required(VERSION 3.21)
# to generate a changelog, use: (python3 -m pip install git-changelog)
# $ git-changelog -s conventional . -o CHANGELOG.MD
project(expr VERSION 2.2.0)
cmake_minimum_required(VERSION 3.18)
project(expr VERSION 3.0.0)
include(cmake/CPM.cmake)
configure_file(src/config.h.in config.h)
set(CMAKE_CXX_STANDARD 20)
Expand All @@ -32,10 +30,12 @@ set(CXX_STANDARD_REQUIRED ON)
option(ENABLE_Z3 "Enables the download and compilation of the expr::z3_driver driver. OFF by default" OFF)

# DEPENDENCIES
# library dependencies
CPMAddPackage("gh:yalibs/[email protected]")
CPMAddPackage("gh:yalibs/[email protected]")
CPMAddPackage("gh:yalibs/[email protected]")
# demo dependencies
CPMAddPackage("gh:yalibs/[email protected]")
CPMAddPackage("gh:yalibs/[email protected]")
CPMAddPackage("gh:sillydan1/[email protected]")

if(ENABLE_Z3)
Expand All @@ -45,56 +45,53 @@ if(ENABLE_Z3)
endif()

set(${PROJECT_NAME}_BUILD_DIR ${CMAKE_CURRENT_BINARY_DIR} CACHE STRING "expr_BUILD_DIR" FORCE)
find_package(FLEX REQUIRED)
find_package(BISON REQUIRED)

add_custom_command(OUTPUT
${CMAKE_CURRENT_BINARY_DIR}/lex.l
COMMAND m4
ARGS -I ${PROJECT_SOURCE_DIR}/src/parser/lex -P ${PROJECT_SOURCE_DIR}/src/parser/lex/scanner.l > ${CMAKE_CURRENT_BINARY_DIR}/lex.l
VERBATIM)
add_custom_command(OUTPUT
${CMAKE_CURRENT_BINARY_DIR}/yacc.y
COMMAND m4
ARGS -I ${PROJECT_SOURCE_DIR}/src/parser/yacc -P ${PROJECT_SOURCE_DIR}/src/parser/yacc/parser.y > ${CMAKE_CURRENT_BINARY_DIR}/yacc.y
VERBATIM)

BISON_TARGET(expr_parser ${CMAKE_CURRENT_BINARY_DIR}/yacc.y ${CMAKE_CURRENT_BINARY_DIR}/parser.cpp)
FLEX_TARGET(expr_lexer ${CMAKE_CURRENT_BINARY_DIR}/lex.l ${CMAKE_CURRENT_BINARY_DIR}/scanner.cpp)
ADD_FLEX_BISON_DEPENDENCY(expr_lexer expr_parser)
add_library(${PROJECT_NAME} SHARED
${BISON_expr_parser_OUTPUTS}
${FLEX_expr_lexer_OUTPUTS}
src/drivers/interpreter.cpp
src/drivers/tree_interpreter.cpp
src/drivers/tree_compiler.cpp
src/drivers/compiler.cpp

src/clock.cpp
src/symbol_table.cpp
src/symbol/clock.cpp
src/symbol/symbol_table.cpp
src/operations/add.cpp
src/operations/subtract.cpp
src/operations/multiply.cpp
src/operations/divide.cpp
src/operations/modulo.cpp
src/operations/pow.cpp
src/operations/boolean.cpp)
src/operations/boolean.cpp
src/driver/evaluator.cpp
)

target_include_directories(${PROJECT_NAME} PUBLIC
${CMAKE_CURRENT_BINARY_DIR}
${CMAKE_CURRENT_BINARY_DIR}/src
${yatree_SOURCE_DIR}/include
${yatimer_SOURCE_DIR}/include
${yaoverload_SOURCE_DIR}/include
${yahashcombine_SOURCE_DIR}/include
${argvparse_SOURCE_DIR}/include
${z3_SOURCE_DIR}/src/api/c++
${z3_SOURCE_DIR}/include
src/symbol
include
src)

add_library(${PROJECT_NAME}_generic_driver SHARED src/generic-driver.cpp)
target_include_directories(${PROJECT_NAME}_generic_driver PUBLIC
${CMAKE_CURRENT_BINARY_DIR}
${CMAKE_CURRENT_BINARY_DIR}/src
${yatree_SOURCE_DIR}/include
${yatimer_SOURCE_DIR}/include
${yaoverload_SOURCE_DIR}/include
${yahashcombine_SOURCE_DIR}/include
${argvparse_SOURCE_DIR}/include
${z3_SOURCE_DIR}/src/api/c++
${z3_SOURCE_DIR}/include
src/symbol
include
src)

add_subdirectory(src/expr-lang)

if(ENABLE_Z3)
target_sources(${PROJECT_NAME} PUBLIC src/drivers/z3_driver.cpp)
target_sources(${PROJECT_NAME} PUBLIC src/driver/z3/z3-driver.cpp)
target_link_directories(${PROJECT_NAME} PUBLIC ${z3_SOURCE_DIR}/bin)
target_link_libraries(${PROJECT_NAME} z3)
target_compile_definitions(${PROJECT_NAME} PUBLIC ENABLE_Z3)
Expand All @@ -104,4 +101,6 @@ endif()

add_executable(${PROJECT_NAME}_demo src/main.cpp)
set_target_properties(${PROJECT_NAME}_demo PROPERTIES RPATH ${z3_SOURCE_DIR}/bin)
target_link_libraries(${PROJECT_NAME}_demo ${PROJECT_NAME} argvparse)
target_link_libraries(${PROJECT_NAME}_demo ${PROJECT_NAME} expr_lang argvparse ${PROJECT_NAME}_generic_driver)
target_link_libraries(${PROJECT_NAME}_generic_driver expr_lang)

90 changes: 60 additions & 30 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ This project is compiled through cmake, so you can simply configure the project
mkdir bin && cd bin
cmake .. \
-DCMAKE_BUILD_TYPE=Release \
-DENABLE_Z3=ON # z3 theorem prover is an opt-in feature. Note that compilation will take much longer if enabled
-DENABLE_Z3=ON # z3 theorem prover is an opt-in feature
make
```
Note that because the flex/bison parser is generated at compile-time, your editor might complain about some invalid
Expand All @@ -26,63 +26,93 @@ If you want to use the project in your own cmake project, simply include `expr`
with the `libexpr` library. The project is also tagged with release versions to be compatible with [cpm](https://github.com/cpm-cmake/CPM.cmake),
so if your project uses that, simply include the project like so:
```cmake
CPMAddPackage("gh:sillydan1/expr@1.4.0")
CPMAddPackage("gh:sillydan1/expr@3.0.0")
```

## Examples
Disclaimer: The examples in this section may be outdated. Look at [main.cpp](src/main.cpp) for an in-depth example of how to use the library.

This project comes with a demo command line interface called `expr_demo` so that you
can test if the project supports your expression syntax.
```
$ ./expr_demo -
a := (1 + 2 + 3 + 4);
b := one + two;
^D
a :-> 6 i
b :-> 3 i
$ ./expr_demo -m -
provide an environment. End with <<EOF>> (ctrl+d):
<<
a := 32
>>
provide an expression. End with <<EOF>> (ctrl+d):
<<
b := a / 2
>>
ast:
> b :-> ROOT[/[a 2 i ]]
evaluated:
> b :-> 16 i
z3 sat check: (apply these changes to satisfy the expression)
> not a raw rhs, cannot check for sat
```

You can also use the project directly in code like so:
```c++
using namespace expr; // All elements are in the expr:: namespace
symbol_table_t env{}; // Initialize an environment
interpreter drv{env}; // Initialize the expr interpreter with the environment
if (drv.parse("a := 32 + 2") == 0) // Parse your expressions
std::cout << drv.result; // Print the resulting symbol table
else // Parsing went wrong. Maybe bad syntax, type error or identifier not in environment
std::cout << drv.error; // Print what went wrong
expr::symbol_table_t env{}; // provide an environment for identifier lookup(s)
expr::generic_driver d{}; // instantiate default driver (make sure to link with libexpr_generic_driver.so for this
d.parse_expressions("a := 32 + 2"); // parse your expression
auto result = d.get_symbols(env); // extract the symbol-table
```

### Using The `expr::z3_driver`
If you want more direct control, or want to inject some custom code (e.g. override the `add/+` operator), you can use the direct API:
```c++
using namespace expr; // All elements are in the expr:: namespace
std::string expression = "a := 32+2"; // Some expression string
std::stringstream stream{expression}; // inputs must be wrapped in a c++ stream
ast_factory factory{}; // Initialize an overridable ast factory
declaration_tree_builder builder{}; // Initialize an overridable tree builder
scanner sc{stream, std::cerr, &factory}; // Initialize scanner with input stream - write errors to std::cerr
parser_args args{expression, &sc, &factory, &builder}; // Wrap parser arguments
if(parser{args}.parse() != 0) // Actually parse the expression(s)
throw std::logic_error(""); // something bad happened either throw or handle the error
auto result = builder.build(); // build the resulting AST(s)

// Now, we can evaluate our built AST(s)
symbol_table_t env{}; // Initialize an environment for identifier lookup
symbol_operator op{}; // Initialize an overridable operator collection
evaluator e{{env}, op}; // Initialize an evaluator tree-visitor
symbol_table_t result_env{};
for(auto& r : result.declarations) // Extract all the declarations
result_env[r.first] = e.evaluate(r.second.tree);
for(auto& s : result_env) // Print the resulting declarations
std::cout << s.first << " :-> " << s.second << "\n";
if(result.raw_expression) // If the expression is just a RHS expression, print it
std::cout << e.evaluate(result.raw_expression.value()) << "\n";
```
### Using The Z3 Functionality
If enabled, expr includes an integration with the [z3 sat solver](https://github.com/Z3Prover/z3).
By providing an initial environment and a boolean expression, the `expr::z3_driver` can provide you with an assignment
of those variables, such that the boolean expression evaluates to `true`.
By providing an initial environment, some "unknown"/assignable variables and a boolean expression,
expr can provide you with an assignment of the "unknown" variables, such that the boolean expression evaluates to `true`.
This is best explained with an example. The demo binary is a fine place to explore this driver:
```shell
$ ./expr_demo --driver z3 \
--environment "a := false; b := false; c := false" \
$ ./expr_demo --unknown-environment "a := false; b := false; c := false" \
--expression "a == !(b || c)"
```
We ask z3 to find a solution where `a` would be the same value as the expression `!(b || c)`.
Below is the result of the above query.
```
result:
a :-> false b
b :-> true b
c :-> false b
z3 sat check: (apply these changes to satisfy the expression)
> a :-> false b
> b :-> true b
> c :-> false b
```
There are in fact more than one solution to this query - you could just as well set `c :-> true` and the query would still
be satisfied.
If you want to iterate over all solutions, you can just append every solution you get to your query with a `!`-operator in front of it, and run the program again.

If you provide a query, where no assignment of the variables would lead to `true`, the driver will exclaim `"unsat"` in the terminal, and the `result` symbol table will be empty:
```shell
$ ./expr_demo --driver z3 \
--environment "a := false" \
$ ./expr_demo --unknown-environment "a := false" \
--expression "a != a" # not satisfiable
```
```
unsat
result:
z3 sat check: (apply these changes to satisfy the expression)
> unsatisfiable
```
2 changes: 1 addition & 1 deletion cmake/CPM.cmake
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
set(CPM_DOWNLOAD_VERSION 0.36.0)
set(CPM_DOWNLOAD_VERSION 0.38.0)

if(CPM_SOURCE_CACHE)
# Expand relative path. This is important if the provided path contains a tilde (~)
Expand Down
74 changes: 0 additions & 74 deletions include/drivers/driver.h

This file was deleted.

Loading

0 comments on commit 4e80daa

Please sign in to comment.