ARM/v4/arm_rulesScript.sml

242 val ARM_AND_NOP = eval_nop ``instruction$AND``
243 val ARM_EOR_NOP = eval_nop ``instruction$EOR``
244 val ARM_SUB_NOP = eval_nop ``instruction$SUB``
245 val ARM_RSB_NOP = eval_nop ``instruction$RSB``
246 val ARM_ADD_NOP = eval_nop ``instruction$ADD``
247 val ARM_ADC_NOP = eval_nop ``instruction$ADC``
248 val ARM_SBC_NOP = eval_nop ``instruction$SBC``
249 val ARM_RSC_NOP = eval_nop ``instruction$RSC``
250 val ARM_ORR_NOP = eval_nop ``instruction$ORR``
251 val ARM_BIC_NOP = eval_nop ``instruction$BIC``
254   ``enc (instruction$MOV c s Rd Op2)``);
257   ``enc (instruction$MVN c s Rd Op2)``);
260   ``enc (instruction$TST c Rm Op2)``);
263   ``enc (instruction$TEQ c Rm Op2)``);
266   ``enc (instruction$CMP c Rm Op2)``);
269   ``enc (instruction$CMN c Rm Op2)``);
272   ``enc (instruction$MUL c s Rd Rs Rm)``);
275   ``enc (instruction$MLA c s Rd Rs Rm Rn)``);
278   ``enc (instruction$UMULL c s RdLo RdHi Rs Rm)``);
281   ``enc (instruction$UMLAL c s RdLo RdHi Rs Rm)``);
284   ``enc (instruction$SMULL c s RdLo RdHi Rs Rm)``);
287   ``enc (instruction$SMLAL c s RdLo RdHi Rs Rm)``);
290   ``enc (instruction$B c offset)``);
293   ``enc (instruction$BL c offset)``);
296   ``enc (instruction$SWI c)``);
299   ``enc (instruction$UND c)``);
302   ``enc (instruction$LDR c b opt Rd Rn Op2)``);
305   ``enc (instruction$STR c b opt Rd Rn Op2)``);
308   ``enc (instruction$SWP c b Rd Rm Rn)``);
311   ``enc (instruction$LDM c s opt Rd list)``);
314   ``enc (instruction$STM c s opt Rd list)``);
317   ``enc (instruction$MRS c r Rd)``);
320   ``enc (instruction$MSR c psrd op2)``);
323   ``enc (instruction$CDP c CPn Cop1 CRd CRn CRm Cop2)``);
326   ``enc (instruction$LDC c n options CPn CRd Rn offset)``);
329   ``enc (instruction$STC c n options CPn CRd Rn offset)``);
332   ``enc (instruction$MRC c CPn Cop1 Rd CRn CRm Cop2)``);
335   ``enc (instruction$MCR c CPn Cop1 Rd CRn CRm Cop2)``);
342   (SYMBOLIC_EVAL_CONV BRANCH_ss (cntxt [] ``enc (instruction$B c offset)``));
345   (SYMBOLIC_EVAL_CONV BRANCH_ss (cntxt [] ``enc (instruction$BL c offset)``));
352   (SYMBOLIC_EVAL_CONV SWI_EX_ss (cntxt [] ``enc (instruction$SWI c)``));
355   (SYMBOLIC_EVAL_CONV SWI_EX_ss (cntxt [] ``enc (instruction$UND c)``));
396   [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$TST c Rm Op2)``);
399   [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$TEQ c Rm Op2)``);
402   [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$CMP c Rm Op2)``);
405   [``~(Rm = 15w:word4)``,abbrev_mode1] ``enc (instruction$CMN c Rm Op2)``);
416 val ARM_AND = eval_op ``instruction$AND``;
417 val ARM_EOR = eval_op ``instruction$EOR``;
418 val ARM_SUB = eval_op ``instruction$SUB``;
419 val ARM_RSB = eval_op ``instruction$RSB``;
420 val ARM_ADD = eval_op ``instruction$ADD``;
421 val ARM_ORR = eval_op ``instruction$ORR``;
422 val ARM_BIC = eval_op ``instruction$BIC``;
423 val ARM_ADC = eval_op ``instruction$ADC``;
424 val ARM_SBC = eval_op ``instruction$SBC``;
425 val ARM_RSC = eval_op ``instruction$RSC``;
429   ``enc (instruction$MOV c s Rd Op2)``);
433   ``enc (instruction$MVN c s Rd Op2)``);
448 val ARM_ADD_TO_PC = eval_op ``instruction$ADD``;
449 val ARM_SUB_TO_PC = eval_op ``instruction$SUB``;
459   ``enc (instruction$MUL c s Rd Rm Rs)``);
463   ``enc (instruction$MLA c s Rd Rm Rs Rn)``);
468   ``enc (instruction$UMULL c s RdLo RdHi Rm Rs)``);
473   ``enc (instruction$UMLAL c s RdLo RdHi Rm Rs)``);
478   ``enc (instruction$SMULL c s RdLo RdHi Rm Rs)``);
483   ``enc (instruction$SMLAL c s RdLo RdHi Rm Rs)``);
510   ``enc (instruction$LDR c b opt Rd Rn offset)``);
514   ``enc (instruction$STR c b opt Rd Rn offset)``);
519   ``enc (instruction$LDR c b opt Rd Rn offset)``));
524   ``enc (instruction$STR c b opt Rd Rn offset)``));
535   ``enc (instruction$SWP c b Rd Rm Rn)``);
628   ``enc (instruction$LDM c s opt Rd list)``));
633   ``enc (instruction$STM c s opt Rd list)``));
657    ``enc (instruction$MSR c psrd op2)``);
660   (SYMBOLIC_EVAL_CONV MRS_MSR_ss (cntxt [] ``enc (instruction$MRS c r Rd)``));
692    ``enc (instruction$CDP c CPn Cop1 CRd CRn CRm Cop2)``));
696    ``enc (instruction$LDC c n options CPn CRd Rn offset)``));
700    ``enc (instruction$STC c n options CPn CRd Rn offset)``));
704    ``enc (instruction$MRC c CPn Cop1 Rd CRn CRm Cop2)``));
708    ``enc (instruction$MCR c CPn Cop1 Rd CRn CRm Cop2)``));