ARM/v4/instructionSyntax.sml

47     AND => ``instruction$AND`` | EOR => ``instruction$EOR``
48   | SUB => ``instruction$SUB`` | RSB => ``instruction$RSB``
49   | ADD => ``instruction$ADD`` | ADC => ``instruction$ADC``
50   | SBC => ``instruction$SBC`` | RSC => ``instruction$RSC``
51   | TST => ``instruction$TST`` | TEQ => ``instruction$TEQ``
52   | CMP => ``instruction$CMP`` | CMN => ``instruction$CMN``
53   | ORR => ``instruction$ORR`` | MOV => ``instruction$MOV``
54   | BIC => ``instruction$BIC`` | MVN => ``instruction$MVN``;
61         (if #L y then ``instruction$BL c offset``
62                  else ``instruction$B c offset``)
63   | _ => raise ERR "mk_br" "not a branch instruction")
64  | mk_br _ = raise ERR "mk_br" "not a branch instruction";
86      LSL => ``instruction$LSL r``
87    | LSR => ``instruction$LSR r``
88    | ASR => ``instruction$ASR r``
89    | ROR => ``instruction$ROR r``);
109   val err = ERR "mk_data_proc" "not a data processing instruction"
161   | _ => raise ERR "mk_mla_mul" "not a multiply instruction")
162  | mk_mla_mul _ = raise ERR "mk_mla_mul" "not a multiply instruction";
179     | mk_options _ = raise ERR "mk_ldr_str" "not a load/store instruction"
180   val err = ERR "mk_ldr_str" "not a load/store instruction"
192            ``instruction$LDR c b opt rd rn offset``
194            ``instruction$STR c b opt rd rn offset``)
213                                "not a load/store (half) instruction"
214   val err = ERR "mk_ldrh_strh" "not a load/store (half) instruction"
228               ``instruction$LDRH c s h opt rd rn offset``
230            ``instruction$STRH c opt rd rn offset``)
241     | mk_options _ = raise ERR "mk_ldm_stm" "not a block transfer instruction"
242   val err = ERR "mk_ldm_stm" "not a block transfer instruction"
253            ``instruction$LDM c s opt rn list``
255            ``instruction$STM c s opt rn list``)
268       ``instruction$SWP c b rd rm rn``
269   | _ => raise ERR "mk_swp" "not a swap instruction")
270  | mk_swp _ = raise ERR "mk_swp" "not a swap instruction";
278         ``instruction$MRS c r rd``
279   | _ => raise ERR "mk_mrs" "not an mrs instruction")
280  | mk_mrs _ = raise ERR "mk_mrs" "not an mrs instruction";
293     | mk_msr_psr _ = raise ERR "mk_msr" "not an msr instruction"
307   val err = ERR "mk_msr" "not an msr instruction"
315         ``instruction$MSR c psrd op``
330       ``instruction$CDP c cpn cop1 crd crn crm cop2``
331   | _ => raise ERR "mk_cdp" "not a cdp instruction")
332  | mk_cdp _ = raise ERR "mk_cdp" "not a cdp instruction";
345          ``instruction$MRC c cpn cop1 rd crn crm cop2``
347          ``instruction$MCR c cpn cop1 rd crn crm cop2``)
348   | _ => raise ERR "mk_mcr_mrc" "not an mcr or mrc instruction")
349  | mk_mcr_mrc _ = raise ERR "mk_mcr_mrc" "not an mcr or mrc instruction";
357     | mk_options _ = raise ERR "mk_ldc_stc" "not an ldc or stc instruction"
358   val err = ERR "mk_ldc_stc" "not an ldc or stc instruction"
371            ``instruction$LDC c n opt cpn crd rn offset``
373            ``instruction$STC c n opt cpn crd rn offset``)
452   val err = ERR "dest_br" "not a variable-free branch instruction"
456       (i, [c, offset]) => let val l = term_eq i ``instruction$BL`` in
457           if l orelse term_eq i ``instruction$B`` then
467   val err = ERR "dest_swi_ex" "not a valid swi_ex instruction"
471      if term_eq i ``instruction$SWI`` then
479   val err = ERR "dest_undef" "not a valid undefined instruction"
483      if term_eq i ``instruction$UND`` then
492   if eqt ``instruction$AND`` then AND else
493   if eqt ``instruction$EOR`` then EOR else
494   if eqt ``instruction$SUB`` then SUB else
495   if eqt ``instruction$RSB`` then RSB else
496   if eqt ``instruction$ADD`` then ADD else
497   if eqt ``instruction$ADC`` then ADC else
498   if eqt ``instruction$SBC`` then SBC else
499   if eqt ``instruction$RSC`` then RSC else
500   if eqt ``instruction$ORR`` then ORR else
501   if eqt ``instruction$BIC`` then BIC else raise ERR "dest_opc1"
507   if eqt ``instruction$TST`` then TST else
508   if eqt ``instruction$TEQ`` then TEQ else
509   if eqt ``instruction$CMP`` then CMP else
510   if eqt ``instruction$CMN`` then CMN else
515   if term_eq t ``instruction$MOV`` then MOV else
516   if term_eq t ``instruction$MVN`` then MVN else
521   if term_eq s ``instruction$LSL`` then (LSL, dest_register r) else
522   if term_eq s ``instruction$LSR`` then (LSR, dest_register r) else
523   if term_eq s ``instruction$ASR`` then (ASR, dest_register r) else
524   if term_eq s ``instruction$ROR`` then (ROR, dest_register r) else
547   val err = ERR "dest_data_proc" "not a variable-free data_proc instruction"
568   val err = ERR "dest_mla_mul" "not a variable-free multiply instruction"
573          if term_eq i ``instruction$MUL`` then
581          if term_eq i ``instruction$MLA`` then
586          else if term_eq i ``instruction$UMULL`` then
591          else if term_eq i ``instruction$UMLAL`` then
596          else if term_eq i ``instruction$SMULL`` then
601          else if term_eq i ``instruction$SMLAL`` then
640   val err = ERR "dest_ldr_str" "not a variable-free load/store instruction"
645         let val l = term_eq i ``instruction$LDR``
648           if l orelse term_eq i ``instruction$STR`` then
676   val err = ERR "dest_ldr_str" "not a variable-free load/store instruction"
682           if term_eq i ``instruction$LDRH`` then
691           if term_eq i ``instruction$STRH`` then
703   val err = ERR "dest_ldm_stm" "not a variable-free block transfer instruction"
708         let val l = term_eq i ``instruction$LDM``
711           if l orelse term_eq i ``instruction$STM`` then
723   val err = ERR "dest_swp" "not a variable-free swap instruction"
728         if term_eq i ``instruction$SWP`` then
738   val err = ERR "dest_mrs" "not a variable-free mrs instruction"
743         if term_eq i ``instruction$MRS`` then
782   val err = ERR "dest_msr" "not a variable-free mrs instruction"
787         if term_eq i ``instruction$MSR`` then
799   val err = ERR "dest_cdp" "not a variable-free cdp instruction"
804         if term_eq i ``instruction$CDP`` then
815   val err = ERR "dest_ldc_stc" "not a variable-free ldc/stc instruction"
820         let val l = term_eq i ``instruction$LDC``
823           if l orelse term_eq i ``instruction$STC`` then
836   val err = ERR "dest_mcr_mrc" "not a variable-free mcr/mrc instruction"
841         let val l = term_eq i ``instruction$MCR`` in
842           if l orelse term_eq i ``instruction$MRC`` then
862     if eqt ``instruction$SWI`` then
864     else if eqt ``instruction$B`` orelse eqt ``instruction$BL`` then
866     else if eqt ``instruction$MUL`` orelse eqt ``instruction$MLA`` orelse
867             eqt ``instruction$UMULL`` orelse eqt ``instruction$UMLAL`` orelse
868             eqt ``instruction$SMULL`` orelse eqt ``instruction$SMLAL`` then
870     else if eqt ``instruction$LDRH`` orelse eqt ``instruction$STRH`` then
872     else if eqt ``instruction$LDR`` orelse eqt ``instruction$STR`` then
874     else if eqt ``instruction$LDM`` orelse eqt ``instruction$STM`` then
876     else if eqt ``instruction$SWP`` then
878     else if eqt ``instruction$MRS`` then
880     else if eqt ``instruction$MSR`` then
882     else if eqt ``instruction$CDP`` then
884     else if eqt ``instruction$LDC`` orelse eqt ``instruction$STC`` then
886     else if eqt ``instruction$MCR`` orelse eqt ``instruction$MRC`` then
888     else if eqt ``instruction$UND`` then
894   raise ERR "term_to_arm" "not a variable-free ARM instruction";