Index: trunk/src/VBox/VMM/VMMAll/target-armv8/bsd-spec-analyze.py
===================================================================
--- trunk/src/VBox/VMM/VMMAll/target-armv8/bsd-spec-analyze.py	(revision 108950)
+++ trunk/src/VBox/VMM/VMMAll/target-armv8/bsd-spec-analyze.py	(revision 108952)
@@ -353,4 +353,5 @@
 
 
+
 #
 # The ARM instruction AST stuff.
@@ -510,4 +511,13 @@
     def clone(self):
         return ArmAstBinaryOp(self.oLeft.clone(), self.sOp, self.oRight.clone());
+
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstBinaryOp):
+            if self.sOp == oOther.sOp:
+                if self.oLeft.isSame(oOther.oLeft):
+                    if self.oRight.isSame(oOther.oRight):
+                        return True;
+            ## @todo switch sides and whatnot.
+        return False;
 
     @staticmethod
@@ -603,4 +613,11 @@
         return ArmAstUnaryOp(self.sOp, self.oExpr.clone());
 
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstUnaryOp):
+            if self.sOp == oOther.sOp:
+                if self.oExpr.isSame(oOther.oExpr):
+                    return True;
+        return False;
+
     @staticmethod
     def needParentheses(oNode):
@@ -628,4 +645,14 @@
         return ArmAstSquareOp(self.oVar.clone(), [oValue.clone() for oValue in self.aoValues]);
 
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstSquareOp):
+            if self.oVar.isSame(oOther.oVar):
+                if len(self.aoValues) == len(oOther.aoValues):
+                    for idx, oMyValue in enumerate(self.aoValues):
+                        if not oMyValue.isSame(oOther.aoValues[idx]):
+                            return False;
+                    return True;
+        return False;
+
     def toString(self):
         return '%s<%s>' % (self.oVar.toString(), ','.join([oValue.toString() for oValue in self.aoValues]),);
@@ -643,4 +670,13 @@
     def clone(self):
         return ArmAstConcat([oValue.clone() for oValue in self.aoValues]);
+
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstConcat):
+            if len(self.aoValues) == len(oOther.aoValues):
+                for idx, oMyValue in enumerate(self.aoValues):
+                    if not oMyValue.isSame(oOther.aoValues[idx]):
+                        return False;
+                return True;
+        return False;
 
     def toString(self):
@@ -685,4 +721,14 @@
         return ArmAstFunction(self.sName, [oArg.clone() for oArg in self.aoArgs]);
 
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstFunction):
+            if self.sName == oOther.sName:
+                if len(self.aoArgs) == len(oOther.aoArgs):
+                    for idx, oMyArg in enumerate(self.aoArgs):
+                        if not oMyArg.isSame(oOther.aoArgs[idx]):
+                            return False;
+                    return True;
+        return False;
+
     def toString(self):
         return '%s(%s)' % (self.sName, ','.join([oArg.toString() for oArg in self.aoArgs]),);
@@ -702,4 +748,10 @@
     def clone(self):
         return ArmAstIdentifier(self.sName);
+
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstIdentifier):
+            if self.sName == oOther.sName:
+                return True;
+        return False;
 
     def toString(self):
@@ -720,4 +772,10 @@
         return ArmAstBool(self.fValue);
 
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstBase):
+            if self.fValue == oOther.fValue:
+                return True;
+        return False;
+
     def toString(self):
         return 'true' if self.fValue is True else 'false';
@@ -726,4 +784,5 @@
         _ = oHelper;
         return 'true' if self.fValue is True else 'false';
+
 
 class ArmAstInteger(ArmAstBase):
@@ -734,4 +793,10 @@
     def clone(self):
         return ArmAstInteger(self.iValue);
+
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstInteger):
+            if self.iValue == oOther.iValue:
+                return True;
+        return False;
 
     def toString(self):
@@ -746,4 +811,5 @@
         return '%#x' % (self.iValue,);
 
+
 class ArmAstSet(ArmAstBase):
     def __init__(self, aoValues):
@@ -754,4 +820,13 @@
         return ArmAstSet([oValue.clone() for oValue in self.aoValues]);
 
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstSet):
+            if len(self.aoValues) == len(oOther.aoValues):
+                for idx, oMyValue in enumerate(self.aoValues):
+                    if not oMyValue.isSame(oOther.aoValues[idx]):
+                        return False;
+                return True;
+        return False;
+
     def toString(self):
         return '(%s)' % (', '.join([oValue.toString() for oValue in self.aoValues]),);
@@ -760,4 +835,5 @@
         _ = oHelper;
         raise Exception('ArmAstSet does not support conversion to C expression: %s' % (self.toString()));
+
 
 class ArmAstValue(ArmAstBase):
@@ -768,4 +844,10 @@
     def clone(self):
         return ArmAstValue(self.sValue);
+
+    def isSame(self, oOther):
+        if isinstance(oOther, ArmAstValue):
+            if self.sValue == oOther.sValue:
+                return True;
+        return False;
 
     def toString(self):
@@ -899,6 +981,6 @@
         self.sName           = sName;
         self.oParent         = oParent;
-        self.aoFields        = aoFields;
-        self.fFields         = fFields;  ##< Not necessarily correct for Instructions!
+        self.aoFields        = aoFields     # type: List[ArmEncodesetField]
+        self.fFields         = fFields;
         self.oCondition      = oCondition;
 
@@ -1133,4 +1215,35 @@
 ## The instruction groups.
 g_dArmInstructionGroups = {}                                    # type: Dict[ArmInstructionGroup]
+
+
+## Instruction corrections expressed as a list required conditionals.
+#
+# In addition to supplying missing conditionals (IsFeatureImplemented(FEAT_XXX)
+# and missing fixed encoding values (field == <fixed-value>).
+#
+# The reason why this is a list and not an expression, is that it easier to skip
+# stuff that's already present in newer specification and avoiding duplicate tests.
+g_dArmEncodingCorrectionConditions = {
+    # The sdot and udot vector instructions are missing the 'size' restrictions in the 2024-12 specs.
+    'sdot_z_zzz_': (ArmAstBinaryOp(ArmAstIdentifier('size'), '!=', ArmAstValue("'00'")),
+                    ArmAstBinaryOp(ArmAstIdentifier('size'), '!=', ArmAstValue("'01'")),),
+    'udot_z_zzz_': (ArmAstBinaryOp(ArmAstIdentifier('size'), '!=', ArmAstValue("'00'")),
+                    ArmAstBinaryOp(ArmAstIdentifier('size'), '!=', ArmAstValue("'01'")),),
+    # These instructions are FEAT_MTE && FEAT_MOPS. The 2024-12 specs missed the former condition.
+    'SETGEN_SET_memcms':  (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGETN_SET_memcms': (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGET_SET_memcms':  (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGE_SET_memcms':   (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGMN_SET_memcms':  (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGMTN_SET_memcms': (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGMT_SET_memcms':  (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGM_SET_memcms':   (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGPN_SET_memcms':  (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGPTN_SET_memcms': (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGPT_SET_memcms':  (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+    'SETGP_SET_memcms':   (ArmAstFunction('IsFeatureImplemented', [ArmAstIdentifier('FEAT_MTE'),]),),
+
+    ## @todo fexpa_z_z: s/FEAT_SME2p2/FEAT_SSVE_FEXPA/ (2024-12 vs 2025-03); Not relevant since we don't support either.
+};
 
 
@@ -1252,4 +1365,7 @@
 
             oCondition = ArmAstBase.fromJson(oJson['condition']);
+            aoCorrectionConditions = g_dArmEncodingCorrectionConditions.get(sInstrNm)
+            if aoCorrectionConditions:
+                oCondition = addAndConditionsFromList(oCondition, aoCorrectionConditions);
 
             (aoFields, fFields) = ArmEncodesetField.encodesetFromJson(oJson['encoding']);
@@ -1267,5 +1383,6 @@
             (oCondition, fMod) = transferConditionsToEncoding(oCondition, aoFields, collections.defaultdict(list), sInstrNm);
             #if fMod:
-            #    print('debug transfer: %s: %s  ---->  %s' % (sInstrNm, sCondBefore, oCondition.toString()));
+            #    print('debug transfer: %s: %s' % (sInstrNm, sCondBefore,));
+            #    print('              %*s %s' % (len(sInstrNm) + 3, '--->', oCondition.toString(),));
             _ = fMod;
 
@@ -1300,4 +1417,38 @@
 
     return True;
+
+
+def addAndConditionsFromList(oTree, aoAndConditions):
+    """
+    Adds the conditions in aoAndConditions that are not already present in
+    oTree in an required (AND) form.
+
+    This is used when we add corrections, so that we avoid duplicate feature
+    checks and such.
+    """
+    if oTree.isBoolAndTrue():
+        return andConditionListToTree(aoAndConditions);
+
+    def isAndConditionPresent(oTree, oAndCondition):
+        if oAndCondition.isSame(oTree):
+            return True;
+        if isinstance(oTree, ArmAstBinaryOp) and oTree.sOp == '&&':
+            return isAndConditionPresent(oTree.oLeft, oAndCondition) or isAndConditionPresent(oTree.oRight, oAndCondition);
+        return False;
+
+    aoToAdd = [oTree,];
+    for oAndCondition in aoAndConditions:
+        if not isAndConditionPresent(oTree, oAndCondition):
+            aoToAdd.append(oAndCondition);
+
+    return andConditionListToTree(aoToAdd);
+
+
+def andConditionListToTree(aoAndConditions):
+    """ Creates AST tree of AND binary checks from aoAndConditions. """
+    if len(aoAndConditions) <= 1:
+        return aoAndConditions[0].clone();
+    return ArmAstBinaryOp(aoAndConditions[0].clone(), '&&', andConditionListToTree(aoAndConditions[1:]));
+
 
 def transferConditionsToEncoding(oCondition, aoFields, dPendingNotEq, sInstrNm, uDepth = 0, fMod = False):
@@ -1338,5 +1489,5 @@
                 for oField in aoFields: # ArmEncodesetField
                     if oField.sName and oField.sName == sFieldName:
-                        # ArmAstInteger (unlikely):
+                        # ArmAstInteger - not used by spec, only corrections:
                         if isinstance(oValue, ArmAstInteger):
                             if oField.fFixed != 0:
@@ -1357,6 +1508,6 @@
                                 break;
 
-                            #print('debug transfer: %s: integer binaryop -> encoding: %s %s %#x/%#x'
-                            #      % (sInstrNm, oField.sName, oCondition.sOp, oValue.iValue, fFixed));
+                            print('debug transfer: %s: integer binaryop -> encoding: %s %s %#x/%#x'
+                                  % (sInstrNm, oField.sName, oCondition.sOp, oValue.iValue, fFixed));
                             if oCondition.sOp == '==':
                                 oField.fValue = oValue.iValue;
@@ -1395,5 +1546,5 @@
                 if oCondition.sOp == '&&':
                     oCondition.oLeft  = recursiveRemove(oCondition.oLeft, aoToRemove);
-                    oCondition.oRight = recursiveRemove(oCondition.oLeft, aoToRemove);
+                    oCondition.oRight = recursiveRemove(oCondition.oRight, aoToRemove);
                     if oCondition.oLeft.isBoolAndTrue():    return oCondition.oRight;
                     if oCondition.oRight.isBoolAndTrue():   return oCondition.oLeft;
@@ -1427,5 +1578,4 @@
                     oField.fFixed |= fFixed;
 
-
                     # Remove the associated conditions (they'll be leaves).
                     oCondition = recursiveRemove(oCondition, [oCondition for _, _, _, oCondition in atOccurences]);
@@ -1495,7 +1645,14 @@
     #print("oBrk=%s" % (oBrk,))
 
-    if oOptions.fPrintInstructions:
+    if oOptions.fPrintInstructions or oOptions.fPrintInstructionsWithEncoding or oOptions.fPrintInstructionsWithConditions:
         for oInstr in g_aoAllArmInstructions:
             print('%08x/%08x %s %s' % (oInstr.fFixedMask, oInstr.fFixedValue, oInstr.getCName(), oInstr.sAsmDisplay));
+            if oOptions.fPrintInstructionsWithEncoding:
+                for oField in sorted(oInstr.aoFields, key = operator.attrgetter('iFirstBit')): # ArmEncodesetField
+                    print('  %2u L %2u: %010x/%010x%s%s'
+                          % (oField.iFirstBit, oField.cBitsWidth, oField.fFixed, oField.fValue,
+                             ' ' if oField.sName else '', oField.sName if oField.sName else '',));
+            if oOptions.fPrintInstructionsWithConditions and not oInstr.oCondition.isBoolAndTrue():
+                print('  condition: %s' % (oInstr.oCondition.toString(),));
 
     # Gather stats on fixed bits:
@@ -2145,4 +2302,7 @@
         Returns the lines for a license header.
         """
+        sDashYear = '-%s' % datetime.date.today().year;
+        if sDashYear == '-2025':
+            sDashYear = '';
         return [
             '/*',
@@ -2156,5 +2316,5 @@
             '',
             '/*',
-            ' * Copyright (C) 2025-' + str(datetime.date.today().year) + ' Oracle and/or its affiliates.',
+            ' * Copyright (C) 2025' + sDashYear + ' Oracle and/or its affiliates.',
             ' *',
             ' * This file is part of VirtualBox base platform packages, as',
@@ -2293,5 +2453,5 @@
                 ];
                 asTail  = [
-                    '    LogFlow(("Invalid instruction %%#x at %%x\\n", uOpcode, pVCpu->cpum.GstCtx.Pc.u64));',
+                    '    Log(("Invalid instruction %%#x at %%x\\n", uOpcode, pVCpu->cpum.GstCtx.Pc.u64));',
                     '    IEMOP_RAISE_INVALID_OPCODE_RET();',
                     '}',
@@ -2321,5 +2481,5 @@
 
                 asTail = [
-                    sIndent + '    LogFlow(("Invalid instruction %%#x at %%x (cond)\\n", uOpcode, pVCpu->cpum.GstCtx.Pc.u64));',
+                    sIndent + '    Log(("Invalid instruction %%#x at %%x (cond)\\n", uOpcode, pVCpu->cpum.GstCtx.Pc.u64));',
                     sIndent + '    IEMOP_RAISE_INVALID_OPCODE_RET();',
                     sIndent + '}',
@@ -2329,5 +2489,6 @@
             # Log and call implementation.
             asLines += [
-                '%s    LogFlow(("%%010x: %s%s\\n",%s));' % (sIndent, sCName, sLogFmt, ', '.join(['uOpcode',] + asArgs),),
+                '%s    LogFlow(("%%018x/%%010x: %s%s\\n", %s));'
+                % (sIndent, sCName, sLogFmt, ', '.join(['pVCpu->cpum.GstCtx.Pc.u64', 'uOpcode',] + asArgs),),
                 '#ifdef IEM_INSTR_IMPL_%s__%s' % (sInstrSet, sCName,),
                 '%s    IEM_INSTR_IMPL_%s__%s(%s);' % (sIndent, sInstrSet, sCName, ', '.join(asArgs),),
@@ -2486,5 +2647,5 @@
             'FNIEMOP_DEF_1(iemDecode%s_Invalid, uint32_t, uOpcode)' % (sInstrSet,),
             '{',
-            '    LogFlow(("Invalid instruction %%#x at %%x\\n", uOpcode, pVCpu->cpum.GstCtx.Pc.u64));',
+            '    Log(("Invalid instruction %%#x at %%x\\n", uOpcode, pVCpu->cpum.GstCtx.Pc.u64));',
             '    IEMOP_RAISE_INVALID_OPCODE_RET();',
             '}',
@@ -2583,5 +2744,5 @@
                                 dest    = 'sFileDecoderCpp',
                                 action  = 'store',
-                                default = '-',
+                                default = None,
                                 help    = 'The output C++ file for the decoder.');
         oArgParser.add_argument('--out-decoder-hdr',
@@ -2589,5 +2750,5 @@
                                 dest    = 'sFileDecoderHdr',
                                 action  = 'store',
-                                default = '-',
+                                default = None,
                                 help    = 'The output header file for the decoder.');
         oArgParser.add_argument('--out-stub-hdr',
@@ -2595,5 +2756,5 @@
                                 dest    = 'sFileStubHdr',
                                 action  = 'store',
-                                default = '-',
+                                default = None,
                                 help    = 'The output header file for the implementation stubs.');
         # debug:
@@ -2603,4 +2764,14 @@
                                 default = False,
                                 help    = 'List the instructions after loading.');
+        oArgParser.add_argument('--print-instructions-with-conditions',
+                                dest    = 'fPrintInstructionsWithConditions',
+                                action  = 'store_true',
+                                default = False,
+                                help    = 'List the instructions and conditions after loading.');
+        oArgParser.add_argument('--print-instructions-with-encoding',
+                                dest    = 'fPrintInstructionsWithEncoding',
+                                action  = 'store_true',
+                                default = False,
+                                help    = 'List the instructions and encoding details after loading.');
         oArgParser.add_argument('--print-fixed-mask-stats',
                                 dest    = 'fPrintFixedMaskStats',
@@ -2621,10 +2792,5 @@
         if LoadArmOpenSourceSpecification(oOptions):
             #
-            # Sort out the decoding.
-            #
-            self.constructDecoder();
-
-            #
-            # Output.
+            # Check if we're generating any output before constructing the decoder.
             #
             aaoOutputFiles = [
@@ -2633,21 +2799,37 @@
                  ( oOptions.sFileStubHdr,         self.generateA64ImplementationStubHdr, 0, ),
             ];
+
+            cOutputFiles = 0;
+            for sOutFile, _, _ in aaoOutputFiles:
+                cOutputFiles += sOutFile is not None;
+
             fRc = True;
-            for sOutFile, fnGenMethod, iPartNo in aaoOutputFiles:
-                if sOutFile == '-':
-                    oOut = sys.stdout;
-                else:
-                    try:
-                        oOut = open(sOutFile, 'w');                 # pylint: disable=consider-using-with,unspecified-encoding
-                    except Exception as oXcpt:
-                        print('error! Failed open "%s" for writing: %s' % (sOutFile, oXcpt,), file = sys.stderr);
-                        return 1;
-
-                (fRc2, asLines) = fnGenMethod(sOutFile, iPartNo);
-                fRc = fRc2 and fRc;
-
-                oOut.write('\n'.join(asLines));
-                if oOut != sys.stdout:
-                    oOut.close();
+            if cOutputFiles > 0:
+                #
+                # Sort out the decoding.
+                #
+                self.constructDecoder();
+
+                #
+                # Output.
+                #
+                for sOutFile, fnGenMethod, iPartNo in aaoOutputFiles:
+                    if not sOutFile:
+                        continue;
+                    if sOutFile == '-':
+                        oOut = sys.stdout;
+                    else:
+                        try:
+                            oOut = open(sOutFile, 'w');                 # pylint: disable=consider-using-with,unspecified-encoding
+                        except Exception as oXcpt:
+                            print('error! Failed open "%s" for writing: %s' % (sOutFile, oXcpt,), file = sys.stderr);
+                            return 1;
+
+                    (fRc2, asLines) = fnGenMethod(sOutFile, iPartNo);
+                    fRc = fRc2 and fRc;
+
+                    oOut.write('\n'.join(asLines));
+                    if oOut != sys.stdout:
+                        oOut.close();
             if fRc:
                 return 0;
