Class: ADSL::Parser::ASTSpec

Inherits:

ASTNode

• Object
• ASTNode
• ADSL::Parser::ASTSpec

Defined in:

lib/adsl/parser/ast_nodes.rb

Instance Method Summary

• #adsl_ast_size(options = {}) ⇒ Object
• #to_adsl ⇒ Object
• #typecheck_and_resolve ⇒ Object

Methods inherited from ASTNode

#==, #adsl_ast, #block_replace, #dup, #hash, is_formula?, is_objset?, is_statement?, node_type, #objset_has_side_effects?, #optimize, #preorder_traverse

Methods included from Verification::FormulaGenerators

#[], #and, #binary_op, #binary_op_with_any_number_of_params, #equiv, #exists, #false, #forall, #handle_quantifier, #implies, #in_formula_builder, #not, #or, #true

Methods included from Verification::Utils

#classname_for_classname, #infer_classname_from_varname, #t

Instance Method Details

#adsl_ast_size(options = {}) ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 266

def adsl_ast_size(options = {})
  sum = 1
  @classes.each do |c|
    sum += c.adsl_ast_size
  end
  actions = options[:action_name].nil? ? @actions : @actions.select{ |a| a.name.text == options[:action_name] }
  actions.each do |a|
    sum += options[:pre_optimize] ? a.pre_optimize_adsl_ast_size : a.adsl_ast_size
  end
  invs = options[:invariant_name].nil? ? @invariants : @invariants.select{ |a| a.name.text == options[:invariant_name] }
  invs.each do |i|
    sum += i.adsl_ast_size
  end
  sum
end

#to_adsl ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 262

def to_adsl
  "#{ @classes.map(&:to_adsl).join }\n#{ @actions.map(&:to_adsl).join }\n#{ @invariants.map(&:to_adsl).join }"
end

#typecheck_and_resolve ⇒ Object

# File 'lib/adsl/parser/ast_nodes.rb', line 180

def typecheck_and_resolve
  context = ASTTypecheckResolveContext.new

  # make sure class names are unique
  @classes.each do |class_node|
    if context.classes.include? class_node.name.text
      raise ADSLError, "Duplicate class name '#{class_node.name.text}' on line #{class_node.name.lineno} (first definition on line #{context.classes[class_node.name.text][0].name.lineno}"
    end
    klass = ADSL::DS::DSClass.new :name => class_node.name.text
    context.classes[klass.name] = [class_node, klass]
  end

  # make sure the parent classes are declared properly and that the inheritance graph is non-cyclic
  parents = Hash.new{}
  context.classes.values.select{ |v| v[0].parent_name }.each do |class_node, klass|
    parent_node, parent = context.classes[class_node.parent_name.text]
    raise ADSLError, "Unknown parent class name #{class_node.parent_name.text} for class #{class_node.name.text} on line #{class_node.parent_name}" if parent.nil?
    klass.parent = parent

    parents[klass] = parent
    parent_chain = [klass]
    while parent != nil do
      if parent_chain.include? parent
        cyclic_chain = parent_chain.slice(parent_chain.index(parent), parent_chain.length) + [parent]
        raise ADSLError, "Cyclic inheritance detected: #{cyclic_chain.map{ |c| c.name }.join ' -> '}"
      end
      parent_chain << parent
      parent = parents[parent]
    end
  end

  # make sure relations are valid and refer to existing classes
  context.classes.values.each do |class_node, klass|
    class_node.relations.each do |rel_node|
      iter = klass
      while iter != nil
        if context.relations[iter.name].include? rel_node.name.text
          raise ADSLError, "Duplicate relation name '#{class_node.name.text}' under class '#{klass.name}' on line #{rel_node.lineno} (first definition on line #{context.relations[iter.name][rel_node.name.text][0].lineno}"
        end
        iter = iter.parent
      end
      rel = ADSL::DS::DSRelation.new :name => rel_node.name.text, :from_class => klass
      context.relations[klass.name][rel.name] = [rel_node, rel]
    end
  end

  # now that classes and rels are initialized, check them
  @classes.each do |class_node|
    class_node.typecheck_and_resolve context
  end

  @actions.each do |action_node|
    action_node.typecheck_and_resolve context
  end

  # make sure invariants have unique names; add names to unnamed invariants
  names = Set.new
  @invariants.each do |invariant_node|
    invariant = invariant_node.typecheck_and_resolve context
    if invariant.name && names.include?(invariant.name)
      raise ADSLError, "Duplicate invariant name #{invariant.name} on line #{invariant_node.lineno}"
    end
    name = invariant.name || "unnamed_line_#{invariant_node.lineno}"
    while names.include? name
      name = name.increment_suffix
    end
    invariant.name = name
    context.invariants << invariant
    names << name
  end

  @invariants.each do |invariant_node|
    invariant = invariant_node.typecheck_and_resolve context
  end

  ADSL::DS::DSSpec.new(
    :classes => context.classes.map{ |a, b| b[1] }, 
    :actions => context.actions.map{ |a, b| b[1] },
    :invariants => context.invariants.dup
  )
end