class Bpl::Verification

Public Instance Methods

add_inline_annotations!(program, unroll) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 373
def add_inline_annotations! program, unroll
  program.declarations.each do |d|
    if d.is_a?(ProcedureDeclaration) && d.body && !d.is_entrypoint?
      d.attributes[:inline] = [bpl("#{unroll || 1}")]
    end
  end
end
prepare_for_boogie_fi!(program, unroll) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 369
def prepare_for_boogie_fi! program, unroll
  add_inline_annotations! program, unroll
end
prepare_for_boogie_si!(program) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 381
def prepare_for_boogie_si! program
  program.declarations.each do |proc|
    next unless proc.is_entrypoint?
    proc.body.each do |stmt|
      next unless stmt.is_a?(AssertStatement)
      stmt.remove
    end
  end
end
run!(program, options = {}) click to toggle source

option :verifier, “which verifier to use (boogie, corral, …)” option :incremental, “do incremental verification?” option :parallel, “do verification in parallel?” option :unroll, “the loop/procedure unrolling bound” option :timeout, “verifier time limit” option :trace_file, “file for storage of traces” option :debug_solver, “enable solver debugging”

# File lib/bpl/passes/utility/verification.rb, line 15
def run!(program, options = {})

  # begin
  #   require 'eventmachine'
  # rescue LoadError
  #   warn "Parallel verification requires the eventmachine gem; disabling." if @parallel
  #   @parallel = false
  # end

  if options[:incremental] && options[:parallel]
    verify_parallel_accelerated program, options
  elsif options[:incremental]
    verify_incremental program, options
  else
    verify_one_shot program, options
  end
end
verify_incremental(program, options = {}) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 67
def verify_incremental(program, options = {})
  unroll_bound = options[:unroll] || Float::INFINITY
  rounds_bound = options[:rounds] || Float::INFINITY

  unroll = 0
  rounds = 1

  done = false
  trace = nil
  last = start = Time.now

  printer = Thread.new do
    until done do
      print (" " * 80 + "\r")
      print \
        "Verifying w/ depth #{unroll} and #{rounds} rounds " \
        "(#{(Time.now - last).round}s) total #{(Time.now - start).round}s" \
        "\r" unless $quiet
      sleep 1
    end
  end

  while true
    last = Time.now
    break if trace = vvvvv(program, options.merge(unroll: unroll, rounds: rounds))
    break if round >= rounds_bound && unroll >= unroll_bound

    if (rounds < rounds_bound && rounds < unroll) || unroll >= unroll_bound
      rounds += 1
    else
      unroll += 1
    end
  end
  done = true
  printer.join
  puts unless $quiet

  if trace == :timeout
    puts "Verification timed out." unless $quiet
  elsif trace
    puts "Got a trace w/ depth #{unroll} and #{rounds} rounds." unless $quiet
  else
    puts "Verified up to depth #{unroll} w/ #{rounds} rounds." unless $quiet
  end

  return trace
end
verify_one_shot(program, options = {}) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 33
def verify_one_shot(program, options = {})
  unroll = options[:unroll]
  rounds = options[:rounds]

  done = false
  trace = nil
  start = Time.now

  printer = Thread.new do
    until done do
      print (" " * 80 + "\r")
      print \
        "Verifying w/ depth #{unroll || "inf."} and #{rounds} rounds " \
        "(#{(Time.now - start).round}s)" \
        "\r" unless $quiet
      sleep 1
    end
  end

  trace = vvvvv(program, options)
  done = true
  printer.join
  puts unless $quiet

  if trace == :timeout
    puts "Verification timed out." unless $quiet
  elsif trace
    puts "Got a trace w/ depth #{unroll || "inf."} and #{rounds} rounds." unless $quiet
  else
    puts "Verified w/ depth #{unroll || "inf."} and #{rounds} rounds." unless $quiet
  end
  return trace
end
verify_parallel_accelerated(program, options = {}) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 115
def verify_parallel_accelerated(program, options = {})
  unroll_bound = options[:unroll] || Float::INFINITY
  rounds_bound = options[:rounds] || Float::INFINITY

  done = 0

  unroll_lower = 0
  round_lower = 0

  tasks = [nil, nil]
  start = Time.now
  trace = nil

  EventMachine.run do
    EventMachine.add_periodic_timer(0.5) do
      print (" " * 80 + "\r")
      print \
        "Verifying in parallel w/ unroll/rounds " \
        "#{tasks[0] ? "#{tasks[0][:unroll]}/#{tasks[0][:rounds]}" : "-/-"} " \
          "(#{tasks[0] ? (Time.now - tasks[0][:time]).round : "-"}s) and " \
        "#{tasks[1] ? "#{tasks[1][:unroll]}/#{tasks[1][:rounds]}" : "-/-"} " \
          "(#{tasks[1] ? (Time.now - tasks[1][:time]).round : "-"}s) " \
        "total #{(Time.now - start).round}s" \
        "\r" unless $quiet
    end

    (0..1).each do |i|
      EventMachine.defer do
        while true
          unroll = unroll_lower
          rounds = round_lower
          mode = tasks[i] ? tasks[i][:mode] : (i == 0 && :unroll || i == 1 && :rounds)
          mode = :unroll if rounds == rounds_bound
          mode = :rounds if unroll == unroll_bound
          unroll += 1 if mode == :unroll
          rounds += 1 if mode == :rounds
          if unroll > unroll_bound || rounds > round_bound
            tasks[i] = nil
            break
          end
          tasks[i] = {mode: mode, time: Time.now, unroll: unroll, rounds: rounds}

          if trace = vvvvv(program, options.merge(unroll: unroll, rounds: rounds)) then
            EventMachine.stop
            puts unless $quiet
            if trace == :timeout
              puts "Verification timed out." unless $quiet
            else
              puts "Got a trace w/ depth #{unroll} and #{rounds} rounds." unless $quiet
            end
            break
          end
          unroll_lower += 1 if i == 0
          rounds_lower += 1 if i == 1
        end
        if (done += 1) >= 2
          EventMachine.stop
          puts unless $quiet
        end
      end
    end
  end

  puts "Verified up to depth #{unroll_bound} w/ #{rounds_bound} rounds." \
    unless trace || $quiet

  return trace
end
verify_parallel_worklist(program, options = {}) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 184
def verify_parallel_worklist(program, options = {})
  unroll_bound = options[:unroll] || Float::INFINITY
  # round_bound = options[:rounds] || Float::INFINITY

  covered = []
  worklist = [{unroll: 0, rounds: 0}, {unroll: 1, rounds: 0}]
  tasks = [nil, nil]
  start = Time.now
  trace = nil
  idle = 0

  # EventMachine.threadpool_size = 2
  EventMachine.run do
    EventMachine.add_periodic_timer(0.5) do
      print (" " * 80 + "\r")
      print \
        "Verifying in parallel w/ unroll/rounds " \
        "#{tasks[0] ? "#{tasks[0][:unroll]}/#{tasks[0][:rounds]}" : "-/-"} " \
          "(#{tasks[0] ? (Time.now - tasks[0][:time]).round : "-"}s) and " \
        "#{tasks[1] ? "#{tasks[1][:unroll]}/#{tasks[1][:rounds]}" : "-/-"} " \
          "(#{tasks[1] ? (Time.now - tasks[1][:time]).round : "-"}s) " \
        "total #{(Time.now - start).round}s" \
        "\r" unless $quiet
    end

    (0..1).each do |i|
      EventMachine.defer do
        while true
          work = worklist.shift
          break unless work
          unroll = work[:unroll]
          rounds = work[:rounds]
          next if covered.any?{|w| w[:unroll] >= unroll && w[:rounds] >= rounds}
          covered.reject!{|w| w[:unroll] <= unroll && w[:rounds] <= rounds}
          covered << work

          tasks[i] = {time: Time.now, unroll: unroll, rounds: rounds}

          if trace = vvvvv(program, options.merge(unroll: unroll, rounds: rounds)) then
            EventMachine.stop
            puts unless $quiet
            if trace == :timeout
              puts "Verification timed out." unless $quiet
            else
              puts "Got a trace w/ depth #{unroll} and #{rounds} rounds." unless $quiet
            end
            break
          else
            worklist.reject!{|w| w[:unroll] <= unroll && w[:rounds] <= rounds}
            worklist << {unroll: unroll+1, rounds: rounds} if unroll < unroll_bound
            worklist << {unroll: unroll, rounds: rounds+1} if rounds < rounds_bound
          end
        end
        tasks[i] = nil
        EventMachine.stop if (idle += 1) >= 2
      end
    end
  end

  puts "Verified up to depth #{unroll_bound} w/ #{rounds_bound} rounds." \
    unless trace || $quiet
  return trace
end
vvvvv(program, options = {}) click to toggle source
# File lib/bpl/passes/utility/verification.rb, line 248
def vvvvv(program, options = {})
  boogie_opts = []

  orig = program.source_file || "a.bpl"
  base = File.basename(orig).chomp(File.extname(orig))
  $temp << src = "#{base}.bam.#{Time.now.to_f}.bpl"
  $temp << model_file = src.chomp('.bpl') + '.model'
  $temp << trace_file = src.chomp('.bpl') + '.trace'

  unless options[:unroll]
    case options[:verifier]
    when :boogie_fi
      warn "without loop unrolling, Boogie may be imprecise"
    else
      warn "without specifying an unroll bound, Boogie may not terminate"
    end
  end

  case options[:verifier]
  when :boogie_fi, nil
    boogie_opts << "/loopUnroll:#{options[:unroll]}" if options[:unroll]
    prepare_for_boogie_fi!(program, options[:unroll])

  when :boogie_si
    boogie_opts << "/stratifiedInline:2"
    boogie_opts << "/extractLoops"
    boogie_opts << "/recursionBound:#{options[:unroll]}" if options[:unroll]
    boogie_opts << "/weakArrayTheory"
    boogie_opts << "/siVerbose:1" if $verbose
    prepare_for_boogie_si! program

  else
    err "invalid back-end: #{options[:verifier]}"
  end

  # boogie_opts << "/useArrayTheory" # NOTE always slower for mje

  boogie_opts << "/errorLimit:1"
  boogie_opts << "/errorTrace:2"
  boogie_opts << "/printModel:4"
  boogie_opts << "/printModelToFile:#{model_file}"
  boogie_opts << "/removeEmptyBlocks:0" # XXX
  boogie_opts << "/coalesceBlocks:0"    # XXX

  boogie_opts << "/timeLimit:#{options[:timeout]}" if options[:timeout]
  boogie_opts << "/proverOpt:C:TRACE=true" if options[:debug_solver]

  if program.declarations.any?{|d| d.is_a?(ConstantDeclaration) && d.names.include?('#ROUNDS')}
    program.declarations.push bpl("axiom #ROUNDS == #{options[:rounds]};")
  end
  if program.declarations.any?{|d| d.is_a?(FunctionDeclaration) && d.name == '$R'}
    (0..(options[:rounds]-1)).each do |i|
      program.declarations.push bpl("axiom $R(#{i});")
    end
  end
  File.write(src,program)
  if program.declarations.any?{|d| d.is_a?(ConstantDeclaration) && d.names.include?('#ROUNDS')}
    program.declarations.pop
  end

  cmd = "#{boogie} #{src} #{boogie_opts * " "} 1> #{trace_file}"
  puts cmd.bold if $verbose
  # t = Time.now

  system cmd
  output = File.read(trace_file).lines

  if output.grep(/Boogie program verifier finished/).empty?
    abort begin
      "there was a problem running Boogie." +
      ($verbose ? "\n" + output.drop(1) * "\n" : "")
    end
  end

  has_errors = output.last.match(/(\d+) error/){|m| m[1].to_i > 0}
  timeout = output.last.match(/(\d+) time out/){|m| m[1].to_i > 0}

  if timeout
    trace = :timeout
  elsif has_errors
    model = Z3::Model.new(model_file)
    trace = Trace.new(trace_file, program, model)
  else
    trace = nil
  end

  return trace

  # output = `#{cmd}`

  # res = output.match /(\d+) verified, (\d+) errors?/ do |m| m[2].to_i > 0 end
  # warn "unexpected Boogie result: #{output}" if res.nil?

  # res = nil if output.match(/ \d+ time outs?/)

  # time = output.match /Boogie finished in ([0-9.]+)s./ do |m| m[1].to_f end
  # warn "unknown Boogie time" unless time

  # puts "#{res.nil? ? "TO" : res} / #{time} / #{args.reject{|k,_| k =~ /limit/}}"
  # return res

  # cleanup = []
  # if not $?.success? then
  #   err "problem with Boogie: #{output}"
  # else
  #   if @graph && output =~ /[1-9]\d* errors?/ then
  #     puts "Rendering error trace.." unless @quiet
  #     File.open("#{src}.trace",'w'){|f| f.write(output) }
  #     showtrace "#{src}.trace"
  #   else
  #     if @@quiet then
  #       puts output.lines.select{|l| l =~ /[0-9]* verified/}[0]
  #     else
  #       puts output.lines.reject{|l| l.strip.empty?} * ""
  #     end
  #   end
  # end
  # File.delete( *cleanup ) unless @keep
  # puts "Boogie finished in #{Time.now - t}s." unless @@quiet
end