Class: Udb::Z3Solver

Inherits:
Object
  • Object
show all
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.

Defined Under Namespace

Classes: self

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize 



1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
 
# 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 ⇒ Z3::Solver (readonly)

Returns:



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

def solver
  @solver
end

Class Method Details

.configure_parallelization(desired)

This method returns an undefined value.

Parameters:

  • desired (Boolean) 


1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
 
# 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 ⇒ Boolean?

Returns:

  • (Boolean, nil) 


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

def parallel_enabled
  @parallel_enabled
end

.parallel_enabled=(value)

This method returns an undefined value.

Parameters:

  • value (Boolean, nil) 


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

def parallel_enabled=(value)
  @parallel_enabled = value
end

Instance Method Details

#ext_major(name) ⇒ Z3::IntExpr

Get or create the major version term for an extension

All versions of the same extension share these component terms.

Parameters:

  • name (String)

Returns:

  • (Z3::IntExpr) 


1250
1251
1252
1253
1254
1255
1256
1257
 
# 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) ⇒ Z3::IntExpr

Parameters:

  • name (String)

Returns:

  • (Z3::IntExpr) 


1260
1261
1262
1263
1264
1265
1266
1267
 
# 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) ⇒ Z3::IntExpr

Parameters:

  • name (String)

Returns:

  • (Z3::IntExpr) 


1270
1271
1272
1273
1274
1275
1276
1277
 
# 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) ⇒ Z3::BoolExpr

Parameters:

  • name (String)

Returns:

  • (Z3::BoolExpr) 


1280
1281
1282
1283
1284
1285
1286
1287
 
# 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) ⇒ Z3ExtensionRequirement

Get or create an extension requirement term

Returns a cached term if it exists, otherwise creates a new one.

Parameters:

Returns:



1236
1237
1238
1239
1240
1241
1242
1243
1244
 
# 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) ⇒ Z3ExtensionVersion

Get or create an extension version term

Returns a cached term if it exists, otherwise creates a new one. The term is stored in the current context level.

Parameters:

Returns:



1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
 
# 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) ⇒ Z3ParameterTerm

Get or create a parameter term with JSON schema constraints

Returns a cached term if it exists, otherwise creates a new one with all schema constraints applied.

Parameters:

  • name (String)
  • schema_hsh (Hash{String => T.untyped})

Returns:



1295
1296
1297
1298
1299
1300
1301
1302
 
# 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

This method returns an undefined value.

Pop a solver context level

Removes the most recent push level, discarding all terms and assertions added since that push. Raises an error if already at the base level.



1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
 
# 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

This method returns an undefined value.

Push a new solver context level

Creates a new scope for terms and assertions. All changes can be undone with a corresponding pop operation.



1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
 
# 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 ⇒ Z3::IntExpr

Get or create the XLEN term

XLEN represents the base integer register width (32 or 64 bits). This term is constrained to be either 32 or 64.

Returns:

  • (Z3::IntExpr) 


1204
1205
1206
1207
1208
1209
1210
 
# 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