class Bpl::Simplification
Public Instance Methods
readonly_variable?(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 30 def readonly_variable?(elem) elem.is_a?(VariableDeclaration) && elem.bindings.none? do |b| b.parent && ( b.parent.is_a?(HavocStatement) || ( b.parent.is_a?(AssignStatement) && b.parent.lhs.include?(b) ) ) end end
run!(program)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 146 def run! program program.each(&method(:simplify)) end
simplify(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 91 def simplify(elem) cfg = cfg_construction case when trivial_statement?(elem) info "removing trivial element: #{elem}" elem.remove if elem.is_a?(AssertStatement) invalidates :assertion_localization redo! end when readonly_variable?(elem) && elem.parent && elem.parent.is_a?(Program) # NOTE Boogie does not permit local constant declarations info "converting read-only variable to constant: #{elem}" elem.replace_with(bpl("const #{elem.names * ", "}: #{elem.type};")) invalidates :resolution redo! when unused_storage?(elem) if elem.parent.is_a?(Program) invalidates :modification redo! end info "removing unused storage: #{elem.names * ", "}" elem.bindings. map {|b| b.siblings.count > 1 ? b : b.parent}. each(&:remove) elem.remove when trivial_implementation?(elem) info "removing body of procedure: #{elem.name}" elem.replace_children(:body, nil) when trivial_block?(elem) info "removing trivial block: #{elem.name}" pred = cfg.predecessors[elem].first pred.statements.last.replace_with(elem.statements.last) if pred elem.remove invalidates :resolution invalidates :cfg_construction redo! when trivial_branch?(elem) info "removing trivial branch: #{elem.name}" elem.statements.last. replace_with(cfg.successors[elem].first.statements.last.copy) cfg.successors[elem].each(&:remove) invalidates :cfg_construction redo! end end
trivial_block?(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 60 def trivial_block?(elem) cfg = cfg_construction elem.is_a?(Block) && elem.parent && elem.statements.count == 1 && elem.statements.first.is_a?(GotoStatement) && elem.statements.first.identifiers.count == 1 && (preds = cfg.predecessors[elem]) && (preds.count <= 1) && (!preds.first || preds.first.statements.last.is_a?(GotoStatement)) && (!preds.first || preds.first.statements.last.identifiers.count == 1) end
trivial_branch?(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 74 def trivial_branch?(elem) cfg = cfg_construction elem.is_a?(Block) && cfg.successors[elem].count == 2 && elem.statements.last.is_a?(GotoStatement) && elem.statements.last.identifiers.count == 2 && (b1, b2 = cfg.successors[elem].to_a) && (b1 != b2) && cfg.successors[b1].count == 1 && cfg.successors[b1] == cfg.successors[b2] && b1.statements.count == 1 && b1.statements.last.is_a?(GotoStatement) && b2.statements.count == 1 && b2.statements.last.is_a?(GotoStatement) end
trivial_implementation?(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 48 def trivial_implementation?(elem) mods = modification asserts = assertion_localization elem.is_a?(ProcedureDeclaration) && elem.body && !asserts.has_assert[elem] && mods.modifies[elem].empty? && elem.returns. all? {|x| x.bindings.all? {|b| b.parent.is_a?(HavocStatement)}} end
trivial_statement?(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 11 def trivial_statement?(elem) mods = modification asserts = assertion_localization case elem when AxiomDeclaration, AssumeStatement, AssertStatement (expr = elem.expression) && (expr.is_a?(BooleanLiteral)) && (expr.value == true) when CallStatement (decl = elem.procedure.declaration) && mods.modifies[decl].empty? && decl.returns.empty? && !asserts.has_assert[decl] else false end end
unused_storage?(elem)
click to toggle source
# File lib/bpl/passes/transformation/simplification.rb, line 42 def unused_storage?(elem) (elem.is_a?(VariableDeclaration) || elem.is_a?(ConstantDeclaration)) && elem.bindings.map(&:parent). all? {|n| n.is_a?(HavocStatement) || n.is_a?(ModifiesClause)} end