class Bpl::CtAnnotation
Constants
- BLOCK_ANNOTATIONS
- FUNCTION_ANNOTATIONS
- LOOP_ANNOTATIONS
- VARIABLE_ANNOTATIONS
Public Instance Methods
run!(program)
click to toggle source
# File lib/bpl/passes/security/ct_annotation.rb, line 27 def run! program cfg = cfg_construction program.declarations.each do |decl| next unless decl.is_a?(ProcedureDeclaration) next unless decl.body values = {} decl.body.each do |stmt| next unless stmt.is_a?(CallStatement) if stmt.procedure.name =~ /__SMACK_value/ name = stmt.attributes.find{|a| a.key =~ /name/} kind = stmt.attributes.find{|a| a.key =~ /array|field/} values[stmt.assignments.first.name] = { id: name.values.first, kind: kind && kind.key, access: kind && kind.values } elsif stmt.procedure.name =~ /#{VARIABLE_ANNOTATIONS * "|"}/ var = stmt.arguments.first.name v = values[var] fail "Unknown value: #{var}" unless v access = v[:access] || [v[:id]] decl.append_children(:specifications, bpl("requires {:#{stmt.procedure.name} #{access * ", "}} true;") ) invalidates :resolution stmt.remove elsif stmt.procedure.name =~ /#{FUNCTION_ANNOTATIONS * "|"}/ var = stmt.arguments.first decl.append_children(:specifications, bpl("requires {:#{stmt.procedure.name} #{var}} true;") ) invalidates :resolution stmt.remove elsif stmt.procedure.name =~ /#{BLOCK_ANNOTATIONS * "|"}/ head = cfg.predecessors[stmt.parent].first cond = conditional_identification.conditionals[head] next unless cond cond[:blocks].each do |blk| fail "Unexpected conditional exits" if cond[:exits].count > 1 block_list = ([head] + cond[:exits].first(1)).map(&:name) blk.prepend_children(:statements, bpl("assume true;")) blk.statements.first.add_attribute(:selfcomp, *block_list) end stmt.remove elsif stmt.procedure.name =~ /#{LOOP_ANNOTATIONS * "|"}/ var = stmt.arguments.first stmt.insert_after((bpl("assume {:loop_var #{var}} true;"))) stmt.remove end end end end