Merge pull request #1260 from AleoHQ/feature-tgc-ci

[CI] ACL2 tgc CI
This commit is contained in:
Alessandro Coglio 2021-08-21 11:23:53 -07:00 committed by GitHub
commit d609bb28d1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 290 additions and 2 deletions

95
.github/workflows/acl2.yml vendored Normal file
View File

@ -0,0 +1,95 @@
name: Leo-ACL2
on:
pull_request:
push:
branches:
- master
- staging
- trying
paths-ignore:
- 'docs/**'
- 'documentation/**'
env:
RUST_BACKTRACE: 1
# This job can only be run on linux (Ubuntu)
jobs:
acl2:
name: leo-acl2
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Install Rust
uses: actions-rs/toolchain@v1
with:
profile: minimal
toolchain: stable
override: true
- name: Generate asts
run: |
cargo -q run -p leo-test-framework --bin tgc
# 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.
- name: Pull tgc executable
run: |
mkdir acl2 && cd acl2;
wget $(curl -s https://api.github.com/repos/AleoHQ/leo-acl2-bin/releases/latest \
| grep "browser_download_url.*.tgz" \
| cut -d : -f 2,3 \
| tr -d \" \
| xargs)
tar -xvzf $(ls)
# Using the prepared ASTs and the pulled and unzipped tgc run theorem generation.
- name: Run tgc over ASTs
run: |
canonicalization_errors=();
type_inference_errors=();
for dir in `ls tmp/tgc`;
do
cd tmp/tgc/$dir; # enter the directory
./../../../acl2/tgc canonicalization initial_ast.json canonicalization_ast.json canonicalization-theorem.lisp > canonicalization_result.out || canonicalization_errors+=("$dir");
# Disabling Type inference for now
# ./../../../acl2/tgc type-inference canonicalization_ast.json type_inferenced_ast.json type-inference-theorem.lisp > type_inference_result.out || type_inference_errors+=("$dir");
cd ../../..
done;
if [ ${#canonicalization_errors[@]} -eq 0 ]; then
echo "Canonicalization - Success!"
else
echo "Canonicalization Failures:";
for dir in ${canonicalization_errors[@]};
do
echo $dir;
done;
echo "Attaching logs:"
for dir in ${canonicalization_errors[@]};
do
cat tmp/tgc/$dir/canonicalization_result.out
done;
exit 1
fi
if [ ${#type_inference_errors[@]} -eq 0 ]; then
echo "Type Inference - Success!"
else
echo "Type Inference Failures:";
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;
exit 1
fi

6
Cargo.lock generated
View File

@ -1425,9 +1425,15 @@ dependencies = [
name = "leo-test-framework"
version = "1.5.3"
dependencies = [
"leo-asg",
"leo-ast",
"leo-compiler",
"leo-imports",
"leo-parser",
"serde",
"serde_json",
"serde_yaml",
"structopt",
]
[[package]]

View File

View File

@ -291,7 +291,7 @@ impl Canonicalizer {
return Expression::Identifier(self.circuit_name.as_ref().unwrap().clone());
}
}
_ => {}
_ => (),
}
expression.clone()

1
test-framework/.gitignore vendored Normal file
View File

@ -0,0 +1 @@
!src/bin

View File

@ -26,3 +26,28 @@ version = "1.0"
[dependencies.serde_yaml]
version = "0.8"
# List of dependencies for tgc binary;
[dependencies.leo-ast]
path = "../ast"
version = "1.5.2"
[dependencies.leo-parser]
path = "../parser"
version = "1.5.2"
[dependencies.leo-imports]
path = "../imports"
version = "1.5.2"
[dependencies.leo-asg]
path = "../asg"
version = "1.5.2"
[dependencies.leo-compiler]
path = "../compiler"
version = "1.5.2"
[dependencies.structopt]
version = "0.3"

View File

@ -0,0 +1,161 @@
// Copyright (C) 2019-2021 Aleo Systems Inc.
// This file is part of the Leo library.
// The Leo library is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
// The Leo library is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU General Public License for more details.
// You should have received a copy of the GNU General Public License
// along with the Leo library. If not, see <https://www.gnu.org/licenses/>.
use leo_asg::Asg;
use leo_compiler::{compiler::thread_leaked_context, TypeInferencePhase};
use leo_imports::ImportParser;
use leo_test_framework::{
fetch::find_tests,
test::{extract_test_config, TestExpectationMode as Expectation},
};
use std::{error::Error, fs, path::PathBuf};
use structopt::{clap::AppSettings, StructOpt};
#[derive(StructOpt)]
#[structopt(name = "ast-stages-generator", author = "The Aleo Team <hello@aleo.org>", setting = AppSettings::ColoredHelp)]
struct Opt {
#[structopt(
short,
long,
help = "Path to the output folder (auto generated)",
default_value = "tmp/tgc"
)]
path: PathBuf,
#[structopt(short, long, help = "Run only for test that match pattern")]
filter: Option<String>,
#[structopt(short, long, help = "Skip tests matching pattern")]
skip: Option<Vec<String>>,
}
fn main() {
handle_error(run_with_args(Opt::from_args()));
}
fn run_with_args(opt: Opt) -> Result<(), Box<dyn Error>> {
// Variable that stores all the tests.
let mut tests = Vec::new();
let mut test_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
test_dir.push("../tests/");
find_tests(&test_dir, &mut tests);
if !opt.path.exists() {
fs::create_dir_all(&opt.path)?;
}
// Prepare directory for placing results.
'main_loop: for (index, (path, text)) in tests.iter().enumerate() {
if let Some(config) = extract_test_config(text) {
// Skip namespaces that we don't need; also skip failure tests.
if config.namespace != "Compile" || config.expectation == Expectation::Fail {
continue;
}
let mut test_name = path
.split("tests/")
.last()
.unwrap()
.replace(std::path::MAIN_SEPARATOR, "_");
// Filter out the tests that do not match pattern, if pattern is set.
if let Some(filter) = &opt.filter {
if !test_name.contains(filter) {
continue;
}
}
// If skip flag is used, don't run tests matching the pattern.
if let Some(skips) = &opt.skip {
for skip_pattern in skips {
if test_name.contains(skip_pattern) {
println!("Skipping: {} because of {}", test_name, skip_pattern);
continue 'main_loop;
}
}
}
test_name.push_str(&format!("_{}", index));
// Create directory for this file.
let mut target = PathBuf::from("tmp/tgc");
target.push(test_name);
if !target.exists() {
fs::create_dir_all(target.clone())?;
}
let cwd = config
.extra
.get("cwd")
.map(|val| {
let mut cwd = PathBuf::from(path);
cwd.pop();
cwd.join(&val.as_str().unwrap())
})
.unwrap_or(PathBuf::from(path));
// Write all files into the directory.
let (initial, canonicalized, type_inferenced) = generate_asts(cwd, text)?;
target.push("initial_ast.json");
fs::write(target.clone(), initial)?;
target.pop();
target.push("canonicalization_ast.json");
fs::write(target.clone(), canonicalized)?;
target.pop();
target.push("type_inferenced_ast.json");
fs::write(target.clone(), type_inferenced)?;
}
}
Ok(())
}
/// Do what Compiler does - prepare 3 stages of AST: initial, canonicalized and type_inferenced
fn generate_asts(path: PathBuf, text: &String) -> Result<(String, String, String), Box<dyn Error>> {
let mut ast = leo_parser::parse_ast(path.clone().into_os_string().into_string().unwrap(), text)?;
let initial = ast.to_json_string()?;
ast.canonicalize()?;
let canonicalized = ast.to_json_string()?;
let asg = Asg::new(
thread_leaked_context(),
&ast,
&mut ImportParser::new(path, Default::default()),
)?;
let type_inferenced = TypeInferencePhase::default()
.phase_ast(&ast.into_repr(), &asg.clone().into_repr())
.expect("Failed to produce type inference ast.")
.to_json_string()?;
Ok((initial, canonicalized, type_inferenced))
}
fn handle_error(res: Result<(), Box<dyn Error>>) {
match res {
Ok(_) => (),
Err(err) => {
eprintln!("Error: {}", err);
std::process::exit(1);
}
}
}

View File

@ -22,7 +22,7 @@ pub enum TestExpectationMode {
Fail,
}
#[derive(serde::Serialize, serde::Deserialize)]
#[derive(Debug, serde::Serialize, serde::Deserialize)]
pub struct TestConfig {
pub namespace: String,
pub expectation: TestExpectationMode,