Class: Udb::Z3Solver

Inherits:

Object

• Object
• Udb::Z3Solver

Extended by:

Forwardable, T::Sig

Defined in:

lib/udb/z3.rb

Overview

Main Z3 solver wrapper for RISC-V architecture validation

This class provides a high-level interface to Z3 for validating RISC-V configurations. It manages:

• Parameter terms with JSON schema constraints
• Extension version terms
• Extension requirement terms
• Stack-based solver contexts (push/pop)

The solver maintains caches of terms organized in stacks, allowing incremental solving with backtracking via push/pop operations.

Instance Attribute Summary

• #solver ⇒ Object readonly

  Returns the value of attribute solver.

Class Method Summary

• .configure_parallelization(desired) ⇒ Object
• .parallel_enabled ⇒ Object
• .parallel_enabled=(value) ⇒ Object

Instance Method Summary

• #ext_major(name) ⇒ Object
• #ext_minor(name) ⇒ Object
• #ext_patch(name) ⇒ Object
• #ext_pre(name) ⇒ Object
• #ext_req(name, req, cfg_arch) ⇒ Object
• #ext_ver(name, version, cfg_arch) ⇒ Object
• #initialize ⇒ Z3Solver constructor

  A new instance of Z3Solver.

• #param(name, schema_hsh) ⇒ Object
• #pop ⇒ Object
• #push ⇒ Object
• #xlen ⇒ Object

Constructor Details

#initialize ⇒ Z3Solver

Returns a new instance of Z3Solver.

# File 'lib/udb/z3.rb', line 1140

def initialize
  if Udb.global_options.parallel_z3
    Z3Solver.configure_parallelization(true)
  else
    Z3Solver.configure_parallelization(false)
  end

  @solver = T.let(Z3::Solver.new, Z3::Solver)

  # Stacks for incremental solving with push/pop
  @ext_vers = T.let([{}], T::Array[T::Hash[Integer, Z3ExtensionVersion]])
  @ext_reqs = T.let([{}], T::Array[T::Hash[Integer, Z3ExtensionRequirement]])
  @param_terms = T.let([{}], T::Array[T::Hash[String, Z3ParameterTerm]])

  # Extension version component terms (shared across versions of same extension)
  @ext_majors = T.let([{}], T::Array[T::Hash[String, Z3::IntExpr]])
  @ext_minors = T.let([{}], T::Array[T::Hash[String, Z3::IntExpr]])
  @ext_patches = T.let([{}], T::Array[T::Hash[String, Z3::IntExpr]])
  @ext_pres = T.let([{}], T::Array[T::Hash[String, Z3::BoolExpr]])

  @xlen = T.let(nil, T.nilable(Z3::IntExpr))
end

Instance Attribute Details

#solver ⇒ Object (readonly)

Returns the value of attribute solver.

# File 'lib/udb/z3.rb', line 1105

def solver
  @solver
end

Class Method Details

.configure_parallelization(desired) ⇒ Object

# File 'lib/udb/z3.rb', line 1123

def configure_parallelization(desired)
  previous = parallel_enabled

  if !previous.nil? && previous != desired
    if desired
      Udb.logger.warn "Z3 parallelization was previously disabled, but is now being enabled"
    else
      Udb.logger.warn "Z3 parallelization was previously enabled, but is now being disabled"
    end
  end

  Z3.set_param("parallel.enable", desired ? "true" : "false")
  self.parallel_enabled = desired
end

.parallel_enabled ⇒ Object

# File 'lib/udb/z3.rb', line 1113

def parallel_enabled
  @parallel_enabled
end

.parallel_enabled=(value) ⇒ Object

# File 'lib/udb/z3.rb', line 1118

def parallel_enabled=(value)
  @parallel_enabled = value
end

Instance Method Details

#ext_major(name) ⇒ Object

# File 'lib/udb/z3.rb', line 1250

def ext_major(name)
  @ext_majors.reverse_each do |h|
    if h.key?(name)
      return h.fetch(name)
    end
  end
  T.must(@ext_majors.last)[name] ||= Z3.Int("#{name}_major")
end

#ext_minor(name) ⇒ Object

# File 'lib/udb/z3.rb', line 1260

def ext_minor(name)
  @ext_minors.reverse_each do |h|
    if h.key?(name)
      return h.fetch(name)
    end
  end
  T.must(@ext_minors.last)[name] ||= Z3.Int("#{name}_minor")
end

#ext_patch(name) ⇒ Object

# File 'lib/udb/z3.rb', line 1270

def ext_patch(name)
  @ext_patches.reverse_each do |h|
    if h.key?(name)
      return h.fetch(name)
    end
  end
  T.must(@ext_patches.last)[name] ||= Z3.Int("#{name}_patch")
end

#ext_pre(name) ⇒ Object

# File 'lib/udb/z3.rb', line 1280

def ext_pre(name)
  @ext_pres.reverse_each do |h|
    if h.key?(name)
      return h.fetch(name)
    end
  end
  T.must(@ext_pres.last)[name] ||= Z3.Bool("#{name}_pre")
end

#ext_req(name, req, cfg_arch) ⇒ Object

# File 'lib/udb/z3.rb', line 1236

def ext_req(name, req, cfg_arch)
  key = [name, req].hash
  @ext_reqs.reverse_each do |h|
    if h.key?(key)
      return h.fetch(key)
    end
  end
  T.must(@ext_reqs.last)[key] ||= Z3ExtensionRequirement.new(name, req, self, cfg_arch)
end

#ext_ver(name, version, cfg_arch) ⇒ Object

# File 'lib/udb/z3.rb', line 1217

def ext_ver(name, version, cfg_arch)
  version_spec = version.is_a?(VersionSpec) ? version : VersionSpec.new(version)
  key = [name, version_spec].hash
  # Search from most recent context backwards
  @ext_vers.reverse_each do |h|
    if h.key?(key)
      return h.fetch(key)
    end
  end
  # Create new term in current context
  ev = Z3ExtensionVersion.new(name, version_spec, self, cfg_arch)
  T.must(@ext_vers.last)[key] = ev
  ev
end

#param(name, schema_hsh) ⇒ Object

# File 'lib/udb/z3.rb', line 1295

def param(name, schema_hsh)
  @param_terms.reverse_each do |h|
    if h.key?(name)
      return h.fetch(name)
    end
  end
  T.must(@param_terms.last)[name] = Z3ParameterTerm.new(name, self, schema_hsh)
end

#pop ⇒ Object

# File 'lib/udb/z3.rb', line 1168

def pop
  if @ext_vers.size == 1
    Udb.logger.error "Popping solver at base level"
    raise
  end
  @ext_vers.pop
  @ext_reqs.pop
  @param_terms.pop
  @ext_majors.pop
  @ext_minors.pop
  @ext_patches.pop
  @ext_pres.pop
  @solver.pop
end

#push ⇒ Object

# File 'lib/udb/z3.rb', line 1188

def push
  @ext_vers.push({})
  @ext_reqs.push({})
  @param_terms.push({})
  @ext_majors.push({})
  @ext_minors.push({})
  @ext_patches.push({})
  @ext_pres.push({})
  @solver.push
end

#xlen ⇒ Object

# File 'lib/udb/z3.rb', line 1204

def xlen
  unless @xlen
    @xlen = Z3.Int("xlen")
    @solver.assert_as((@xlen == 32) | (@xlen == 64), "_pxlen")
  end
  @xlen
end