class Bpl::Normalization
Public Class Methods
sanity_check(program)
click to toggle source
TODO OBSOLETE CODE
# File lib/bpl/passes/transformation/normalization.rb, line 53 def self.sanity_check program program.each do |elem| case elem when CallStatement abort "found call to entry point procedure #{elem.procedure}." \ if elem.target && elem.target.is_entrypoint? when AssumeStatement abort "found :startpoint annotation." \ if elem.attributes.include? :startpoint abort "found :endpoint annotation." \ if elem.attributes.include? :endpoint end end end
uniq_starts_and_ends!(program)
click to toggle source
TODO OBSOLETE CODE
# File lib/bpl/passes/transformation/normalization.rb, line 70 def self.uniq_starts_and_ends! program program << bpl("var $e: bool;") program.declarations.each do |proc| next unless proc.is_a?(ProcedureDeclaration) && proc.body proc.specifications << bpl("modifies $e;", scope: program) if proc.is_entrypoint? proc.body.first.unshift bpl("$e := false;", scope: program) proc.body.first.unshift bpl("assume {:startpoint} true;") else ## this branch costs extra, on the order of 10s in my tests # proc.body.statements.unshift bpl("if ($e) { goto $exit; }") end case proc.body.last.last when GotoStatement, ReturnStatement else proc.body.last << bpl("return;") end exit_block = if proc.is_entrypoint? then bpl(<<-END, scope: program) $exit: assume {:endpoint} true; assume $e; assert false; return; END else bpl("$exit: return;") end # an artificial scope containing the exit block scope = [Body.new(blocks: [exit_block]), proc.body, proc, program] proc.body.each do |stmt| case stmt when AssertStatement stmt.replace_with \ bpl("if (!#{stmt.expression}) { $e := true; goto $exit; }", scope: scope) when CallStatement # TODO why do these "optimizations" make things slower?? # next s unless s.target && s.target.body # next s if s.target.attributes.include?(:atomic) # next s unless s.target.modifies.include?(bpl("$e").resolve!(program)) # next s if s.target.attributes.include?(:async) # next [s, bpl("if ($e) { goto $exit; }", scope: scope)] stmt.insert_after bpl("if ($e) { goto $exit; }", scope: scope) when AssumeStatement if stmt.attributes.include? :yield stmt.insert_after bpl("if ($e) { goto $exit; }", scope: scope) end when ReturnStatement stmt.replace_with bpl("goto $exit;", scope: scope) end end proc.body << exit_block end end
Public Instance Methods
run!(program)
click to toggle source
# File lib/bpl/passes/transformation/normalization.rb, line 7 def run! program # TODO specify what normalization should be doing program.each do |elem| case elem when AssignStatement if elem.lhs.count > 1 info "NORMALIZING MULTI-ASSIGNMENT" info info elem.to_s.indent info writes = elem.lhs.map(&:ident).map(&:name) unless elem.rhs.any? do |e| e.any? do |x| x.is_a?(StorageIdentifier) && writes.include?(x.name) end end then # the simple case, no conflicts elem.replace_with( *elem.lhs.count.times.map do |i| bpl("#{elem.lhs[i]} := #{elem.rhs[i]};") end ) else # the complicated case, read all before writing any p = elem.each_ancestor.find{|d| d.is_a?(ProcedureDeclaration)} vars = elem.lhs.count.times.map do |i| p.fresh_var(elem.lhs[i].type) end elem.replace_with( *vars.map.with_index {|x,i| bpl("#{x} := #{elem.rhs[i]};")}, *vars.map.with_index {|x,i| bpl("#{elem.lhs[i]} := #{x};")} ) end invalidates :all end end end # TODO what to do with this stuff? # sanity_check program # uniq_starts_and_ends! program end