Awesome
V
This repository contains the grammar for the V specification language (in V.g4) and a parser that converts a given V specification into an intermediate representation called VAST.
Building
./build.sh
This step generates a library libparse_lib.a
and an executable parse
that links this library.
- A user can run the exectuable (compiled from
main.cpp
) to get an idea of how to use the V library. - A user can also include V as a submodule and include the libraries directly in their repostory.
Usage
The build/parse
executable compiled from main.cpp
invoke the V parser and visitors.
./parse <path-to-spec>
This executable takes as input a specification file, parses it using ANTLR4, converts the resulting parse tree into a VAST using VASTGenVisitor and performs various operations over it. For example, you can traverse the VAST using the ToString VAST visitor, to convert it into a string.
To illustrate, running
./parse ../example_specs/invariant1.spec
which contains the invariant specification
vars: ERC20 erc20
inv: finished(erc20.*, address(this).balance = sum(balances))
returns the following:
Parsing the specfile with ANTLR
Creating the VAST using (parse tree) VASTGenVisitor
Converting VAST to String using the VAST ToStringVisitor
import:
vars: ERC20 erc20
inv: finished(erc20.*, (address(this).balance = sum(balances)))
Converting VAST to propostional LTL using the VAST ToPropLTLVisitor
Exception: Not a Temporal Specification. ToPropLTLVisitor visits temporal specifications only.
Converting VAST to JSON using the VAST ToJsonVisitor
{"imports":{"imports":[],"ntype":"VImportList"},"inv":{"con":{"lhs":{"expr":{"args":{"args":[{"ntype":"VVarExpr","var":{"name":"this","ntype":"VID"}}],"ntype":"VArgList"},"base":null,"func":{"name":"address","ntype":"VID"},"ntype":"VFuncCallExpr"},"field":{"name":"balance","ntype":"VID"},"ntype":"VFieldAccessExpr"},"ntype":"VBinExpr","op":{"ntype":"VBinOp","op":"="},"rhs":{"args":{"args":[{"ntype":"VVarExpr","var":{"name":"balances","ntype":"VID"}}],"ntype":"VArgList"},"base":null,"func":{"name":"sum","ntype":"VID"},"ntype":"VFuncCallExpr"}},"fun":{"args":{"ntype":"VVarExpr","var":{"name":"erc20","ntype":"VID"}},"base":null,"func":{"name":"*","ntype":"VID"},"ntype":"VFunctionID"},"ntype":"VFinishedStatementExpr","pre":null},"ntype":"VInvSpec","var_decls":{"ntype":"VVarDeclList","var_decls":[{"ntype":"VVarDecl","type":{"name":"ERC20","ntype":"VType"},"var":{"name":"erc20","ntype":"VID"}}]}}
Converting VAST to JSON without using any visitor
{"imports":{"imports":[],"ntype":"VImportList"},"inv":{"con":{"lhs":{"expr":{"args":{"args":[{"ntype":"VVarExpr","var":{"name":"this","ntype":"VID"}}],"ntype":"VArgList"},"base":null,"func":{"name":"address","ntype":"VID"},"ntype":"VFuncCallExpr"},"field":{"name":"balance","ntype":"VID"},"ntype":"VFieldAccessExpr"},"ntype":"VBinExpr","op":"=","rhs":{"args":{"args":[{"ntype":"VVarExpr","var":{"name":"balances","ntype":"VID"}}],"ntype":"VArgList"},"base":null,"func":{"name":"sum","ntype":"VID"},"ntype":"VFuncCallExpr"}},"fun":{"args":null,"base":{"ntype":"VVarExpr","var":{"name":"erc20","ntype":"VID"}},"func":{"name":"*","ntype":"VID"},"ntype":"VFunctionID"},"ntype":"VFinishedStatementExpr","pre":null},"ntype":"VInvSpec","var_decls":{"ntype":"VVarDeclList","var_decls":[{"ntype":"VVarDecl","type":{"name":"ERC20","ntype":"VType"},"var":{"name":"erc20","ntype":"VID"}}]}}
Using Dockerfile
Build using:
docker build -t veridise/v:1.0 .
Run using:
docker run -d -it --name v_run veridise/v:1.0
Access the bash using:
docker exec -it v_run bash
Stop snd remove using:
docker stop v_run
docker rm v_run
Alternatively, the VSCode remote extension for Docker can also be used to develop directly within the container.
Using the VAST Visitors
This code is a part of the code present in main.cpp
. The comments explain the usage.
// Generate the ast from VASTGenVisitor as earlier
VASTGenVisitor visitor;
VAST* ast = visitor.visitSpec(tree);
// Using the ToString visitor.
vastvisitor::ToStringVisitor tsvisitor;
string vastString = std::any_cast<std::string>(tsvisitor.visit(ast));
std::cout<<vastString;
// Using the ToPropLTL visitor. Throws a const char* exception.
vastvisitor::ToPropLTLVisitor tpvisitor;
try{
string vastPropString = std::any_cast<std::string>(tpvisitor.visit(ast));
std::cout<<vastPropString;
// Extract the map
std::map<string, VAST*> atomMap = tpvisitor.getMap();
// Print the map
tpvisitor.printMap();
}
catch(const char* txtException){
std::cout<<"Exception: "<<txtException;
}
// Using the ToJson visitor.
vastvisitor::ToJsonVisitor tjvisitor;
json vastJsonString = std::any_cast<json>(tjvisitor.visit(ast));
std::cout<<vastJsonString;
Code organization
.
├── ast # VAST Classes and an ANTLR4 visitor VASTGenVisitor to generate a VAST from V.g4
├── build # Compiled files
├── cmake # ANTLR cmake files
├── docs
├── example_specs
├── libs
├── test # Automated tests
├── tools # Tools and utilities
├── visitors # Visitors over the VAST.
├── CMakeLists.txt
├── Dockerfile
├── LICENSE
├── main.cpp # Code showing the usage of the V language parser that generates VAST, and VAST visitors
├── README.md
└── V.g4 # V Specification grammar
Use V as a submodule
Add V
as a submodule of a project using:
git submodule add https://github.com/Veridise/V
Set up the project by including the following statements in the CMakeLists.txt
file:
link_directories(V)
add_subdirectory(V)
target_link_libraries(project_executable PRIVATE parse_lib)
Commit and push the changes using:
git commit -am "Add V as a submodule"
git push
Clone a project that contains submodules using:
git clone --recurse-submodules https://github.com/Veridise/V
OR
git clone https://github.com/Veridise/V
git submodule init
git submodule update
To update/sync V (or any sub-module), from within an external repo, use:
git submodule update --init --recursive --remote