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)

  • References ($ref to uint32/uint64)

  • Array constraints (items, minItems, maxItems, contains, uniqueItems)

Not yet supported (TODO):

  • anyOf, oneOf, noneOf (would require disjunctive constraints)

  • 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.



768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
 
# File 'lib/udb/z3.rb', line 768

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.



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

def name
  @name
end

#term ⇒ Object (readonly)

Returns the value of attribute term.



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

def term
  @term
end

Class Method Details

.constrain_array(solver, schema_hsh, subtype_constrain) ⇒ Object 



572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
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
 
# File 'lib/udb/z3.rb', line 572

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 



453
454
455
456
457
458
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
 
# File 'lib/udb/z3.rb', line 453

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)
    end
  end

  if schema_hsh.key?("anyOf")
    raise "TODO: anyOf not yet implemented for boolean constraints"
  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 



362
363
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
 
# File 'lib/udb/z3.rb', line 362

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)
    end
  end

  if schema_hsh.key?("anyOf")
    raise "TODO: anyOf not yet implemented for integer constraints"
  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 



512
513
514
515
516
517
518
519
520
521
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
 
# File 'lib/udb/z3.rb', line 512

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")
    raise "TODO: anyOf not yet implemented for string constraints"
  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 



745
746
747
748
749
750
751
752
753
754
755
 
# File 'lib/udb/z3.rb', line 745

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 



642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
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
 
# File 'lib/udb/z3.rb', line 642

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 



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

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 



869
870
871
 
# File 'lib/udb/z3.rb', line 869

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

#<=(val) ⇒ Object 



864
865
866
 
# File 'lib/udb/z3.rb', line 864

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

#==(val) ⇒ Object 



839
840
841
842
843
844
845
846
847
848
849
 
# File 'lib/udb/z3.rb', line 839

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 



879
880
881
 
# File 'lib/udb/z3.rb', line 879

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

#>=(val) ⇒ Object 



874
875
876
 
# File 'lib/udb/z3.rb', line 874

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

#[](idx) ⇒ Object 



823
824
825
826
827
828
 
# File 'lib/udb/z3.rb', line 823

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

#extract(msb, lsb) ⇒ Object 



818
819
820
 
# File 'lib/udb/z3.rb', line 818

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

#has_value?(val) ⇒ Boolean

Returns:

  • (Boolean) 


831
832
833
834
835
836
 
# File 'lib/udb/z3.rb', line 831

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 



812
813
814
815
 
# File 'lib/udb/z3.rb', line 812

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