diff options
Diffstat (limited to 'src/translation')
-rw-r--r-- | src/translation/HTLgen.v | 4 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 7 |
2 files changed, 8 insertions, 3 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index e0f860e..1cc30c7 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -366,7 +366,9 @@ Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := (Vlit (intToValue n))))*) | Op.Oshru, r1::r2::nil => ret (bop Vshru r1 r2) | Op.Oshruimm n, r::nil => ret (boplit Vshru r n) - | Op.Ororimm n, r::nil => ret (boplit Vror r n) + | Op.Ororimm n, r::nil => error (Errors.msg "Htlgen: Instruction not implemented: Ororimm") + (*ret (Vbinop Vor (boplit Vshru r (Integers.Int.modu n (Integers.Int.repr 32))) + (boplit Vshl r (Integers.Int.sub (Integers.Int.repr 32) (Integers.Int.modu n (Integers.Int.repr 32)))))*) | Op.Oshldimm n, r::nil => ret (Vbinop Vor (boplit Vshl r n) (boplit Vshr r (Integers.Int.sub (Integers.Int.repr 32) n))) | Op.Ocmp c, _ => translate_condition c args | Op.Osel c AST.Tint, r1::r2::rl => diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index da0b662..dd1d967 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -587,6 +587,9 @@ Section CORRECTNESS. - rewrite Heqb in Heqb0. discriminate. - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate. - rewrite Heqb in Heqb0. discriminate. + (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu, + Search Int.repr. + repeat (rewrite Int.unsigned_repr). auto.*) - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2. + unfold translate_eff_addressing in *. repeat (unfold_match H1). destruct v0; inv Heql; rewrite H2; inv H1; repeat eval_correct_tac. @@ -811,7 +814,7 @@ Section CORRECTNESS. inv CONST; constructor; simplify; rewrite AssocMap.gso; auto; lia. - Unshelve. auto. + Unshelve. exact tt. Qed. Hint Resolve transl_inop_correct : htlproof. @@ -863,7 +866,7 @@ Section CORRECTNESS. assert (HPle: Ple res0 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_def; eauto; simpl; auto). unfold Ple in HPle. lia. - Unshelve. trivial. + Unshelve. exact tt. Qed. Hint Resolve transl_iop_correct : htlproof. |