module ADSL::Spass::Bin

Public Instance Methods

default_options() click to toggle source
# 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) click to toggle source
# 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) click to toggle source
# 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) click to toggle source
# 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) click to toggle source
# 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) click to toggle source
# 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={}) click to toggle source
# 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