-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathRakefile
172 lines (150 loc) · 5.4 KB
/
Rakefile
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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
require "open3"
require "pp"
ENV["BBBEDITOR"] ||= "xterm -e /usr/bin/nano"
semantics = [:reals, :records, :uid, :objects]
semantics.each do |s|
namespace s do
desc "Build Babelsberg/#{s.to_s.capitalize}"
task :build do
Dir.chdir "#{s}" do
exitcode = system("make babelsberg-#{s}")
fail unless exitcode
end
end
desc "Run Babelsberg/#{s.to_s.capitalize}/program.txt"
task :program => [:build] do |t, args|
Dir.chdir "#{s}" do
run_example(s, "program.txt", [])
end
end
desc "Run paper examples for Babelsberg/#{s.to_s.capitalize}"
task :test, [:example] => [:build] do |t, args|
errors = []
Dir.chdir "#{s}" do
if args[:example]
run_example(s, "examples/#{args[:example]}.txt", errors)
else
Dir["examples/*.txt"].sort_by {|a| a.split("/").last.to_i }.each do |example|
run_example(s, example, errors)
end
end
end
if errors.any?
puts "The following programs failed:\n#{errors.join}"
fail
end
end
task :citest, [:example] => :build do |t, args|
input = "#{s}/input"
File.unlink(input) if File.exist?(input)
$Errortest = lambda do |example, output|
if File.exist?(example.sub(/txt$/, "illegal"))
return "#{example}: Illegal, but didn't fail" unless output =~ /Evaluation failed!/
if File.exist?("input")
lastinput = File.read("input")
File.unlink("input")
envinput = example.sub(/txt$/, "env")
return "#{example}: No environment given" unless File.exist?(envinput)
environments = File.read(envinput).split(";\n")
return "#{example}: No CIIndex" unless lastinput =~ /^[Cc]IIndex\s*(?::=)?\s*(\d+)/m
idx = $1.to_i
return "#{example}: Not all environments used" unless environments.size == idx
end
return nil
else
return "#{example}: No input created" unless File.exist?("input")
lastinput = File.read("input")
File.unlink("input")
envinput = example.sub(/txt$/, "env")
return "#{example}: No environment given" unless File.exist?(envinput)
environments = File.read(envinput).split(";\n")
return "#{example}: No CIIndex" unless lastinput =~ /^[cC]IIndex\s*(?::=)?\s*(\d+)/m
idx = $1.to_i
return "#{example}: Not all environments used" unless environments.size == idx
if output =~ /Evaluation failed!/
return "#{example}: Unexpected failure" unless environments.last =~ /unsat/
end
end
end
ENV["BBBEDITOR"] = File.expand_path("../#{s}/cisolver.rb", __FILE__)
retval = Rake::Task["#{s}:test"].invoke(args[:example])
puts "\nAll OK!\n" if retval
retval
end
desc "Review the example and 'play solver'"
task :review, [:example] => :build do |t, args|
ENV["BBBReview"] = "true"
Rake::Task["#{s}:citest"].invoke(args[:example])
end
if s == :objects
desc "Review the example and Z3's solution"
task :z3, [:example] => :build do |t, args|
ENV["BBBZ3"] = "true"
Rake::Task["#{s}:citest"].invoke(args[:example])
end
desc "Review the example and Z3's solution, but use the fallback env"
task :z3fb, [:example] => :build do |t, args|
ENV["BBBZ3FB"] = "true"
Rake::Task["#{s}:z3"].invoke(args[:example])
end
desc "Run an example completely with Z3"
task :z3run, [:example] => :build do |t, args|
ENV["BBBZ3Auto"] = "true"
Rake::Task["#{s}:z3"].invoke(args[:example])
end
desc "Run and compare an example completely automatically with Z3"
task :z3ci, [:example] => :build do |t, args|
ENV["BBBZ3AutoCompare"] = "true"
Rake::Task["#{s}:z3run"].invoke(args[:example])
end
end
end
end
$Errortest = lambda do |example, output|
return example if output.end_with?("Evaluation failed!\n")
end
def run_example(s, example, errors)
puts "Program #{example}:"
puts File.read example
output = run_example_quiet(s, example)
print output
error = $Errortest[example, output]
errors << "\t#{error}\n" if error
end
def run_example_quiet(s, example)
output = ""
Open3.popen3("cat #{example} | ./babelsberg-#{s}") do |stdin, stdout, stderr|
ios = [stdout, stderr]
until stdout.eof? and stderr.eof?
ready = IO.select(ios)
ready[0].each do |io|
(ios.delete(io); next) if io.eof?
result = io.read_nonblock(1024)
print result if caller.detect { |c| c =~ /`run_example'/ }
output << result
end
end
end
output
end
languages = [:javascript, :ruby, :squeak]
languages.each do |l|
desc "Generate tests for Babelsberg/#{l.to_s.capitalize}"
task l, [:example] do |t, args|
lpath = File.expand_path("../#{l}", __FILE__)
ENV["BBBPATH"] = lpath
Dir.chdir lpath do
exitcode = system("make babelsberg-#{l} > /dev/null")
fail unless exitcode
if args[:example]
output = run_example_quiet(l, "../spec/examples/#{args[:example]}.txt")
else
output = Dir["../spec/examples/*.txt"].sort_by {|a| a.split("/").last.to_i }.map do |example|
run_example_quiet(l, example)
end.join("\n")
end
scaffold = File.read(Dir["#{lpath}/scaffold.*"][0])
puts scaffold.sub("INSERTHERE", output)
end
end
end