Skip to content
Permalink
Browse files

fix

  • Loading branch information
gokhankici committed Jun 18, 2019
1 parent 2acce2b commit c769cd8ee9b297dc1111aa2e5b034ffe12ae69a2
@@ -12,14 +12,15 @@
{
"type": "sink",
"variables": [
"out",
"inf",
"snan",
"qnan",
"div_by_zero",
"out",
"ine",
"overflow",
"underflow",
"zero"
"zero",
"div_by_zero"
]
}
],
15 iodine
@@ -1,3 +1,14 @@
#!/bin/sh
#!/usr/bin/env python3

stack exec iodine -- $@
import os.path as p
import subprocess
import sys

THIS_DIR = p.realpath(p.dirname(__file__))
IVERILOG_DIR = p.join(THIS_DIR, "iverilog-parser")

r = subprocess.run(["stack", "exec", "iodine", "--",
"--iverilog-dir", IVERILOG_DIR] +
sys.argv[1:],
cwd=THIS_DIR)
sys.exit(r.returncode)
@@ -2,7 +2,8 @@
import os.path as p
import subprocess
import sys
from config import IVERILOG_DIR, DEBUG
from config import IODINE_SCRIPT, ABDUCTION_OUTPUT, DEBUG
import shutil


class Benchmark(collections.namedtuple("Benchmark",
@@ -11,10 +12,7 @@ class Benchmark(collections.namedtuple("Benchmark",
Contains the information required to run a benchmark.
"""
def run_iodine(self, extra_args=[], **kwargs):
args = ["stack", "exec", "iodine", "--",
"--iverilog-dir", IVERILOG_DIR]

args.extend(extra_args)
args = [IODINE_SCRIPT] + extra_args
args.extend([p.realpath(self.filename),
self.module,
p.realpath(self.annotfile)])
@@ -27,7 +25,10 @@ def run_iodine(self, extra_args=[], **kwargs):

def run_abduction(self):
""" Run Iodine but with the abduction feature """
return self.run_iodine(["--abduction"])
rc = self.run_iodine(["--abduction"])
if rc == 0:
shutil.move(ABDUCTION_OUTPUT, p.basename(ABDUCTION_OUTPUT))
return rc

def with_annot(self, annotfile):
""" Returns a new benchmark with the given annotation file """
@@ -4,6 +4,7 @@

LINPROG_DIR = p.realpath(p.dirname(__file__))
PROJECT_ROOT = p.realpath(p.join(LINPROG_DIR, "../../"))
IVERILOG_DIR = p.join(PROJECT_ROOT, "iverilog-parser")
BENCHMARK_DIR = p.join(PROJECT_ROOT, "benchmarks")
SCHEMA_FILE = p.join(PROJECT_ROOT, "annotation-schema.json")
IODINE_SCRIPT = p.join(PROJECT_ROOT, "iodine")
ABDUCTION_OUTPUT = p.join(PROJECT_ROOT, "cplex.json")
@@ -13,21 +13,5 @@
"out"
]
}
],
"qualifiers": [
{
"type": "pairs",
"variables": [
"r1",
"r2"
]
},
{
"type": "pairs",
"variables": [
"opb_r",
"opa_r"
]
}
]
}
@@ -13,21 +13,5 @@
"o"
]
}
],
"qualifiers": [
{
"type": "implies",
"lhs": "i1",
"rhs": [
"i2"
]
},
{
"type": "implies",
"lhs": "i2",
"rhs": [
"i1"
]
}
]
}
@@ -1,19 +1,11 @@
module test(clk, in1, in2, in3, out);
// @annot{taint_source(in1)}
// @annot{taint_source(in2)}
// @annot{taint_source(in3)}
input wire clk, in1, in2, in3;

// @annot{taint_sink(out)}
output reg out;

reg in1_r, in2_r, in3_r;
reg in1_r2, in2_r2, in3_r2;
reg out_tmp;

// @annot{qualifierPairs([in1_r2, in2_r2])}
// @annot{qualifierPairs([in1_r, in2_r])}

always @(posedge clk)
in1_r <= in1;

@@ -1,15 +1,8 @@
module test(clk, i1, i2, o);
// @annot{taint_source(i1)}
// @annot{taint_source(i2)}
// @annot{taint_sink(o)}

input wire clk, i1, i2;
output reg o;
reg cond;

// @annot{qualifierImp(i1,[i2])}
// @annot{qualifierImp(i2,[i1])}

always @(posedge clk)
if (cond)
o <= i1;

0 comments on commit c769cd8

Please sign in to comment.
You can’t perform that action at this time.