module Bpl
module Transformation class DfAsyncRemoval < Bpl::Pass def self.description "The async-to-call part of the EQR sequentialization." end def run! program return unless program.any? {|elem| elem.attributes.include?(:async)} globals = program.global_variables gs = globals.map(&:idents).flatten if globals.empty? program.each {|elem| elem.attributes.delete(:async)} return end globals.each do |decl| program << bpl( "var #{decl.names.map{|g| "#{g}.next"} * ", "}: #{decl.type};" ) end program.declarations.each do |proc| next unless proc.is_a?(ProcedureDeclaration) next unless proc.body accs = (proc.accesses & gs).sort mods = accs - proc.modifies proc.specifications << bpl("modifies #{mods * ", "};", scope: program) \ unless mods.empty? proc.specifications << bpl("modifies #{accs.map{|g| "#{g}.next"} * ", "};", scope: program) \ unless accs.empty? globals.each do |decl| proc.body.declarations << bpl("var #{decl.names.map{|g| "#{g}.start"} * ", "}: #{decl.type};") end if proc.is_entrypoint? globals.each do |decl| proc.body.declarations << bpl("var #{decl.names.map{|g| ["#{g}.save", "#{g}.guess"]}.flatten * ", "}: #{decl.type};") end if proc.body.any? {|elem| elem.attributes.include?(:async)} scope = [proc.body, proc, program] proc.body.each do |stmt| case stmt when AssumeStatement if stmt.attributes.include? :startpoint stmt.insert_before \ *(accs.map{|g| bpl("#{g}.next := #{g}.start;", scope: scope)}) elsif stmt.attributes.include? :endpoint stmt.insert_after *( accs.map{|g| bpl("assume #{g} == #{g}.start;", scope: scope)} + accs.map{|g| bpl("#{g} := #{g}.next;", scope: scope)}) # elsif elem.attributes.include? :pause # next gs.map{|g| bpl("#{g}.save := #{g};")} + # gs.map{|g| bpl("#{g} := #{g}.next;")} + # gs.map{|g| bpl("havoc #{g}.guess;")} + # gs.map{|g| bpl("#{g}.next := #{g}.guess;")} # # elsif elem.attributes.include? :resume # next gs.map{|g| bpl("assume #{g} == #{g}.guess;")} + # gs.map{|g| bpl("#{g} := #{g}.save;")} end when CallStatement called = stmt.target if stmt.attributes.include? :async then # var = elem.attributes[:async].first stmt.attributes.delete :async # replace the return assignments with dummy assignments stmt.assignments.map! do |x| proc.fresh_var(x.declaration.type) end # make sure to pass the 'save'd version of any globals stmt.arguments.map! do |e| e.replace! do |e| e.is_a?(Identifier) && globals.include?(e.declaration) ? e.save : e end end call_mods = (called ? called.modifies & gs : gs).sort call_accs = (called ? called.accesses & gs : gs).sort # call_accs = call_mods # some async-simulating guessing magic stmt.insert_before *( call_accs.map{|g| bpl("#{g}.save := #{g};", scope: scope)} + call_accs.map{|g| bpl("#{g} := #{g}.next;", scope: scope)} + call_mods.map{|g| bpl("havoc #{g}.guess;", scope: scope)} + call_mods.map{|g| bpl("#{g}.next := #{g}.guess;", scope: scope)}) # [ bpl("#tasks := #tasks + 1;") ] + # (var ? [bpl("#{var} := #tasks;")] : []) + stmt.insert_after *( call_mods.map{|g| bpl("assume #{g} == #{g}.guess;", scope: scope)} + call_accs.map{|g| bpl("#{g} := #{g}.save;", scope: scope)}) else # a synchronous procedure call # elem.arguments << bpl("#t") if called && called.body end end end end Bpl::Analysis::correct_modifies! program end end end
end