Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Rebase onto recent version of upstream #9

Open
wants to merge 56 commits into
base: master
Choose a base branch
from
Open

Rebase onto recent version of upstream #9

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
56 commits
Select commit Hold shift + click to select a range
46b8679
add attributes for the haskell backend (#742)
yzhang90 Feb 26, 2020
dfb08b9
prove hkg-totalSupply using haskell backend (#743)
yzhang90 Feb 28, 2020
a3fc1b0
Web3: Append reason to error message (#744)
anvacaru Mar 6, 2020
3113bfa
json: implement reverseJSONs (#734)
ehildenb Mar 6, 2020
e147901
Update dependency: deps/k (#715)
rv-jenkins Mar 9, 2020
b0e941f
Json refactors and cleanups (#749)
ehildenb Mar 11, 2020
06f1d2f
SOLAR support - module EVM-IMP-SPECS (#657)
denis-bogdanas Mar 11, 2020
4f5143b
Update dependency: deps/plugin (#751)
rv-jenkins Mar 12, 2020
98c577a
kevm: set kevm-client in PATH (#748)
anvacaru Mar 12, 2020
17841f9
Update dependency: deps/k (#746)
rv-jenkins Mar 13, 2020
e5fef8e
Makefile: do not prefix commands with K_BIN (#756)
ehildenb Mar 19, 2020
13d03fd
Use pipes instead of a socket for communication with plugin (#755)
Mar 19, 2020
b5e15a2
Simplification rules for bool2Word (#758)
ttuegel Mar 20, 2020
53c9279
Update dependency: deps/k (#752)
rv-jenkins Mar 21, 2020
6ad0293
Update dependency: deps/k (#759)
rv-jenkins Mar 24, 2020
17021fc
Update dependency: deps/k (#760)
rv-jenkins Mar 26, 2020
e62199c
Fix a couple of bugs (#762)
gtrepta Mar 26, 2020
cc24c99
Haskell concrete lemmas (#763)
ana-pantilie Mar 30, 2020
ae17eb4
Add lemmas needed by the Haskell backend (#733)
virgil-serbanuta Mar 30, 2020
e3c2c54
Add back Jello Paper deploy (#764)
ehildenb Mar 31, 2020
822525c
Update dependency: deps/k (#761)
rv-jenkins Mar 31, 2020
4d59bcf
Refactor `finishTX` in Web3 (#766)
anvacaru Apr 2, 2020
03d7365
New slow lists (#765)
ehildenb Apr 2, 2020
84c4955
Implement firefly_setGasPrice (#767)
anvacaru Apr 3, 2020
224e3e3
Update repository layout in README.md (#770)
gtrepta Apr 8, 2020
1ba5032
Update dependency: deps/k (#768)
rv-jenkins Apr 10, 2020
c72eba3
Implement firefly_setNetworkId web3 method (#773)
anvacaru Apr 14, 2020
ff617e8
Update <blockhashes> in web3 (#771)
gtrepta Apr 14, 2020
2ffdb9d
Fix side effects from failed sendRawTransaction (#775)
gtrepta Apr 24, 2020
e23f8a2
Make `#range` and `_[_.._]` total on Bytes builds (#777)
ehildenb Apr 26, 2020
0f97eb9
Update dependency: deps/k (#772)
rv-jenkins Apr 26, 2020
660c0a5
Handle alternate transaction signatures (#776)
gtrepta Apr 26, 2020
9404d9b
kevm: add -p and -h options (#780)
anvacaru Apr 28, 2020
058c3dd
deps/k: cdc484531 - Better debugging support (#1229) (#779)
rv-jenkins Apr 28, 2020
78fa283
Update dependency: deps/plugin (#781)
rv-jenkins Apr 28, 2020
8e925ee
loadTransaction: Ignore fields that aren't part of the web3 spec (#778)
gtrepta Apr 28, 2020
b682b27
Update dependency: deps/k (#782)
rv-jenkins May 1, 2020
f8db3bc
Update dependency: deps/k (#784)
rv-jenkins May 2, 2020
7065e7c
Remove node build from semantics (#786)
ehildenb May 4, 2020
96415f8
Update dependency: deps/k (#787)
rv-jenkins May 5, 2020
a6a1823
Update dependency: deps/plugin (#789)
rv-jenkins May 5, 2020
8bc89ee
Improve timestamp updates (#783)
gtrepta May 7, 2020
5b4d864
Update requirements info in README. (#791)
radumereuta May 8, 2020
309d449
Helper changes for symbolic testing (#769)
denis-bogdanas May 12, 2020
effb00e
Update dependency: deps/k (#790)
rv-jenkins May 13, 2020
0732f35
Unit test for failing Arbitrum `eth_call` (#754)
anvacaru May 13, 2020
c7503f1
deps/plugin: 1081ab8 - Kframework dockerfile (#97) (#795)
rv-jenkins May 14, 2020
9b9b4e6
edsl: #Ceil(#buf) rule simplified to use #rangeBytes (#794)
denis-bogdanas May 18, 2020
fac5ebb
Makefile refactors for global install and new sysroot (#801)
ehildenb May 27, 2020
7ef36b5
Update dependency: deps/k (#799)
rv-jenkins May 27, 2020
8f3ecb5
data.md: add smtlib translation for signed/unsigned
MrChico Jul 12, 2019
8fc888a
keep on skipping haskell and llvm backends
MrChico Sep 30, 2019
5910e02
evm-types.md: simplify sizeWordStack
MrChico Feb 17, 2020
9ebac26
evm-types.md: add constraint on sizeWordStack
asymmetric Feb 18, 2020
4322d4e
Revert "evm-types.md: add constraint on sizeWordStack"
MrChico Feb 18, 2020
1958128
Merge branch 'master' into rebase-May2020
kmbarry1 May 29, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 0 additions & 3 deletions Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,15 +11,13 @@ RUN apt-get update \
flex \
gcc \
jq \
libboost-all-dev \
libboost-test-dev \
libcrypto++-dev \
libffi-dev \
libgflags-dev \
libjemalloc-dev \
libmpfr-dev \
libprocps-dev \
libprotobuf-dev \
libsecp256k1-dev \
libssl-dev \
libtool \
Expand All @@ -32,7 +30,6 @@ RUN apt-get update \
openjdk-11-jdk \
pandoc \
pkg-config \
protobuf-compiler \
python3 \
python-pygments \
python-recommonmark \
Expand Down
211 changes: 66 additions & 145 deletions Jenkinsfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,26 +8,14 @@ pipeline {
PACKAGE = 'kevm'
ROOT_URL = 'https://github.com/kframework/evm-semantics/releases/download'
}
options {
ansiColor('xterm')
}
options { ansiColor('xterm') }
stages {
stage("Init title") {
when {
changeRequest()
beforeAgent true
}
steps {
script {
currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}"
}
}
when { changeRequest() }
steps { script { currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}" } }
}
stage('Build and Test') {
when {
changeRequest()
beforeAgent true
}
when { changeRequest() }
agent {
dockerfile {
additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
Expand All @@ -36,56 +24,15 @@ pipeline {
}
}
stages {
stage('Dependencies') {
parallel {
stage('K') {
steps {
sh '''
make deps RELEASE=true
'''
}
}
stage('Tests') {
steps {
sh '''
make split-tests -j3
'''
}
}
}
}
stage('Build') {
steps {
sh '''
make build -j4
'''
}
}
stage('K Dependencies') { steps { sh 'make deps RELEASE=true' } }
stage('Build') { steps { sh 'make build RELEASE=true -j6' } }
stage('Test Execution') {
failFast true
options { timeout(time: 20, unit: 'MINUTES') }
parallel {
stage('Conformance (LLVM)') {
steps {
sh '''
make test-conformance -j8 TEST_CONCRETE_BACKEND=llvm
'''
}
}
stage('VM (Haskell)') {
steps {
sh '''
make test-vm -j8 TEST_CONCRETE_BACKEND=haskell
'''
}
}
stage('Conformance (Web3)') {
steps {
sh '''
make test-web3 -j8
'''
}
}
stage('Conformance (LLVM)') { steps { sh 'make test-conformance -j8 TEST_CONCRETE_BACKEND=llvm' } }
stage('VM (Haskell)') { steps { sh 'make test-vm -j8 TEST_CONCRETE_BACKEND=haskell' } }
stage('Conformance (Web3)') { steps { sh 'make test-web3 -j8' } }
}
}
stage('Proofs') {
Expand All @@ -94,102 +41,76 @@ pipeline {
timeout(time: 55, unit: 'MINUTES')
}
parallel {
stage('Java + Haskell') {
steps {
sh '''
make test-prove -j6
'''
}
}
stage('Haskell (dry-run)') {
steps {
sh '''
make test-prove -j2 KPROVE_OPTIONS='--dry-run' TEST_SYMBOLIC_BACKEND='haskell'
'''
}
}
stage('Java + Haskell') { steps { sh 'make test-prove -j6' } }
stage('Haskell (dry-run)') { steps { sh 'make test-prove -j2 KPROVE_OPTIONS=--dry-run TEST_SYMBOLIC_BACKEND=haskell' } }
}
}
stage('Test Interactive') {
failFast true
options { timeout(time: 35, unit: 'MINUTES') }
parallel {
stage('LLVM krun') {
steps {
sh '''
make test-interactive-run TEST_CONCRETE_BACKEND=llvm
'''
}
}
stage('Java krun') {
steps {
sh '''
make test-interactive-run TEST_CONCRETE_BACKEND=java
'''
}
}
stage('Haskell krun') {
steps {
sh '''
make test-interactive-run TEST_CONCRETE_BACKEND=haskell
'''
}
}
stage('LLVM Kast') {
steps {
sh '''
make test-parse TEST_CONCRETE_BACKEND=llvm
'''
}
}
stage('Failing tests') {
steps {
sh '''
make test-failure TEST_CONCRETE_BACKEND=llvm
'''
}
}
stage('Java KLab') {
steps {
sh '''
make test-klab-prove TEST_SYMBOLIC_BACKEND=java
'''
}
}
stage('Haskell Search') {
steps {
sh '''
make test-interactive-search TEST_SYMBOLIC_BACKEND=haskell -j4
'''
}
}
stage('KEVM help') {
steps {
stage('LLVM krun') { steps { sh 'make test-interactive-run TEST_CONCRETE_BACKEND=llvm' } }
stage('Java krun') { steps { sh 'make test-interactive-run TEST_CONCRETE_BACKEND=java' } }
stage('Haskell krun') { steps { sh 'make test-interactive-run TEST_CONCRETE_BACKEND=haskell' } }
stage('LLVM Kast') { steps { sh 'make test-parse TEST_CONCRETE_BACKEND=llvm' } }
stage('Failing tests') { steps { sh 'make test-failure TEST_CONCRETE_BACKEND=llvm' } }
stage('Java KLab') { steps { sh 'make test-klab-prove TEST_SYMBOLIC_BACKEND=java' } }
stage('Haskell Search') { steps { sh 'make test-interactive-search TEST_SYMBOLIC_BACKEND=haskell -j4' } }
stage('KEVM help') { steps { sh './kevm help' } }
}
}
}
}
stage('Deploy') {
when { branch 'master' }
agent { dockerfile { reuseNode true } }
stages {
stage('Update Dependents') {
steps {
build job: 'rv-devops/master', propagate: false, wait: false \
, parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
, string(name: 'PR_REVIEWER', value: 'ehildenb') \
, string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/firefly') \
, string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
]
build job: 'rv-devops/master', propagate: false, wait: false \
, parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
, string(name: 'PR_REVIEWER', value: 'ehildenb') \
, string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/erc20-verification') \
, string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
]
}
}
stage('Jello Paper') {
steps {
sshagent(['2b3d8d6b-0855-4b59-864a-6b3ddf9c9d1a']) {
dir("kevm-${env.VERSION}-jello-paper") {
sh '''
./kevm help
git config --global user.email "[email protected]"
git config --global user.name "RV Jenkins"
mkdir -p ~/.ssh
echo 'host github.com' > ~/.ssh/config
echo ' hostname github.com' >> ~/.ssh/config
echo ' user git' >> ~/.ssh/config
echo ' identityagent SSH_AUTH_SOCK' >> ~/.ssh/config
echo ' stricthostkeychecking accept-new' >> ~/.ssh/config
chmod go-rwx -R ~/.ssh
ssh github.com || true
git clone 'ssh://github.com/kframework/evm-semantics.git'
cd evm-semantics
git checkout -B gh-pages origin/master
rm -rf .build .gitignore .gitmodules cmake deps Dockerfile Jenkinsfile kast-json.py kevm kore-json.py LICENSE Makefile media package
git add ./
git commit -m 'gh-pages: remove unrelated content'
git fetch origin gh-pages
git merge --strategy ours FETCH_HEAD
git push origin gh-pages
'''
}
}
}
}
}
}
stage('Update Dependents') {
when { branch 'master' }
steps {
build job: 'rv-devops/master', propagate: false, wait: false \
, parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
, string(name: 'PR_REVIEWER', value: 'ehildenb') \
, string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/firefly') \
, string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
]
build job: 'rv-devops/master', propagate: false, wait: false \
, parameters: [ booleanParam(name: 'UPDATE_DEPS_SUBMODULE', value: true) \
, string(name: 'PR_REVIEWER', value: 'ehildenb') \
, string(name: 'UPDATE_DEPS_REPOSITORY', value: 'runtimeverification/erc20-verification') \
, string(name: 'UPDATE_DEPS_SUBMODULE_DIR', value: 'deps/evm-semantics') \
]
}
}
}
}
Loading