module BAM
def self.violin_instrument! program, monitor methods = {} monitor_vars = [] specs = [] inits = [] program.declarations += BoogieLanguage.new.parse(File.read(monitor)).declarations program.declarations.each do |decl| if decl.is_a?(AxiomDeclaration) && decl.attributes.include?(:method) ax = decl.attributes[:method] methods.merge!({ax[0] => ax[1]}) elsif decl.is_a?(VariableDeclaration) && decl.attributes.include?(:monitor_vars) monitor_vars += decl.names.map{|id| bpl(id)} elsif decl.is_a?(FunctionDeclaration) && decl.attributes.include?(:spec) specs << decl elsif decl.is_a?(ProcedureDeclaration) && decl.attributes.include?(:monitor_init) inits << decl end end program.declarations.each do |decl| case decl when ProcedureDeclaration next unless decl.body unless (new_mods = monitor_vars - decl.modifies).empty? decl.specifications << bpl("modifies #{new_mods * ", "};") end if methods.include?(decl.name) params = decl.parameters.map{|p| p.names}.flatten rets = ["$myop"] + decl.returns.map{|r| r.names}.flatten decl.body.declarations << bpl("var $myop: int;") decl.body.statements.unshift \ bpl("call $myop := #{methods[decl.name]}.start(#{params * ","});") decl.body.each do |stmt| if stmt.is_a?(ReturnStatement) stmt.insert_before \ bpl("call #{methods[decl.name]}.finish(#{rets * ","});"), end end end decl.body.each do |stmt| case stmt when AssumeStatement if stmt.attributes.include? :startpoint stmt.insert_after \ inits.reverse.map{|init| bpl("call #{init.name}();")} end when AssertStatement if stmt.attributes.include?(:spec) && (ax = stmt.attributes[:spec]) && !ax.empty? && (name = ax.first) && (spec = specs.detect{|s| s.name == name}) then stmt.replace_with \ bpl("assert #{spec.name}(#{spec.arguments.map{|arg| arg.names}.flatten * ","});") end end end end end end
end