class Bpl::Unstructuring

Public Instance Methods

cond(expr, polarity) click to toggle source
# File lib/bpl/passes/transformation/unstructuring.rb, line 12
def cond(expr, polarity)
  if expr == Expression::Wildcard
    bpl("true")
  elsif polarity
    expr
  else
    bpl("!#{expr}")
  end
end
fresh_id() click to toggle source

depends :cfg_construction

# File lib/bpl/passes/transformation/unstructuring.rb, line 7
def fresh_id
  @id ||= 0
  @id += 1
end
run!(program) click to toggle source
# File lib/bpl/passes/transformation/unstructuring.rb, line 101
def run! program
  work_list = []
  work_list << program

  until work_list.empty?
    root = work_list.shift
    root.each do |stmt|
      if elem = unstructure_conditional(stmt) || unstructure_loop(stmt)
        invalidates :all
        work_list.unshift root
        work_list.unshift elem
        break
      end
    end
  end

end
unstructure_conditional(stmt) click to toggle source
# File lib/bpl/passes/transformation/unstructuring.rb, line 22
def unstructure_conditional(stmt)
  return unless stmt.is_a?(IfStatement)

  block = stmt.parent
  post = block.statements.chunk{|s| s == stmt}.map{|_,s| s}[2]
  id = fresh_id

  stmt.replace_with(bpl("goto $then.#{id}, $else.#{id};"))
  left = []
  right = []

  left << bpl("$then.#{id}: assume #{cond(stmt.condition,true)};").
    append_children(:statements, *stmt.blocks.first.statements.dup)
  left.push(*stmt.blocks.drop(1))
  left.last.append_children(:statements, bpl("goto $merge.#{id};"))

  right << bpl("$else.#{id}: assume #{cond(stmt.condition,false)};")
  if stmt.else.is_a?(IfStatement)
    right.first.append_children(:statements, stmt.else)
  elsif stmt.else
    right.first.append_children(:statements,
      *stmt.else.first.statements.dup)
    right.push(*stmt.else.drop(1))
  end
  right.last.append_children(:statements, bpl("goto $merge.#{id};"))

  tail = bpl("$merge.#{id}: assume true;").
    append_children(:statements, *post)

  block.insert_after(*left, *right, tail)

  return block.parent
end
unstructure_loop(stmt) click to toggle source
# File lib/bpl/passes/transformation/unstructuring.rb, line 56
def unstructure_loop(stmt)
  return unless stmt.is_a?(WhileStatement)

  block = stmt.parent
  post = block.statements.chunk{|s| s == stmt}.map{|_,s| s}[2]
  id = fresh_id

  stmt.replace_with(bpl("goto $head.#{id};"))

  head = bpl("$head.#{id}: goto $body.#{id}, $exit.#{id};").
    prepend_children(:statements,
      *stmt.invariants.reverse.map {|i| bpl("assert #{i.expression};")})

  body = []
  body << bpl("$body.#{id}: assume #{cond(stmt.condition,true)};").
    append_children(:statements, *stmt.blocks.first.statements.dup)
  body.push(*stmt.blocks.drop(1))
  body.last.append_children(:statements, bpl("goto $head.#{id};"))

  has_break = false
  body.each do |blk|
    blk.each do |br|
      next unless br.is_a?(BreakStatement)
      next if br.each_ancestor.any? {|w| w.is_a?(WhileStatement)}
      fail "Unexpected break statement." unless br.identifier.nil?
      rest = br.parent.statements.chunk{|s| s == br}.map{|_,s| s}[2] || []
      br.replace_with(bpl("goto $break.#{id};"))
      rest.each(&:remove)
      has_break = true
    end
  end

  exits = []
  exits << bpl("$exit.#{id}: assume #{cond(stmt.condition,false)};")
  if has_break
    exits.first.append_children(:statements, bpl("goto $break.#{id};"))
    exits << bpl("$break.#{id}: assume true;")
  end
  exits.last.append_children(:statements, *post)

  block.insert_after(head, *body, *exits)

  return block.parent
end