Module: ADSL::Spass::Bin

Includes:
Util
Included in:
Test::Unit::TestCase
Defined in:
lib/adsl/spass/bin.rb

Instance Method Summary collapse

Methods included from Util

#replace_conjecture

Instance Method Details

#default_options ⇒ Object 



15
16
17
18
19
20
21
22
23
24
 
# File 'lib/adsl/spass/bin.rb', line 15

def default_options
  {
    :halt_on_error => false,
    :check_satisfiability => true,
    :timeout => 180,
    :output => :terminal,
    :actions => nil,
    :invariants => nil
  }
end

#exec_spass(spass_code, timeout = -1,, include_stats = false) ⇒ Object 



174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
 
# File 'lib/adsl/spass/bin.rb', line 174

def exec_spass(spass_code, timeout=-1, include_stats = false)
  tmp_file = Tempfile.new "spass_temp"
  tmp_file.write spass_code
  tmp_file.close
  arg_combos = ["", "-Sorts=0"]
  commands = arg_combos.map{ |a| "SPASS #{a} -TimeLimit=#{timeout} #{tmp_file.path}" }
  output = process_race(*commands)
  result = /^SPASS beiseite: (.+)\.$/.match(output)[1]

  stats = include_stats ? pack_stats(spass_code, output) : nil
  verdict = nil

  case result
  when 'Proof found'
    verdict = :correct
  when 'Completion found'
    verdict = :incorrect
  else
    verdict = :inconclusive
  end
  return stats.nil? ? verdict : [verdict, stats]
ensure
  tmp_file.delete unless tmp_file.nil?
end

#filter_by_name(elems, names) ⇒ Object 



40
41
42
43
 
# File 'lib/adsl/spass/bin.rb', line 40

def filter_by_name(elems, names)
  return elems if names.nil?
  elems.select{ |elem| names.map{ |name| elem.name.include? name}.include? true }
end

#output(term_msg, csv) ⇒ Object 



26
27
28
29
30
31
32
33
34
35
36
37
38
 
# File 'lib/adsl/spass/bin.rb', line 26

def output(term_msg, csv)
  if @verification_output == :terminal
    if term_msg
      print term_msg
      STDOUT.flush
    end
  elsif @verification_output == :csv
    @csv_output << csv if csv
  elsif @verification_output == :silent
  else
    raise "Unknown verification output #{@verification_output}"
  end
end

#pack_stats(spass_code, spass_output) ⇒ Object 



199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
 
# File 'lib/adsl/spass/bin.rb', line 199

def pack_stats(spass_code, spass_output)
  spass_output = spass_output.split("\n").last(10).join("\n")
  stats = {}

  # should be set externally
  stats[:translation_time] = nil
  stats[:action] = nil
  stats[:invariant] = nil
  stats[:result] = nil

  identifiers = /predicates\s*\[([^\]]*)\]/.match(spass_code)[1].scan(/\w+/)
  stats[:spass_predicate_count] = identifiers.length

  formulae = spass_code.scan(/formula\s*\([^\.]+\)\./)
  stats[:spass_formula_count] = formulae.length
  stats[:average_formula_length] = formulae.inject(0){ |total, formula| total += formula.length} / formulae.length

  times = spass_output.scan(/(\d):(\d\d):(\d\d)\.(\d\d)/)
  raise "Incorrect time format extracted from spass output. Tail of spass output: #{spass_output}" if times.length != 6
  times = times.map{ |time| time[3].to_i*10 + time[2].to_i*1000 + time[1].to_i*60*1000 + time[0].to_i*60*60*1000 }
  stats[:spass_preparation_time] = times[1..2].sum 
  stats[:spass_proof_lookup_time] = times[3..5].sum

  stats[:proof_clause_count] = /^SPASS derived (\d+) clauses.*$/.match(spass_output)[1].to_i
  
  stats[:memory] = /^\s*SPASS allocated (\d+) KBytes.*$/.match(spass_output)[1].to_i

  stats
end

#remove_empty_actions(actions) ⇒ Object 



45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
 
# File 'lib/adsl/spass/bin.rb', line 45

def remove_empty_actions(actions)
  empty, valid = actions.select_reject{ |a| a.block.statements.empty? }
  unless empty.empty?
    if @verification_output == :terminal
      puts 'Actions with empty bodies trivially preserve invariants.'
      puts "The following actions are empty: #{ empty.map(&:name).join ', ' }"
    elsif @verification_output == :csv
      empty.each do |empty_action|
        @csv_output << {
          :action => empty_action.name,
          :result => 'trivially correct'
        }
      end
    end
  end
  actions.set_to valid
end

#verify(input, options = {}) ⇒ Object 



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
 
# File 'lib/adsl/spass/bin.rb', line 63

def verify(input, options={})
  ds_spec = if input.is_a? String
    ADSL::Parser::ADSLParser.new.parse input
  elsif input.is_a? ADSL::Parser::ASTNode
    input.typecheck_and_resolve
  elsif input.is_a? ADSL::DS::DSSpec
    input
  end

  options = default_options.merge options

  stop_on_incorrect = options[:halt_on_error]
  check_satisfiability = options[:check_satisfiability]
  timeout = options[:timeout] || -1
  actions = filter_by_name ds_spec.actions, options[:actions]
  invariants = filter_by_name ds_spec.invariants, options[:invariants]

  @csv_output = ::ADSL::Util::CSVHashFormatter.new

  options[:output] = options[:output].to_sym unless options[:output].nil?
  raise "Unknown verification format `#{options[:output]}'" unless [nil, :terminal, :csv, :silent].include? options[:output]
  @verification_output = options[:output]
  do_stats = @verification_output == :csv
  
  actions = remove_empty_actions actions
  
  if check_satisfiability
    begin
      output "Checking for satisfiability...", nil
      
      translation = nil
      translation_time = Time.time_execution do
        translation = ds_spec.translate_action nil
      end

      result, stats = exec_spass translation, timeout, true
      if do_stats
        stats[:translation_time] = translation_time
        stats[:action] = '<unsatisfiability>'
        stats[:result] = result.to_s
        if input.is_a? ADSL::Parser::ASTNode
          stats[:pre_optimize_size] = input.adsl_ast_size :pre_optimize => true
          stats[:adsl_ast_size] = input.adsl_ast_size
        end
      end

      if result == :correct
        output "\rSatisfiability check #{ 'failed!'.red }                ", stats
        return false
      elsif result == :inconclusive
        output "\rSatisfiability check #{ 'inconclusive'.yellow }        ", stats
      else
        output "\rSatisfiability check #{ 'passed'.green }.              ", stats
      end
    ensure
      output "\n", nil
    end
  end

  all_correct = true
  actions.each do |action|
    invariants.each do |invariant|
      output "Verifying action '#{action.name}' with invariant '#{invariant.name}'...", nil
      begin
        translation = nil
        translation_time = Time.time_execution do
          translation = ds_spec.translate_action action.name, invariant
        end
        result, stats = exec_spass translation, timeout, do_stats
        if do_stats
          stats[:translation_time] = translation_time
          stats[:action] = action.name
          stats[:invariant] = invariant.name
          stats[:result] = result.to_s
          if input.is_a? ADSL::Parser::ASTNode
            stats[:adsl_ast_size] = input.adsl_ast_size(
              :action_name => action.name,
              :invariant_name => invariant.name
            )
            stats[:pre_optimize_size] = input.adsl_ast_size(
              :pre_optimize => true,
              :action_name => action.name,
              :invariant_name => invariant.name
            )
          end
        end

        case result
        when :correct
          output "\rAction '#{action.name}' with invariant '#{invariant.name}': #{ 'correct'.green }     ", stats
        when :incorrect
          output "\rAction '#{action.name}' with invariant '#{invariant.name}': #{ 'incorrect'.red }     ", stats
          all_correct = false
          return false if stop_on_incorrect
        when :inconclusive
          output "\rAction '#{action.name}' with invariant '#{invariant.name}': #{ 'inconclusive'.yellow } ", stats
          all_correct = false
        else
          raise "Unknown exec_spass result: #{result}"
        end
      ensure
        output "\n", nil
      end
    end
  end
  return all_correct
ensure
  puts @csv_output.sort!(:action, :invariant).to_s if @verification_output == :csv
  @csv_output = nil
end