AleoHQ/leo
1
1
Fork 0
mirror of https://github.com/AleoHQ/leo.git synced 2024-09-21 12:07:56 +03:00
Code Issues Packages Projects Releases Wiki Activity

merge upstream changes

Browse Source
This commit is contained in:
gluax 2022-05-25 09:21:47 -07:00
commit 8cb4b19e66
10 changed files with 168 additions and 93 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

67
.github/workflows/acl2.yml vendored
View File

@ -21,7 +21,18 @@ jobs:
- name: Generate asts
run: |
cargo -q run -p leo-test-framework --bin tgc
# This currently has to be on testnet3 to work:
cd compiler/parser
cargo -q install --path . --example parser
# To ensure full file tests,
# just do compiler tests and remove expectation: Fail tests
cd ../../tests/compiler
find . -type f -exec grep -q 'expectation *: *Fail' {} \; -delete
find . -name '*.leo' -execdir parser {} \; > /dev/null
# Show how many there are:
echo "Counts (.leo / .json):"
find . -name '*.leo' -print | wc -l
find . -name '*.json' -print | wc -l
# Pull the latest release from the leo-acl2-bin repo, and put it into the
# repo/acl2 directory. After it's done, unpack the tgz file locally.
@ -29,7 +40,7 @@ jobs:
run: |
mkdir acl2 && cd acl2;
wget $( curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
| jq -r '.assets[0].browser_download_url' )
| jq -r '.assets[].browser_download_url|scan("^.*leo-acl2--v.*\\.tgz$")' )
echo "Unpacking $(ls):"
tar -xvzf $(ls)
@ -37,28 +48,31 @@ jobs:
# Run theorem generation and checking using the prepared ASTs and the pulled and unzipped leo-acl2 tarball.
- name: Run tgc over ASTs
run: |
canonicalization_errors=();
type_inference_errors=();
num_dirs=0;
for dir in `ls tmp/tgc`;
parsing_errors=();
num_cases=0;
# Note that PWD gets reset at the beginning of each the step
# to /home/runner/work/leo/leo
acl2dir="${PWD}"/acl2
cd tests/compiler;
for tc in `find ${PWD} -name '*.leo' -print`;
do
cd tmp/tgc/$dir; # enter the directory
num_dirs=$((num_dirs + 1));
./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
cd ../../..
cd "${tc%/*}"; # enter the directory
leofile="${tc##*/}";
jsonfile="${leofile%.leo}.json";
num_cases=$((num_cases + 1));
"$acl2dir"/tgc parsing "$leofile" "$jsonfile" parsing-theorem.lisp > parsing_result.out || parsing_errors+=("$tc");
done;
echo "----------------"
echo "Ran tgc in ${num_dirs} directories."
echo "Ran tgc on ${num_cases} programs."
echo "----------------"
if [ ${#canonicalization_errors[@]} -eq 0 ]; then
echo "Canonicalization - Success!"
if [ ${#parsing_errors[@]} -eq 0 ]; then
echo "Parsing - Total Success!"
else
echo "Canonicalization Failures (total: ${#canonicalization_errors[@]}):"
for dir in ${canonicalization_errors[@]};
echo "Parsing Failures (total: ${#parsing_errors[@]}):"
for tc in ${parsing_errors[@]};
do
echo $dir
echo $tc
done;
#echo "Attaching logs:"
@ -69,24 +83,7 @@ jobs:
#done;
fi
echo "----------------"
if [ ${#type_inference_errors[@]} -eq 0 ]; then
echo "Type Inference - Success!"
else
echo "Type Inference Failures (total: ${#type_inference_errors[@]}):"
for dir in ${type_inference_errors[@]};
do
echo $dir
done;
#echo "Attaching logs:"
#for dir in ${type_inference_errors[@]};
#do
# cat tmp/tgc/$dir/type_inference_result.out
#done;
fi
if [[ ${#canonicalization_errors[@]} -ne 0 || ${#type_inference_errors[@]} -ne 0 ]]; then
if [[ ${#parsing_errors[@]} -ne 0 ]]; then
echo "----------------"
echo "Exiting with status 1 due to at least one tgc error."
exit 1

8
Cargo.lock generated
View File

@ -2006,9 +2006,9 @@ dependencies = [
[[package]]
name = "regex"
version = "1.5.5"
version = "1.5.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1a11647b6b25ff05a515cb92c365cec08801e83423a235b51e231e1808747286"
checksum = "d83f127d94bdbcda4c8cc2e50f6f84f4b611f69c902699ca385a39c3a75f9ff1"
dependencies = [
"aho-corasick",
"memchr",
@ -2023,9 +2023,9 @@ checksum = "6c230d73fb8d8c1b9c0b3135c5142a8acee3a0558fb8db5cf1cb65f8d7862132"
[[package]]
name = "regex-syntax"
version = "0.6.25"
version = "0.6.26"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f497285884f3fcff424ffc933e56d7cbca511def0c9831a7f9b5f6153e3cc89b"
checksum = "49b3de9ec5dc0a3417da371aab17d729997c15010e7fd24ff707773a33bddb64"
[[package]]
name = "remove_dir_all"

4
compiler/ast/src/expression/value.rs
View File

@ -21,14 +21,14 @@ use crate::{Char, CharValue};
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub enum ValueExpression {
// todo: deserialize values here
/// An address literal, e.g., `aleo1..`.
/// An address literal, e.g., `aleo1qnr4dkkvkgfqph0vzc3y6z2eu975wnpz2925ntjccd5cfqxtyu8s7pyjh9`.
Address(String, #[serde(with = "leo_span::span_json")] Span),
/// A boolean literal, either `true` or `false`.
Boolean(String, #[serde(with = "leo_span::span_json")] Span),
/// A char literal, e.g., `'a'`, representing a single unicode code point.
Char(CharValue),
/// A field literal, e.g., `42field`.
/// That is, a signed number followed by the keyword `field`.
/// A signed number followed by the keyword `field`.
Field(String, #[serde(with = "leo_span::span_json")] Span),
/// A group literal, either product or affine.
/// For example, `42group` or `(12, 52)group`.

2
compiler/ast/src/types/type_.rs
View File

@ -53,9 +53,9 @@ impl Type {
match (self, other) {
(Type::Address, Type::Address)
| (Type::Boolean, Type::Boolean)
| (Type::Char, Type::Char)
| (Type::Field, Type::Field)
| (Type::Group, Type::Group)
| (Type::Char, Type::Char)
| (Type::Scalar, Type::Scalar) => true,
(Type::IntegerType(left), Type::IntegerType(right)) => left.eq(right),
_ => false,

64
compiler/passes/src/type_checker/checker.rs
View File

@ -64,9 +64,10 @@ const FIELD_SCALAR_INT_TYPES: [Type; 12] = create_type_superset(FIELD_INT_TYPES,
const FIELD_GROUP_INT_TYPES: [Type; 12] = create_type_superset(FIELD_INT_TYPES, [Type::Group]);
const ALL_NUMERICAL_TYPES: [Type; 13] = create_type_superset(FIELD_GROUP_INT_TYPES, [Type::Scalar]);
const FIELD_GROUP_SCALAR_INT_TYPES: [Type; 13] = create_type_superset(FIELD_GROUP_INT_TYPES, [Type::Scalar]);
impl<'a> TypeChecker<'a> {
/// Returns a new type checker given a symbol table and error handler.
pub fn new(symbol_table: &'a mut SymbolTable<'a>, handler: &'a Handler) -> Self {
Self {
symbol_table,
@ -76,6 +77,7 @@ impl<'a> TypeChecker<'a> {
}
}
// Checks wether two given types are the same and if not emits an error.
pub(crate) fn assert_eq_types(&self, t1: Option<Type>, t2: Option<Type>, span: Span) {
match (t1, t2) {
(Some(t1), Some(t2)) if t1 != t2 => self
@ -88,6 +90,7 @@ impl<'a> TypeChecker<'a> {
}
}
/// Returns the given type if it equals the expected type or the expected type is none.
pub(crate) fn assert_type(&self, type_: Type, expected: Option<Type>, span: Span) -> Type {
if let Some(expected) = expected {
if type_ != expected {
@ -99,52 +102,39 @@ impl<'a> TypeChecker<'a> {
type_
}
pub(crate) fn assert_one_of_types(&self, type_: Option<Type>, expected: &[Type], span: Span) -> Option<Type> {
/// Emits an error to the error handler if the given type is not equal to any of the expected types.
pub(crate) fn assert_one_of_types(&self, type_: Option<Type>, expected: &[Type], span: Span) {
if let Some(type_) = type_ {
for t in expected.iter() {
if &type_ == t {
return Some(type_);
}
if !expected.iter().any(|t: &Type| t == &type_) {
self.handler.emit_err(
TypeCheckerError::expected_one_type_of(
expected.iter().map(|t| t.to_string() + ",").collect::<String>(),
type_,
span,
)
.into(),
);
}
self.handler.emit_err(
TypeCheckerError::expected_one_type_of(
expected.iter().map(|t| t.to_string() + ",").collect::<String>(),
type_,
span,
)
.into(),
);
}
type_
}
pub(crate) fn _assert_arith_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
self.assert_one_of_types(type_, &FIELD_GROUP_INT_TYPES, span)
}
pub(crate) fn _assert_field_or_int_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
/// Emits an error to the handler if the given type is not a field or integer.
pub(crate) fn assert_field_int_type(&self, type_: Option<Type>, span: Span) {
self.assert_one_of_types(type_, &FIELD_INT_TYPES, span)
}
pub(crate) fn _assert_int_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
self.assert_one_of_types(type_, &INT_TYPES, span)
}
pub(crate) fn assert_field_group_scalar_int_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
self.assert_one_of_types(type_, &ALL_NUMERICAL_TYPES, span)
}
pub(crate) fn assert_field_group_int_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
self.assert_one_of_types(type_, &FIELD_GROUP_INT_TYPES, span)
}
pub(crate) fn assert_field_scalar_int_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
/// Emits an error to the handler if the given type is not a field, scalar, or integer.
pub(crate) fn assert_field_scalar_int_type(&self, type_: Option<Type>, span: Span) {
self.assert_one_of_types(type_, &FIELD_SCALAR_INT_TYPES, span)
}
pub(crate) fn assert_field_int_type(&self, type_: Option<Type>, span: Span) -> Option<Type> {
self.assert_one_of_types(type_, &FIELD_INT_TYPES, span)
/// Emits an error to the handler if the given type is not a field, group, or integer.
pub(crate) fn assert_field_group_int_type(&self, type_: Option<Type>, span: Span) {
self.assert_one_of_types(type_, &FIELD_GROUP_INT_TYPES, span)
}
/// Emits an error to the handler if the given type is not a field, group, scalar or integer.
pub(crate) fn assert_field_group_scalar_int_type(&self, type_: Option<Type>, span: Span) {
self.assert_one_of_types(type_, &FIELD_GROUP_SCALAR_INT_TYPES, span)
}
}

BIN
docs/grammar/README.md
View File

Binary file not shown.

2
docs/grammar/abnf-grammar.txt
View File

@ -375,7 +375,7 @@ input-expression = literal
input-item = identifier ":" input-type "=" input-expression ";"
input-title = "[" identifier "]"
input-title = "[" ( %s"public" / %s"private" / %s"constant" / %s"const" ) "]"
input-section = input-title *input-item

31
tests/README.md
View File

@ -45,27 +45,32 @@ generated instead. A PR should contain changes to expectations as well as to tes
Here is the list of all possible configuration options for compiler and parser tests.
#### namespace
### namespace
```
```yaml
- Mandatory: yes
- Namespace: all
- Values: Compile / Parse
- Values: ...
```
Only two values are supported: `Parse` and `Compile`. The former is meant to be a parser test, the latter
is a full compiler test.
Several values are supported, but they vary depending on the directory you are in.
Besides the `Parse` value,
there are actually additional possible values for this field:
`ParseStatement`, `ParseExpression`, and `Token`.
Each one of them allows testing Leo parser on different levels - lexer tokens or just expressions/statements.
Parser Directory namespaces:
Compiler tests always include complete Leo programs.
- `Parse` - Test a file to check that it is a valid Leo program.
- `ParseExpression` - Test a file line by line to check that each line is a valid Leo expression.
- `ParseStatement` - Test a file consuming multiple lines till a blank line to check that it contains a valid Leo statement.
- `Serialize` - Test a file to check that it can be serialized to JSON.
- `Input` - Test an input file to check that it is a valid Leo input file.
- `Token` - Test a file line by line to check that it contains zero or more valid Leo parser tokens.
Compiler Directory namespaces:
- `Compiler` - Test a file to check that it is a valid Leo program, and it can be compiled without errors.
### expectation
```
```yaml
- Mandatory: yes
- Namespace: all
- Values: Pass / Fail
@ -77,7 +82,7 @@ you'll know that something went wrong and the test or the compiler/parser needs
### input_file (Compile)
```
```yaml
- Mandatory: no
- Namespace: Compile
- Values: <input file path>, ...
@ -87,7 +92,7 @@ This setting allows using one or more input files for the Leo program.
The program will be run with every provided input.
See this example:
```
```yaml
/*
namespace: Compile
expectation: Pass

82
tests/test-framework/README.md
View File

@ -0,0 +1,82 @@
# Leo Test Framework
This directory includes the code for the Leo Test Framework.
## How it works
You would first create a rust test file inside the folder of some part of the compiler, as the test framework tests are run by the rust test framework.
### Namespaces
Then you would create a `struct` that represents a `Namespace` where you have to implement the following:
#### Parse Type
Each `namespace` must have a function, `parse_type` that returns a `ParseType`. There are several kinds of `ParseTypes`:
- Line - Parses the File line one by one.
- ContinuousLines - Parses lines continuously as one item until an empty line is encountered.
- Whole - Parses the whole file.
#### Run Test
Each `namespace` must have a function, that runs and dictates how you want the tests for that namespace to work. To make running a test possible you are given information about the test file, like its name, content, path, etc. It allows you to return any type of output to be written to an expectation file as long as it's serializable.
### Runner
Then you would create a `struct` that represents a `Runner` where you have to implement the following:
#### Resolve Namespace
Each test file only needs one runner that represents the namespace resolution to which type of test should be run with a given string.
i.e.
```rust
struct ParseTestRunner;
impl Runner for ParseTestRunner {
fn resolve_namespace(&self, name: &str) -> Option<Box<dyn Namespace>> {
Some(match name {
"Parse" => Box::new(ParseNamespace),
"ParseExpression" => Box::new(ParseExpressionNamespace),
"ParseStatement" => Box::new(ParseStatementNamespace),
"Serialize" => Box::new(SerializeNamespace),
"Input" => Box::new(InputNamespace),
"Token" => Box::new(TokenNamespace),
_ => return None,
})
}
}
```
### Rust test Function
A rust test function that calls the framework over the runner, as well as the name of the directory, is the last thing necessary.
i.e.
```rust
#[test]
pub fn parser_tests() {
// The second argument indicates the directory where tests(.leo files)
// would be found(tests/parser).
leo_test_framework::run_tests(&ParseTestRunner, "parser");
}
```
### Clearing Expectations
To do so you can simply remove the corresponding `.out` file in the `tests/expectations` directory. Doing so will cause the output to be regenerated. There is an easier way to mass change them as well discussed in the next section.
### Test Framework Environment Variables
To make several aspects of the test framework easier to work with there are several environment variables:
- `TEST_FILTER` - runs all tests that contain the specified name.
- `CLEAR_LEO_TEST_EXPECTATIONS` - which if set clears all current expectations and regenerates them all.
To set environment variables please look at your Shell(bash/powershell/cmd/fish/etc) specific implementation for doing so
**NOTE**: Don't forget to clear the environment variable after running it with that setting, or set a temporary env variable if your shell supports it.

1
tests/test-framework/src/lib.rs
View File

@ -22,6 +22,7 @@
//! To regenerate the tests after a syntax change or failing test, delete the [`tests/expectations/`]
//! directory and run the [`parser_tests()`] test in [`parser/src/test.rs`].
#![cfg(not(doctest))] // Don't doctest the markdown.
#![doc = include_str!("../README.md")]
pub mod error;