isla 0.2.0

Isla is a symbolic execution engine for Sail instruction set architecture specifications.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

#!/usr/bin/env ruby

require 'open3'
require 'optparse'
include Process

$TEST_DIR = File.expand_path(File.dirname(__FILE__))

$options = {}
OptionParser.new do |opts|
  opts.banner = "Usage: run_tests.rb [options]"

  opts.on("-c", "--config [PATH]", String, "Set config for RISC-V concurrency tests") do |c|
    $options[:config] = File.expand_path c
  end
end.parse!

class String
  def colorize(color_code)
    "\e[#{color_code}m#{self}\e[0m"
  end

  def red
    colorize(91)
  end

  def green
    colorize(92)
  end

  def yellow
    colorize(93)
  end

  def blue
    colorize(94)
  end

  def cyan
    colorize(96)
  end
end

class Dir
  def self.chunks(dir, n, &block)
    Dir.entries(dir).each_slice(n).each do |chunk|
      chunk.each { |file| fork { yield file } }
      statuses = Process.waitall
      statuses.each do |status|
        exit 1 if status[1].exitstatus != 0
      end
    end
  end
end

def step(str, *extra)
  expected = extra.fetch(0, 0)
  stdout, stderr, status = Open3.capture3("#{str}")
  if status.exitstatus != expected then
    puts <<OUTPUT
#{"Failed".red} (expected #{expected}, got: #{status}): #{str}
#{"stdout".cyan}: #{stdout}
#{"stderr".blue}: #{stderr}
OUTPUT
    exit 1
  end
end

def step_print(str)
  if !system str then
    puts <<OUTPUT
#{"Failed".red}: #{str}
OUTPUT
    exit 1
  end
end

def chdir_relative(path)
  Dir.chdir(File.expand_path(File.join($TEST_DIR, path)))
end

def wget(url, file)
  return if File.file?(file)

  system "wget -O #{file} #{url}"
end

def run_tests()
  chdir_relative "../isla-sail"
  exit 1 if !system "make"
  isla_sail = File.expand_path(File.join($TEST_DIR, "../isla-sail/isla-sail"))
  exit 1 if !File.file?(isla_sail)

  chdir_relative "../isla-litmus"
  exit 1 if !system "make"
  isla_litmus = File.expand_path(File.join($TEST_DIR, "../isla-litmus/isla-litmus"))
  exit 1 if !File.file?(isla_litmus)
  
  chdir_relative ".."
  exit 1 if !system "cargo build --release"

  chdir_relative "property"
  ["", "129"].each do |suffix|
    isla_property = File.expand_path(File.join($TEST_DIR, "../target/release/isla-property#{suffix}"))
    exit 1 if !File.file?(isla_property)
    
    puts "Running tests [#{suffix}]:".blue
    
    Dir.chunks ".", 12 do |file|
      next if file !~ /.+\.sail$/

      basename = File.basename(file, ".*")

      building = Process.clock_gettime(Process::CLOCK_MONOTONIC)
      step("#{isla_sail} #{file} include/config.sail -o #{basename}")
      starting = Process.clock_gettime(Process::CLOCK_MONOTONIC)
      if File.extname(basename) == ".unsat" then
        step("LD_LIBRARY_PATH=..:$LD_LIBRARY_PATH #{isla_property} -A #{basename}.ir -p prop -L lin -T 2 -C ../../configs/plain.toml")
      else
        step("LD_LIBRARY_PATH=..:$LD_LIBRARY_PATH #{isla_property} -A #{basename}.ir -p prop -T 2 -C ../../configs/plain.toml", 1)
      end
      ending = Process.clock_gettime(Process::CLOCK_MONOTONIC)
      build_time = (starting - building) * 1000
      time = (ending - starting) * 1000
      puts "#{file}".ljust(40).concat("#{"ok".green} (#{build_time.to_i}ms/#{time.to_i}ms)\n")
    end
  end

  isla_axiomatic = File.expand_path(File.join($TEST_DIR, "../target/release/isla-axiomatic"))
  exit 1 if !File.file?(isla_axiomatic)

  chdir_relative "."
  
  arch = "axiomatic/riscv64.ir"
  wget("https://raw.githubusercontent.com/rems-project/isla-snapshots/master/riscv64.ir", arch)
  
  step_print("LD_LIBRARY_PATH=..:$LD_LIBRARY_PATH #{isla_axiomatic} -A #{arch} -C #{$options[:config]} -m ../web/client/dist/riscv.cat -t axiomatic/tests --refs axiomatic/refs")
end

run_tests