build

#!/usr/bin/env python3

import os
import subprocess
import sys

# Bootstrapping
# =============

# Make sure the KNinja repo is available.
#
subprocess.check_call(['git', 'submodule', 'update', '--init', '--recursive'])
extdir = 'ext'
sys.path.append(os.path.join(os.path.dirname(__file__), extdir))

from kninja import *

# Build
# =====

proj = KProject(extdir = extdir)

def build(alias):
    selector = 'k | objectk | ' + alias
    return proj.definition( alias         = alias
                          , main          = 'boogie.md'
                          , other         = ['syntax.md', 'helpers.md', 'quantification.md']
                          , backend       = 'haskell'
                          , flags         = '--gen-bison-parser --syntax-module BOOGIE-PROGRAM-SYNTAX --main-module BOOGIE-QUANTIFIERS --md-selector "%s"' % selector
                          )

verification = build('verification')

# Tests
# =====
 
frontend = proj.definition( alias         = 'frontend'
                          , main          = 'frontend/frontend.md'
                          , other         = ['frontend/k-io.md', 'frontend/kore.md', 'quantification.md']
                          , backend       = 'llvm'
                          , flags         = '--main-module BOOGIE-FRONTEND --md-selector "k | metak" -ccopt -g -ccopt -O0 --gen-bison-parser --syntax-module KORE-SYNTAX'
                          )

kboogie_rule      = proj.rule( 'kboogie'
                             , description = 'kboogie: $in'
                             , command = './frontend/frontend "$in" > "$out"'
                             , ext = verification._alias
                             )
kboogie_diff_rule = proj.rule( 'diff-kboogie'
                             , description = 'diff-kboogie: $in'
                             , command = 'bin/diff-kboogie $in $expected'
                             , ext = 'diff'
                             )

def kboogie(input):
    implicit_deps = [verification.target, frontend.target , *glob('frontend/*')]
    kboogie_out = proj.source(input).then(kboogie_rule.implicit(list(implicit_deps)))
    ret = kboogie_out.then(kboogie_diff_rule.variable('expected', input + '.expect'))
    proj.alias(input + '.' + verification._alias, [ret])
    return ret

all_tests       = glob('test/verification/*/*.bpl')
failing_tests   = readlines('test/failing.verification')
passing_tests   = filter_out(all_tests, failing_tests)
proj.suite('test-verification',         passing_tests, kboogie)
proj.suite('test-verification-failing', failing_tests, kboogie, default = False)

# Main
# ====

proj.main()