Class: Udb::Condition

Inherits:
AbstractCondition show all
Extended by:
T::Helpers, T::Sig
Defined in:
lib/udb/condition.rb,
lib/udb/condition.rb

Overview

represents a condition in the UDB data, which could include conditions involving extensions and/or parameters

Defined Under Namespace

Classes: MemoizedState

Constant Summary collapse

EvalCallbackType = 
T.type_alias { T.proc.params(term: TermType).returns(SatisfiedResult) }
Xlen32 = 
XlenCondition.new(32)
Xlen64 = 
XlenCondition.new(64)

Class Method Summary collapse

Instance Method Summary collapse

Constructor Details

#initialize(yaml, cfg_arch, input_file: nil, input_line: nil)

Parameters:

  • yaml (Hash{String => T.untyped}, Boolean)
  • cfg_arch (ConfiguredArchitecture)
  • input_file (Pathname, nil) (defaults to: nil)
  • input_line (Integer, nil) (defaults to: nil) 


425
426
427
428
429
430
431
 
# File 'lib/udb/condition.rb', line 425

def initialize(yaml, cfg_arch, input_file: nil, input_line: nil)
  @yaml = yaml
  @cfg_arch = cfg_arch
  @input_file = input_file
  @input_line = input_line
  @memo = MemoizedState.new(satisfied_by_cfg_arch: {})
end

Class Method Details

.conjunction(conditions, cfg_arch) ⇒ AbstractCondition

return a new Condition that the logical AND of conditions

Parameters:

Returns:



1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
 
# File 'lib/udb/condition.rb', line 1259

def self.conjunction(conditions, cfg_arch)
  if conditions.empty?
    AlwaysFalseCondition.new(cfg_arch)
  elsif conditions.size == 1
    conditions.fetch(0)
  else
    Condition.new(
      LogicNode.new(
        LogicNodeType::And,
        conditions.map { |c| c.to_logic_tree_internal }
      ).to_h,
      cfg_arch
    )
  end
end

.disjunction(conditions, cfg_arch) ⇒ AbstractCondition

return a new Condition that the logical OR of conditions

Parameters:

Returns:



1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
 
# File 'lib/udb/condition.rb', line 1283

def self.disjunction(conditions, cfg_arch)
  if conditions.empty?
    AlwaysFalseCondition.new(cfg_arch)
  elsif conditions.size == 1
    conditions.fetch(0)
  else
    Condition.new(
      LogicNode.new(
        LogicNodeType::Or,
        conditions.map { |c| c.to_logic_tree_internal }
      ).to_h,
      cfg_arch
    )
  end
end

.join(cfg_arch, conds) ⇒ AbstractCondition

Parameters:

Returns:



402
403
404
405
406
407
408
409
410
 
# File 'lib/udb/condition.rb', line 402

def self.join(cfg_arch, conds)
  if conds.size == 0
    (AlwaysTrueCondition.new(cfg_arch))
  elsif conds.size == 1
    conds.fetch(0)
  else
    Condition.new({ "allOf" => conds.map(&:to_h) }, cfg_arch)
  end
end

.not(condition, cfg_arch) ⇒ AbstractCondition

Parameters:

Returns:



1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
 
# File 'lib/udb/condition.rb', line 1330

def self.not(condition, cfg_arch)
  if condition.is_a?(AlwaysFalseCondition)
    AlwaysTrueCondition.new(cfg_arch)
  elsif condition.is_a?(AlwaysTrueCondition)
    AlwaysFalseCondition.new(cfg_arch)
  else
    Condition.new(
      LogicNode.new(
        LogicNodeType::Not,
        [condition.to_logic_tree_internal]
      ).to_h,
      cfg_arch
    )
  end
end

.one_of(conditions, cfg_arch) ⇒ AbstractCondition

return a new Condition that the logical XOR of conditions

Parameters:

Returns:



1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
 
# File 'lib/udb/condition.rb', line 1307

def self.one_of(conditions, cfg_arch)
  if conditions.empty?
    AlwaysFalseCondition.new(cfg_arch)
  elsif conditions.size == 1
    conditions.fetch(0)
  else
    Condition.new(
      LogicNode.new(
        LogicNodeType::Xor,
        conditions.map { |c| c.to_logic_tree_internal }
      ).to_h,
      cfg_arch
    )
  end
end

.solver ⇒ Object 



696
697
698
 
# File 'lib/udb/condition.rb', line 696

def self.solver
  @solver ||= Z3Solver.new
end

Instance Method Details

#&(other) ⇒ AbstractCondition

Parameters:

Returns:



1348
1349
1350
 
# File 'lib/udb/condition.rb', line 1348

def &(other)
  Condition.conjunction([self, other], @cfg_arch)
end

#-@ ⇒ AbstractCondition

Returns:



1358
1359
1360
 
# File 'lib/udb/condition.rb', line 1358

def -@
  Condition.not(self, @cfg_arch)
end

#empty? ⇒ Boolean

Returns:

  • (Boolean) 


434
 
# File 'lib/udb/condition.rb', line 434

def empty? = @yaml == true || @yaml == false || @yaml.empty?

#expand_term_requirements(tree, expansion_clauses = [], touched_terms = T.let(Set.new, T::Set[TermType])) ⇒ Array<LogicNode>

Parameters:

  • tree (LogicNode)
  • expansion_clauses (Array<LogicNode>) (defaults to: [])
  • touched_terms (Set<TermType>) (defaults to: T.let(Set.new, T::Set[TermType]))

Returns:



627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
 
# File 'lib/udb/condition.rb', line 627

def expand_term_requirements(tree, expansion_clauses = [], touched_terms = T.let(Set.new, T::Set[TermType]))
  terms = tree.terms

  terms.each do |term|
    case term
    when ExtensionTerm
      expand_extension_term_requirements(term, expansion_clauses, touched_terms)
    when ParameterTerm
      expand_parameter_term_requirements(term, expansion_clauses, touched_terms)
    else
      #pass
    end
  end

  expansion_clauses
end

#expand_to_enforce_single_ext_ver(tree, expansion_clauses)

This method returns an undefined value.

Parameters:



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
 
# File 'lib/udb/condition.rb', line 526

def expand_to_enforce_single_ext_ver(tree, expansion_clauses)
  # for every mentioned extension, enforce that either zero or one version is ever implemented
  mentioned_ext_terms = (tree.terms.grep(ExtensionTerm) + expansion_clauses.map { |c| c.terms.grep(ExtensionTerm) }.flatten).uniq

  grouped_ext_terms = mentioned_ext_terms.group_by(&:name)

  grouped_ext_terms.each do |ext_name, ext_terms|
    # assuming this comes after expand_extension_version_ranges, so we can ignore ranges
    mentioned_versions = ext_terms.select { |e| e.comparison == ExtensionTerm::ComparisonOp::Equal }
    if mentioned_versions.size > 1
      # add NONE(ext_terms) || XOR(ext_terms)
      expansion_clauses <<
        LogicNode.new(
          LogicNodeType::Or,
          [
            LogicNode.new(
              LogicNodeType::None,
              mentioned_versions.map { |t| LogicNode.new(LogicNodeType::Term, [t]) }
            ),
            LogicNode.new(
              LogicNodeType::Xor,
              mentioned_versions.map { |t| LogicNode.new(LogicNodeType::Term, [t]) }
            )
          ]
        )
    end
  end
end

#has_extension_requirement? ⇒ Boolean

Returns:

  • (Boolean) 


805
806
807
 
# File 'lib/udb/condition.rb', line 805

def has_extension_requirement?
  to_logic_tree(expand: true).terms.any? { |t| t.is_a?(ExtensionVersion) }
end

#has_param? ⇒ Boolean

Returns:

  • (Boolean) 


800
801
802
 
# File 'lib/udb/condition.rb', line 800

def has_param?
  to_logic_tree(expand: true).terms.any? { |t| t.is_a?(ParameterTerm) }
end

#implied_extension_conflicts(expand: true) ⇒ Array<ConditionalExtensionRequirement>

Parameters:

  • expand (Boolean) (defaults to: true)

Returns:



1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
 
# File 'lib/udb/condition.rb', line 1166

def implied_extension_conflicts(expand: true)
  # strategy:
  #   1. invert extension requiremnts (to get conflicts)
  #   1. convert to product-of-sums.
  #   2. for each product, find the positive terms. These are the conflicts
  #   3. for each product, find the negative terms. These are the "conditions" when the positive terms apply

  @conflicts ||= begin
    conflicts = T.let([], T::Array[ConditionalExtensionRequirement])
    pos = LogicNode.new(LogicNodeType::Not, [to_logic_tree(expand:)]).minimize(LogicNode::CanonicalizationType::ProductOfSums)
    if pos.type == LogicNodeType::Term
      # there are no negative terms, do nothing
    elsif pos.type == LogicNodeType::Not
      single_term = pos.node_children.fetch(0).children.fetch(0)
      if single_term.is_a?(ExtensionTerm)
        conflicts << \
          ConditionalExtensionRequirement.new(
            ext_req: single_term.to_ext_req(@cfg_arch),
            cond: AlwaysTrueCondition.new(@cfg_arch)
          )
      else
        # parameter, do nothing
      end
    elsif pos.type == LogicNodeType::And
      pos.children.each do |child|
        child = T.cast(child, LogicNode)
        if child.type == LogicNodeType::Term
          # not a negative term; do nothing
        elsif child.type == LogicNodeType::Not
          term = child.node_children.fetch(0).children.fetch(0)
          if term.is_a?(ExtensionTerm)
            conflicts << \
              ConditionalExtensionRequirement.new(
                ext_req: term.to_ext_req(@cfg_arch),
                cond: (AlwaysTrueCondition.new(@cfg_arch))
              )
          else
            puts "Not a term: #{term} #{term.class.name}"
          end
        elsif child.children.all? { |child| T.cast(child, LogicNode).type == LogicNodeType::Term }
          # there is no negative term, so do nothing
        else
          raise "? #{child.type}" unless child.type == LogicNodeType::Or

          negative_terms =
            child.node_children.select do |and_child|
              and_child.type == LogicNodeType::Not && and_child.node_children.fetch(0).children.fetch(0).is_a?(ExtensionTerm)
            end.map { |n| n.node_children.fetch(0) }
          cond_terms =
            child.node_children.select { |and_child| and_child.type == LogicNodeType::Term }
          negative_terms.each do |nterm|
            cond_node =
              if cond_terms.empty?
                LogicNode::True
              else
                cond_terms.size == 1 \
                    ? cond_terms.fetch(0)
                    : LogicNode.new(LogicNodeType::Or, cond_terms)
              end

            conflicts << \
              ConditionalExtensionRequirement.new(
                ext_req: T.cast(nterm.children.fetch(0), ExtensionTerm).to_ext_req(@cfg_arch),
                cond: Condition.new(cond_node.to_h, @cfg_arch)
              )
          end
          conflicts
        end
      end
    end
    conflicts
  end
end

#implied_extension_requirements(expand: true) ⇒ Array<ConditionalExtensionRequirement>

Parameters:

  • expand (Boolean) (defaults to: true)

Returns:



1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
 
# File 'lib/udb/condition.rb', line 1092

def implied_extension_requirements(expand: true)
  # strategy:
  #   1. convert to sum-of-products.
  #   2. for each product, find the positive terms. These are the implications
  #   3. for each product, find the negative terms. These are the "conditions" when the positive terms apply

  @implications ||= begin
    reqs = T.let([], T::Array[ConditionalExtensionRequirement])
    pos = to_logic_tree(expand:).minimize(LogicNode::CanonicalizationType::ProductOfSums)

    if pos.type == LogicNodeType::Term
      single_term = pos.children.fetch(0)
      if single_term.is_a?(ExtensionTerm)
        reqs << ConditionalExtensionRequirement.new(ext_req: single_term.to_ext_req(@cfg_arch), cond: AlwaysTrueCondition.new(@cfg_arch))
      else
        # this is a single parameter, do nothing
      end
    elsif pos.type == LogicNodeType::Not
      # there are no positive terms, do nothing
    elsif pos.type == LogicNodeType::And
      pos.children.each do |child|
        child = T.cast(child, LogicNode)
        if child.type == LogicNodeType::Term
          term = child.children.fetch(0)
          if term.is_a?(ExtensionTerm)
            reqs << \
              ConditionalExtensionRequirement.new(
                ext_req: term.to_ext_req(@cfg_arch),
                cond: AlwaysTrueCondition.new(@cfg_arch)
              )
          end
        elsif child.type == LogicNodeType::Not
          # not a positive term; do nothing
        elsif child.children.all? { |child| T.cast(child, LogicNode).type == LogicNodeType::Not }
          # there is no positive term, so do nothing
        else
          raise "? #{child.type}" unless child.type == LogicNodeType::Or

          positive_terms =
            child.node_children.select do |and_child|
              and_child.type == LogicNodeType::Term && and_child.children.fetch(0).is_a?(ExtensionTerm)
            end
          cond_terms =
            child.node_children.select { |and_child| and_child.type == LogicNodeType::Not }
            .map { |neg_term| neg_term.node_children.fetch(0) }
          cond_terms +=
            child.node_children.select do |and_child|
              and_child.type == LogicNodeType::Term && and_child.children.fetch(0).is_a?(ParameterTerm)
            end.map { |c| LogicNode.new(LogicNodeType::Not, [c]) }
          positive_terms.each do |pterm|
            cond_node =
              if cond_terms.empty?
                LogicNode::True
              else
                cond_terms.size == 1 \
                    ? cond_terms.fetch(0)
                    : LogicNode.new(LogicNodeType::And, cond_terms)
              end

            reqs << \
              ConditionalExtensionRequirement.new(
                ext_req: T.cast(pterm.children.fetch(0), ExtensionTerm).to_ext_req(@cfg_arch),
                cond: Condition.new(cond_node.to_h, @cfg_arch)
              )
          end
          reqs
        end
      end
    end
    reqs
  end
end

#make_cb_proc(&blk) ⇒ EvalCallbackType

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Parameters:

Returns:



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

def make_cb_proc(&blk)
  blk
end

#minimize(expand: true) ⇒ AbstractCondition

Parameters:

  • expand (Boolean) (defaults to: true)

Returns:



737
738
739
 
# File 'lib/udb/condition.rb', line 737

def minimize(expand: true)
  Condition.new(to_logic_tree(expand:).minimize(LogicNode::CanonicalizationType::ProductOfSums).to_h, @cfg_arch)
end

#partial_eval(ext_reqs: [], expand: true) ⇒ AbstractCondition

Parameters:

Returns:



997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
 
# File 'lib/udb/condition.rb', line 997

def partial_eval(ext_reqs: [], expand: true)
  cb = LogicNode.make_replace_cb do |node|
    if node.type == LogicNodeType::Term
      term = node.children.fetch(0)
      if term.is_a?(ExtensionTerm)
        if ext_reqs.any? { |ext_req| term.to_ext_req(@cfg_arch).satisfied_by?(ext_req) }
          next LogicNode::True
        end
      end
    end
    node
  end
  LogicCondition.new(to_logic_tree(expand:).replace_terms(cb), @cfg_arch)
end

#partially_evaluate_for_params(cfg_arch, expand:) ⇒ Condition

return a new condition where any parameter term with a known outcome is replaced with a true/false

Parameters:

Returns:



818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
 
# File 'lib/udb/condition.rb', line 818

def partially_evaluate_for_params(cfg_arch, expand:)
  cb = make_cb_proc do |term|
    if term.is_a?(ExtensionTerm)
      SatisfiedResult::Maybe
    elsif term.is_a?(ParameterTerm)
      term.partial_eval(cfg_arch.config.param_values)
    elsif term.is_a?(FreeTerm)
      raise "unreachable"
    elsif term.is_a?(XlenTerm)
      # can't use cfg_arch.possible_xlens because of an initialization circular dependency in figuring out
      # is S/U is implemented
      if term.xlen == 32
        if cfg_arch.mxlen.nil?
          SatisfiedResult::Maybe
        elsif cfg_arch.mxlen == 32
          SatisfiedResult::Yes
        else
          # mxlen == 64. can some other mode be 32?
          if !cfg_arch.config.param_values.key?("SXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("SXLEN"), T::Array[Integer]).include?(32)
            SatisfiedResult::Yes
          elsif !cfg_arch.config.param_values.key?("UXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("UXLEN"), T::Array[Integer]).include?(32)
            SatisfiedResult::Yes
          elsif !cfg_arch.config.param_values.key?("VSXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("VSXLEN"), T::Array[Integer]).include?(32)
            SatisfiedResult::Yes
          elsif !cfg_arch.config.param_values.key?("VUXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("VUXLEN"), T::Array[Integer]).include?(32)
            SatisfiedResult::Yes
          else
            SatisfiedResult::No
          end
        end
      elsif term.xlen == 64
        if cfg_arch.mxlen.nil?
          SatisfiedResult::Maybe
        elsif cfg_arch.mxlen == 32
          SatisfiedResult::No
        else
          # mxlen == 64. can some other mode be 32?
          if !cfg_arch.config.param_values.key?("SXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("SXLEN"), T::Array[Integer]) == [32]
            SatisfiedResult::Maybe
          elsif !cfg_arch.config.param_values.key?("UXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("UXLEN"), T::Array[Integer]) == [32]
            SatisfiedResult::Maybe
          elsif !cfg_arch.config.param_values.key?("VSXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("VSXLEN"), T::Array[Integer]) == [32]
            SatisfiedResult::Maybe
          elsif !cfg_arch.config.param_values.key?("VUXLEN")
            SatisfiedResult::Maybe
          elsif T.cast(cfg_arch.config.param_values.fetch("VUXLEN"), T::Array[Integer]) == [32]
            SatisfiedResult::Maybe
          else
            SatisfiedResult::Yes
          end
        end
      else
        raise "term.xlen is not 32 or 64"
      end
    else
      T.absurd(term)
    end
  end

  Condition.new(
    to_logic_tree(expand:).partial_evaluate(cb).to_h,
    cfg_arch
  )
end

#satisfiability_depends_on_ext_req?(ext_req, include_requirements: false) ⇒ Boolean

Parameters:

Returns:

  • (Boolean) 


988
989
990
991
992
993
994
 
# File 'lib/udb/condition.rb', line 988

def satisfiability_depends_on_ext_req?(ext_req, include_requirements: false)
  if include_requirements
    (self & -ext_req.to_condition & -ext_req.requirements_condition).satisfiable? == false
  else
    (self & -ext_req.to_condition).satisfiable? == false
  end
end

#satisfiable? ⇒ Boolean

is this condition satisfiable?

Returns:

  • (Boolean) 


726
727
728
 
# File 'lib/udb/condition.rb', line 726

def satisfiable?
  solver { |s| s.satisfiable? }
end

#satisfied_by_cfg_arch?(cfg_arch) ⇒ SatisfiedResult

Parameters:

Returns:

  • (SatisfiedResult) 


898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
 
# File 'lib/udb/condition.rb', line 898

def satisfied_by_cfg_arch?(cfg_arch)
  @memo.satisfied_by_cfg_arch[cfg_arch] ||=
    if cfg_arch.fully_configured?
      implemented_ext_cb = make_cb_proc do |term|
        if term.is_a?(ExtensionTerm)
          ext_ver = cfg_arch.implemented_extension_version(term.name)
          next SatisfiedResult::No if ext_ver.nil?
          term.to_ext_req(cfg_arch).satisfied_by?(ext_ver) \
            ? SatisfiedResult::Yes
            : SatisfiedResult::No
        elsif term.is_a?(ParameterTerm)
          if cfg_arch.param_values.key?(term.name)
            term.eval(cfg_arch)
          else
            SatisfiedResult::No
          end
        elsif term.is_a?(FreeTerm)
          raise "unreachable"
        elsif term.is_a?(XlenTerm)
          if cfg_arch.possible_xlens.include?(term.xlen)
            if cfg_arch.possible_xlens.size == 1
              SatisfiedResult::Yes
            else
              SatisfiedResult::Maybe
            end
          else
            SatisfiedResult::No
          end
        else
          T.absurd(term)
        end
      end
      if to_logic_tree(expand: false).eval_cb(implemented_ext_cb) == SatisfiedResult::Yes
        SatisfiedResult::Yes
      else
        SatisfiedResult::No
      end
    elsif cfg_arch.partially_configured?
      cb = make_cb_proc do |term|
        if term.is_a?(ExtensionTerm)
          if cfg_arch.mandatory_extension_reqs.any? { |cfg_ext_req| cfg_ext_req.satisfied_by?(term.to_ext_req(cfg_arch)) }
            SatisfiedResult::Yes
          elsif cfg_arch.possible_extension_versions.any? { |cfg_ext_ver| term.to_ext_req(cfg_arch).satisfied_by?(cfg_ext_ver) }
            SatisfiedResult::Maybe
          else
            SatisfiedResult::No
          end
        elsif term.is_a?(ParameterTerm)
          term.eval(cfg_arch)
        elsif term.is_a?(FreeTerm)
          raise "unreachable"
        elsif term.is_a?(XlenTerm)
          if cfg_arch.possible_xlens.include?(term.xlen)
            if cfg_arch.possible_xlens.size == 1
              SatisfiedResult::Yes
            else
              SatisfiedResult::Maybe
            end
          else
            SatisfiedResult::No
          end
        else
          T.absurd(term)
        end
      end

      to_logic_tree(expand: false).eval_cb(cb)
    else
      # unconfig. Can't really say anthing
      SatisfiedResult::Maybe
    end
end

#satisfied_by_ext_req?(ext_req, include_requirements: false) ⇒ Boolean

Parameters:

Returns:

  • (Boolean) 


972
973
974
975
976
977
978
979
980
981
982
983
984
985
 
# File 'lib/udb/condition.rb', line 972

def satisfied_by_ext_req?(ext_req, include_requirements: false)
  cb = make_cb_proc do |term|
    if term.is_a?(ExtensionTerm)
      if term.to_ext_req(@cfg_arch).satisfied_by?(ext_req)
        SatisfiedResult::Yes
      else
        SatisfiedResult::No
      end
    else
      SatisfiedResult::No
    end
  end
  ext_req.to_condition.to_logic_tree(expand: include_requirements).eval_cb(cb) == SatisfiedResult::Yes
end

#solver(&blk) ⇒ T.type_parameter((:U))

Parameters:

  • blk (T.proc.params(s: Z3Solver).returns(T.type_parameter(:U)))

Returns:

  • (T.type_parameter((:U))) 


705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
 
# File 'lib/udb/condition.rb', line 705

def solver(&blk)
  s = Condition.solver
  s.push
  s.assert to_logic_tree(expand: false).to_z3(@cfg_arch, s)
  expansion_clauses = expand_term_requirements(to_logic_tree(expand: false))
  expansion_clauses.each do |clause|
    s.assert clause.to_z3(@cfg_arch, s)
  end
  # puts "-----------------------"
  # puts s.assertions
  # puts "^^^^^^^^^^^^^^^^^^^^^^"

  ret = yield s

  s.pop

  ret
end

#to_asciidoc ⇒ String

Returns:

  • (String) 


1087
1088
1089
 
# File 'lib/udb/condition.rb', line 1087

def to_asciidoc
  to_logic_tree(expand: false).to_asciidoc(include_versions: false)
end

#to_expanded_logic_tree_shallow ⇒ Object 



644
645
646
647
648
649
650
651
652
653
654
655
656
657
 
# File 'lib/udb/condition.rb', line 644

def to_expanded_logic_tree_shallow
  @expanded_logic_tree_shallow ||=
    begin
      starting_tree = to_logic_tree_internal

      expansion_clauses = expand_term_requirements(starting_tree)

      if expansion_clauses.empty?
        starting_tree
      else
        LogicNode.new(LogicNodeType::And, [starting_tree] + expansion_clauses)
      end
    end
end

#to_h ⇒ Hash{String => T.untyped}, Boolean

Returns:

  • (Hash{String => T.untyped}, Boolean) 


1013
1014
1015
 
# File 'lib/udb/condition.rb', line 1013

def to_h
  to_logic_tree(expand: false).to_h
end

#to_idl(cfg_arch) ⇒ String

Parameters:

Returns:

  • (String) 


1018
1019
1020
1021
 
# File 'lib/udb/condition.rb', line 1018

def to_idl(cfg_arch)
  idl = to_logic_tree(expand: false).to_idl(cfg_arch)
  "-> #{idl};"
end

#to_logic_tree(expand:) ⇒ LogicNode

Parameters:

  • expand (Boolean)

Returns:



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
 
# File 'lib/udb/condition.rb', line 660

def to_logic_tree(expand:)
  if expand
    @logic_tree_expanded ||=
      begin
        # we do several things in expansion:
        #
        #  1. expand any requirements of extensions/parameters
        #  2. ensure XLEN is exclusive (can be 32 or 64, but not both)
        #  3. ensure zero or one version of an extension can be implemented
        starting_tree = to_logic_tree_internal

        expansion_clauses = expand_term_requirements(starting_tree)

        expand_extension_version_ranges(starting_tree, expansion_clauses)

        # enforce_single_ext_ver must come after expand_extension_version_ranges
        expand_to_enforce_single_ext_ver(starting_tree, expansion_clauses)

        expand_to_enforce_param_relations(starting_tree, expansion_clauses)

        expand_xlen(starting_tree, expansion_clauses)

        expanded_tree =
          if expansion_clauses.empty?
            starting_tree
          else
            LogicNode.new(LogicNodeType::And, [starting_tree] + expansion_clauses)
          end

        expanded_tree
      end
  else
    @logic_tree_unexpanded ||= to_logic_tree_helper(@yaml)
  end
end

#to_logic_tree_internal ⇒ LogicNode

This method is part of a private API. You should avoid using this method if possible, as it may be removed or be changed in the future.

Returns:



746
747
748
 
# File 'lib/udb/condition.rb', line 746

def to_logic_tree_internal
  to_logic_tree_helper(@yaml)
end

#to_s(expand: false) ⇒ String

Parameters:

  • expand (Boolean) (defaults to: false)

Returns:

  • (String) 


1024
1025
1026
 
# File 'lib/udb/condition.rb', line 1024

def to_s(expand: false)
  to_logic_tree(expand:).to_s(format: LogicNode::LogicSymbolFormat::C)
end

#to_s_pretty ⇒ String

return the condition in a nice, human-readable form

Returns:

  • (String) 


1030
1031
1032
 
# File 'lib/udb/condition.rb', line 1030

def to_s_pretty
  to_logic_tree(expand: false).to_s_pretty
end

#to_s_with_value(cfg_arch, expand: false) ⇒ String

Parameters:

Returns:

  • (String) 


1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
 
# File 'lib/udb/condition.rb', line 1035

def to_s_with_value(cfg_arch, expand: false)
  cb = LogicNode.make_eval_cb do |term|
    case term
    when ExtensionTerm
      if cfg_arch.fully_configured?
        ext_ver = cfg_arch.implemented_extension_version(term.name)
        if ext_ver.nil? || !term.to_ext_req(cfg_arch).satisfied_by?(ext_ver)
          SatisfiedResult::No
        else
          SatisfiedResult::Yes
        end
      elsif cfg_arch.partially_configured?
        if cfg_arch.mandatory_extension_reqs.any? { |cfg_ext_req| cfg_ext_req.satisfied_by?(term.to_ext_req(cfg_arch)) }
          SatisfiedResult::Yes
        elsif cfg_arch.possible_extension_versions.any? { |cfg_ext_ver| term.to_ext_req(cfg_arch).satisfied_by?(cfg_ext_ver) }
          SatisfiedResult::Maybe
        else
          SatisfiedResult::No
        end
      else
        SatisfiedResult::Maybe
      end
    when ParameterTerm
      if cfg_arch.fully_configured?
        if cfg_arch.param_values.key?(term.name)
          term.eval(cfg_arch)
        else
          SatisfiedResult::No
        end
      elsif cfg_arch.partially_configured?
        term.eval(cfg_arch)
      else
        SatisfiedResult::Maybe
      end
    when XlenTerm
      if cfg_arch.possible_xlens.include?(term.xlen)
        if cfg_arch.possible_xlens.size == 1
          SatisfiedResult::Yes
        else
          SatisfiedResult::Maybe
        end
      else
        SatisfiedResult::No
      end
    else
      raise "unexpected term type #{term.class.name}"
    end
  end
  to_logic_tree(expand:).to_s_with_value(cb, format: LogicNode::LogicSymbolFormat::C)
end

#unsatisfiable? ⇒ Boolean

is this condition unsatisfiable?

Returns:

  • (Boolean) 


732
733
734
 
# File 'lib/udb/condition.rb', line 732

def unsatisfiable?
  solver { |s| s.unsatisfiable? }
end

#|(other) ⇒ AbstractCondition

Parameters:

Returns:



1353
1354
1355
 
# File 'lib/udb/condition.rb', line 1353

def |(other)
  Condition.disjunction([self, other], @cfg_arch)
end