Class: Udb::Z3ParameterTerm

Inherits:
Object
  • Object
show all
Extended by:
T::Sig
Defined in:
lib/udb/z3.rb

Overview

Represents a RISC-V parameter as a Z3 term with JSON schema constraints

This class bridges JSON schemas and Z3 solver terms. When constructed, it:

  1. Detects the parameter type from the JSON schema
  2. Creates an appropriate Z3 variable (Bool, Int, Bitvec, or FiniteArray)
  3. Applies all schema constraints as Z3 assertions

There is only one Z3ParameterTerm per parameter name in a solver context. The term is created lazily and cached by the Z3Solver.

Supported JSON schema features:

  • Type constraints (boolean, integer, string, array)
  • Value constraints (const, enum, minimum, maximum)
  • Composition (allOf; anyOf for boolean, integer, and string)
  • References ($ref to uint32/uint64)
  • Array constraints (items, minItems, maxItems, contains, uniqueItems)

Not yet supported (TODO):

  • anyOf for array
  • oneOf, noneOf
  • if/then/else (conditional schemas)

Instance Attribute Summary collapse

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(name, solver, schema_hsh) ⇒ Z3ParameterTerm

Returns a new instance of Z3ParameterTerm.



790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
 
# File 'lib/udb/z3.rb', line 790

def initialize(name, solver, schema_hsh)
  @name = name
  @solver = solver
  @type = T.let(Z3ParameterTerm.detect_type(schema_hsh), Symbol)

  @term = T.let(
    case @type
    when :int
      # Use 64-bit bitvector (width doesn't affect constraint solving, just makes it large enough)
      t = Z3.Bitvec(name, 64)
      Z3ParameterTerm.constrain_int(@solver, t, schema_hsh, name:)
      t
    when :boolean
      t = Z3.Bool(name)
      Z3ParameterTerm.constrain_bool(@solver, t, schema_hsh, name:)
      t
    when :string
      # Represent strings as integer hashes
      t = Z3.Int(name)
      Z3ParameterTerm.constrain_string(@solver, t, schema_hsh, name:)
      t
    when :array
      # Detect element type and create finite array
      subtype = Z3ParameterTerm.detect_array_subtype(schema_hsh)

      case subtype
      when :int
        constraints = Z3ParameterTerm.constrain_array(@solver, schema_hsh, Z3ParameterTerm.method(:constrain_int))
        Z3FiniteArray.new(@solver, name, Z3::BitvecSort, constraints, bitvec_width: 64)
      when :boolean
        constraints = Z3ParameterTerm.constrain_array(@solver, schema_hsh, Z3ParameterTerm.method(:constrain_bool))
        Z3FiniteArray.new(@solver, name, Z3::BoolSort, constraints)
      when :string
        constraints = Z3ParameterTerm.constrain_array(@solver, schema_hsh, Z3ParameterTerm.method(:constrain_string))
        Z3FiniteArray.new(@solver, name, Z3::IntSort, constraints)
      else
        raise "TODO: Unsupported array element type"
      end
    end,
    T.any(Z3::BoolExpr, Z3::IntExpr, Z3::BitvecExpr, Z3FiniteArray)
  )
end

Instance Attribute Details

#name ⇒ Object (readonly)

Returns the value of attribute name.



333
334
335
 
# File 'lib/udb/z3.rb', line 333

def name
  @name
end

#term ⇒ Object (readonly)

Returns the value of attribute term.



336
337
338
 
# File 'lib/udb/z3.rb', line 336

def term
  @term
end

Class Method Details

.constrain_array(solver, schema_hsh, subtype_constrain) ⇒ Object 



594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
 
# File 'lib/udb/z3.rb', line 594

def self.constrain_array(solver, schema_hsh, subtype_constrain)
  constraints = ArrayConstraints.new
  if schema_hsh.key?("items")
    if schema_hsh.fetch("items").is_a?(Array)
      # Tuple-style array: different schema for each position
      schema_hsh.fetch("items").each_with_index do |item_schema, idx|
        constraints.item_by_idx[idx] = TypeConstraint.new(mthd: subtype_constrain, schema: item_schema)
      end
    elsif schema_hsh.fetch("items").is_a?(Hash)
      # Uniform array: same schema for all positions
      # Store for lazy constraint application
      constraints.item_rest = TypeConstraint.new(mthd: subtype_constrain, schema: schema_hsh.fetch("items"))
    else
      raise "unexpected"
    end
  end

  if schema_hsh.key?("additionalItems") && schema_hsh.fetch("additionalItems") != false
    # Schema for positions beyond those specified in tuple-style items
    constraints.item_rest = TypeConstraint.new(mthd: subtype_constrain, schema: schema_hsh.fetch("additionalItems"))
  end

  if schema_hsh.key?("contains")
    # At least one element must match this schema
    constraints.contains = TypeConstraint.new(mthd: subtype_constrain, schema: schema_hsh.fetch("contains"))
  end

  if schema_hsh.key?("unique")
    constraints.unique = true
  end

  if schema_hsh.key?("maxItems")
    constraints.max_size = schema_hsh.fetch("maxItems")
  end

  if schema_hsh.key?("minItems")
    constraints.min_size = schema_hsh.fetch("minItems")
  end

  if schema_hsh.key?("anyOf")
    raise "TODO: anyOf not yet implemented for array constraints"
  end

  if schema_hsh.key?("oneOf")
    raise "TODO: oneOf not yet implemented for array constraints"
  end

  if schema_hsh.key?("noneOf")
    raise "TODO: noneOf not yet implemented for array constraints"
  end

  if schema_hsh.key?("if")
    raise "TODO: if/then/else not yet implemented for array constraints"
  end
  constraints
end

.constrain_bool(solver, term, schema_hsh, name: nil, assert: true) ⇒ Object 



459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
 
# File 'lib/udb/z3.rb', line 459

def self.constrain_bool(solver, term, schema_hsh, name: nil, assert: true)
  assertions = T.let([], T::Array[Z3::BoolExpr])
  if schema_hsh.key?("const")
    assertions << (term == schema_hsh.fetch("const"))
  end

  if schema_hsh.key?("allOf")
    schema_hsh.fetch("allOf").each do |h|
      assertions += constrain_bool(solver, term, h, assert: false)
    end
  end

  if schema_hsh.key?("anyOf")
    branches = schema_hsh.fetch("anyOf").map do |h|
      constrain_bool(solver, term, h, assert: false)
    end
    assertions << any_of_constraint(branches)
  end

  if schema_hsh.key?("oneOf")
    raise "TODO: oneOf not yet implemented for boolean constraints"
  end

  if schema_hsh.key?("noneOf")
    raise "TODO: noneOf not yet implemented for boolean constraints"
  end

  if schema_hsh.key?("if")
    raise "TODO: if/then/else not yet implemented for boolean constraints"
  end

  if assert
    assertions.each { |a| solver.assert a }
  end
  assertions
end

.constrain_int(solver, term, schema_hsh, name: nil, assert: true) ⇒ Object 



364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
 
# File 'lib/udb/z3.rb', line 364

def self.constrain_int(solver, term, schema_hsh, name: nil, assert: true)
  assertions = T.let([], T::Array[Z3::BoolExpr])
  if schema_hsh.key?("const")
    assertions << (term == schema_hsh.fetch("const"))
  end

  if schema_hsh.key?("enum")
    # Build disjunction: term equals one of the enum values
    expr = (term == schema_hsh.fetch("enum")[0])
    schema_hsh.fetch("enum")[1..].each do |v|
      expr = expr | (term == v)
    end
    assertions << expr
  end

  if schema_hsh.key?("minimum")
    # Use unsigned comparison for RISC-V parameter values
    assertions << term.unsigned_ge(schema_hsh.fetch("minimum"))
  end

  if schema_hsh.key?("maximum")
    assertions << term.unsigned_le(schema_hsh.fetch("maximum"))
  end

  if schema_hsh.key?("allOf")
    schema_hsh.fetch("allOf").each do |h|
      assertions += constrain_int(solver, term, h, assert: false)
    end
  end

  if schema_hsh.key?("anyOf")
    branches = schema_hsh.fetch("anyOf").map do |h|
      constrain_int(solver, term, h, assert: false)
    end
    assertions << any_of_constraint(branches)
  end

  if schema_hsh.key?("oneOf")
    raise "TODO: oneOf not yet implemented for integer constraints"
  end

  if schema_hsh.key?("noneOf")
    raise "TODO: noneOf not yet implemented for integer constraints"
  end

  if schema_hsh.key?("if")
    raise "TODO: if/then/else not yet implemented for integer constraints"
  end

  if schema_hsh.key?("$ref")
    # Handle references to shorthand type definitions
    if schema_hsh.fetch("$ref").split("/").last == "uint32"
      assertions << ((term.unsigned_ge(0)) & (term.unsigned_le(2**32 - 1)))
    elsif schema_hsh.fetch("$ref").split("/").last == "uint64"
      assertions << ((term.unsigned_ge(0)) & (term.unsigned_le(2**64 - 1)))
    elsif schema_hsh.fetch("$ref").split("/").last == "32bit_unsigned_pow2"
      assertions << ((term == 0) | (0 == (term & (term - 1))))
      assertions << ((term.unsigned_gt(0)) & (term.unsigned_le(2**32 - 1)))
    elsif schema_hsh.fetch("$ref").split("/").last == "64bit_unsigned_pow2"
      assertions << ((term == 0) | (0 == (term & (term - 1))))
      assertions << ((term.unsigned_gt(0)) & (term.unsigned_le(2**64 - 1)))
    else
      raise "Unhandled schema $ref: #{schema_hsh.fetch("$ref")}"
    end
  end

  if assert
    assertions.each { |a| solver.assert a }
  end
  assertions
end

.constrain_string(solver, term, schema_hsh, name: nil, assert: true) ⇒ Object 



522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
 
# File 'lib/udb/z3.rb', line 522

def self.constrain_string(solver, term, schema_hsh, name: nil, assert: true)
  assertions = T.let([], T::Array[Z3::BoolExpr])
  if schema_hsh.key?("const")
    # Compare string hashes since Z3 doesn't have native string support
    assertions << (term == schema_hsh.fetch("const").hash)
  end

  if schema_hsh.key?("enum")
    # Build disjunction of string hash comparisons
    expr = (term == schema_hsh.fetch("enum")[0].hash)
    schema_hsh.fetch("enum")[1..].each do |v|
      expr = expr | (term == v.hash)
    end
    assertions << expr
  end

  if schema_hsh.key?("anyOf")
    branches = schema_hsh.fetch("anyOf").map do |h|
      constrain_string(solver, term, h, assert: false)
    end
    assertions << any_of_constraint(branches)
  end

  if schema_hsh.key?("oneOf")
    raise "TODO: oneOf not yet implemented for string constraints"
  end

  if schema_hsh.key?("noneOf")
    raise "TODO: noneOf not yet implemented for string constraints"
  end

  if schema_hsh.key?("if")
    raise "TODO: if/then/else not yet implemented for string constraints"
  end

  if assert
    assertions.each { |a| solver.assert a }
  end
  assertions
end

.detect_array_subtype(schema_hsh) ⇒ Object 



767
768
769
770
771
772
773
774
775
776
777
 
# File 'lib/udb/z3.rb', line 767

def self.detect_array_subtype(schema_hsh)
  if schema_hsh.key?("items") && schema_hsh.fetch("items").is_a?(Array)
    # Tuple-style: use first element's type
    detect_type(schema_hsh.fetch("items")[0])
  elsif schema_hsh.key?("items")
    # Uniform: use the single schema's type
    detect_type(schema_hsh.fetch("items"))
  else
    raise "Can't detect array subtype"
  end
end

.detect_type(schema_hsh) ⇒ Object 



664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
 
# File 'lib/udb/z3.rb', line 664

def self.detect_type(schema_hsh)
  if schema_hsh.key?("type")
    case schema_hsh["type"]
    when "boolean"
      :boolean
    when "integer"
      :int
    when "string"
      :string
    when "array"
      :array
    else
      raise "Unhandled JSON schema type"
    end
  elsif schema_hsh.key?("minimum") || schema_hsh.key?("maximum")
    :int
  elsif schema_hsh.key?("const")
    # Infer type from const value
    case schema_hsh["const"]
    when TrueClass, FalseClass
      :boolean
    when Integer
      :int
    when String
      :string
    else
      raise "Unhandled const type"
    end
  elsif schema_hsh.key?("enum")
    # Infer type from enum values (must be homogeneous)
    raise "Mixed types in enum" unless schema_hsh["enum"].all? { |e| e.class == schema_hsh["enum"].fetch(0).class }

    case schema_hsh["enum"].fetch(0)
    when TrueClass, FalseClass
      :boolean
    when Integer
      :int
    when String
      :string
    else
      raise "unhandled enum type"
    end
  elsif schema_hsh.key?("allOf")
    # Infer type from subschemas (must agree)
    subschema_types = schema_hsh.fetch("allOf").map { |subschema| detect_type(subschema) }

    if subschema_types.fetch(0) == :string
      raise "Subschema types do not agree" unless subschema_types[1..].all? { |t| t == :string }

      :string
    elsif subschema_types.fetch(0) == :boolean
      raise "Subschema types do not agree" unless subschema_types[1..].all? { |t| t == :boolean }

      :boolean
    elsif subschema_types.fetch(0) == :int
      raise "Subschema types do not agree" unless subschema_types[1..].all? { |t| t == :int }

      :int
    else
      raise "unhandled subschema type"
    end
  elsif schema_hsh.key?("anyOf")
    # Infer type from anyOf subschemas (must agree on type even if values differ)
    subschema_types = schema_hsh.fetch("anyOf").map { |subschema| detect_type(subschema) }

    if subschema_types.fetch(0) == :string
      raise "Subschema types do not agree" unless subschema_types[1..].all? { |t| t == :string }

      :string
    elsif subschema_types.fetch(0) == :boolean
      raise "Subschema types do not agree" unless subschema_types[1..].all? { |t| t == :boolean }

      :boolean
    elsif subschema_types.fetch(0) == :int
      raise "Subschema types do not agree" unless subschema_types[1..].all? { |t| t == :int }

      :int
    else
      raise "unhandled subschema type"
    end
  elsif schema_hsh.key?("$ref")
    case schema_hsh.fetch("$ref").split("/").last
    when "uint32", "uint64", "32bit_unsigned_pow2", "64bit_unsigned_pow2"
      :int
    else
      raise "unhandled ref: #{schema_hsh.fetch("$ref")}"
    end
  elsif schema_hsh.key?("not")
    # Type is same as negated schema
    detect_type(schema_hsh.fetch("not"))
  else
    raise "unhandled scalar schema:\n#{schema_hsh}"
  end
end

Instance Method Details

#!=(val) ⇒ Object 



874
875
876
877
878
879
880
881
882
883
 
# File 'lib/udb/z3.rb', line 874

def !=(val)
  case val
  when String
    T.cast(@term, Z3::IntExpr) != val.hash
  when Array
    T.cast(@term, Z3FiniteArray) != val
  else
    T.cast(@term, Z3::Expr) != val
  end
end

#<(val) ⇒ Object 



891
892
893
 
# File 'lib/udb/z3.rb', line 891

def <(val)
  T.cast(@term, Z3::BitvecExpr).unsigned_lt(val)
end

#<=(val) ⇒ Object 



886
887
888
 
# File 'lib/udb/z3.rb', line 886

def <=(val)
  T.cast(@term, Z3::BitvecExpr).unsigned_le(val)
end

#==(val) ⇒ Object 



861
862
863
864
865
866
867
868
869
870
871
 
# File 'lib/udb/z3.rb', line 861

def ==(val)
  case val
  when String
    # Compare string hashes
    T.cast(@term, Z3::IntExpr) == val.hash
  when Array
    T.cast(@term, Z3FiniteArray) == val
  else
    T.cast(@term, Z3::Expr) == val
  end
end

#>(val) ⇒ Object 



901
902
903
 
# File 'lib/udb/z3.rb', line 901

def >(val)
  T.cast(@term, Z3::BitvecExpr).unsigned_gt(val)
end

#>=(val) ⇒ Object 



896
897
898
 
# File 'lib/udb/z3.rb', line 896

def >=(val)
  T.cast(@term, Z3::BitvecExpr).unsigned_ge(val)
end

#[](idx) ⇒ Object 



845
846
847
848
849
850
 
# File 'lib/udb/z3.rb', line 845

def [](idx)
  unless @term.is_a?(Z3FiniteArray)
    raise "#{@name} is not an array parameter"
  end
  @term[idx]
end

#extract(msb, lsb) ⇒ Object 



840
841
842
 
# File 'lib/udb/z3.rb', line 840

def extract(msb, lsb)
  T.cast(@term, Z3::BitvecExpr).extract(msb, lsb)
end

#has_value?(val) ⇒ Boolean

Returns:

  • (Boolean) 


853
854
855
856
857
858
 
# File 'lib/udb/z3.rb', line 853

def has_value?(val)
  unless @term.is_a?(Z3FiniteArray)
    raise "#{@name} is not an array parameter"
  end
  @term.has_value?(val)
end

#size_term ⇒ Object 



834
835
836
837
 
# File 'lib/udb/z3.rb', line 834

def size_term
  raise "Not an array parameter" unless @term.is_a?(Z3FiniteArray)
  @term.size_term
end