class Bpl::Extraction
Public Instance Methods
extract(condition, invariants, blocks, params, locals)
click to toggle source
# File lib/bpl/passes/transformation/extraction.rb, line 12 def extract(condition, invariants, blocks, params, locals) id = fresh_id accs = blocks.collect do |b| b.collect {|x| x.name if x.is_a?(StorageIdentifier)}.compact end.flatten.uniq mods = blocks.collect do |b| b.collect do |s| Modification.stmt_modifies(s).map(&:name) if s.is_a?(Statement) end.compact.flatten end.flatten.uniq local_mods, global_mods = mods.partition {|x| locals.include?(x)} local_accs = (accs - mods). select {|x| params.include?(x) || locals.include?(x)} exits = blocks.collect do |b| b.select do |x| x.is_a?(LabelIdentifier) && blocks.none? {|bb| bb.names.include?(x.name)} end end.flatten.uniq(&:name) decl = bpl("procedure $loop.#{id}();") local_accs.each do |x| decl.append_children(:parameters, StorageDeclaration.new(names: [x], type: params[x] || locals[x])) end local_mods.each do |x| decl.append_children(:parameters, StorageDeclaration.new(names: [x + ".0"], type: locals[x])) decl.append_children(:returns, StorageDeclaration.new(names: [x], type: locals[x])) end unless global_mods.empty? decl.append_children(:specifications, bpl("modifies #{global_mods * ", "};")) end invariants.each do |i| decl.append_children(:specifications, bpl("requires #{i.expression};"), bpl("ensures #{i.expression};") ) end decl.append_children(:specifications, bpl("ensures !#{condition};")) decl.append_children(:body, Body.new(locals: [], blocks: [])) decl.body.append_children(:blocks, bpl("$entry: goto #{blocks.first.name};")) if blocks.first.name decl.body.append_children(:blocks, *blocks.map(&:copy)) decl.body.blocks.first.prepend_children(:statements, *local_mods.map{|x| bpl("#{x} := #{x}.0;")}) decl.body.append_children(:blocks, *exits.map {|l| bpl("#{l}: assume !#{condition}; return;")}) stmt = bpl %{ call #{local_mods * ", "} #{":=" unless local_mods.empty?} $loop.#{id}(#{(local_accs + local_mods) * ", "}); } return decl, stmt end
fresh_id()
click to toggle source
# File lib/bpl/passes/transformation/extraction.rb, line 7 def fresh_id @id ||= 0 @id += 1 end
run!(program)
click to toggle source
# File lib/bpl/passes/transformation/extraction.rb, line 76 def run! program program.declarations.each do |proc| next unless proc.is_a?(ProcedureDeclaration) next unless proc.body params = proc.parameters. map {|x| x.names.product([x.type])}.flatten(1).to_h locals = (proc.returns + proc.body.locals). map {|x| x.names.product([x.type])}.flatten(1).to_h proc.each(preorder: false) do |stmt| next unless stmt.is_a?(WhileStatement) next if stmt.invariants.empty? info "EXTRACTING WHILE LOOP" info info stmt.to_s.indent info block = Block.new(names: [], statements: [stmt.copy]) decl, call = extract( stmt.condition, stmt.invariants, [block], params, locals) program.append_children(:declarations, decl) stmt.replace_with(call) invalidates :all end end loop_identification.loops.each do |head,body| proc = head.parent.parent params = proc.parameters. map {|x| x.names.product([x.type])}.flatten(1).to_h locals = (proc.returns + proc.body.locals). map {|x| x.names.product([x.type])}.flatten(1).to_h # NOTE filter out previously-removed blocks from nested loops body = body.select{|b| b.parent} ls = head.select {|l| l.is_a?(LabelIdentifier)}.map(&:name) exits = ls.select {|l| body.none? {|b| b.names.include?(l)}} entry = body. collect {|b| b.statements.first if !(b.names & (ls-exits)).empty?}. compact fail "Unexpected loop condition." unless entry.count == 1 && entry.first.is_a?(AssumeStatement) condition = entry.first.expression invariants = [] head.statements.each do |stmt| case stmt when AssertStatement invariants << stmt when AssumeStatement else break end end next if invariants.empty? info "EXTRACTING LOOP" info info "#{(body.to_a * "\n\n").indent}" info decl, call = extract( condition, invariants, body.map(&:copy), params, locals) program.append_children(:declarations, decl) head.replace_children(:statements, call, bpl("goto #{exits * ", "};")) body.each {|b| b.remove if b != head} invalidates :all end end