diff --git a/examples/compute/Holmakefile b/examples/compute/Holmakefile index a256daeac..c5d5291e2 100644 --- a/examples/compute/Holmakefile +++ b/examples/compute/Holmakefile @@ -24,5 +24,6 @@ test-compute.exe: test-compute.uo test: test-compute.exe ./test-compute.exe +.PHONY: test EXTRA_CLEANS = test-compute.exe diff --git a/examples/compute/examples/Holmakefile b/examples/compute/examples/Holmakefile index d15396248..035c28eb4 100644 --- a/examples/compute/examples/Holmakefile +++ b/examples/compute/examples/Holmakefile @@ -6,13 +6,14 @@ INCLUDES = $(HOLBADIR)/examples/compute/examples/increment \ $(HOLBADIR)/examples/compute/examples/sum_list \ $(HOLBADIR)/examples/compute/examples/jump_chain -all: $(DEFAULT_TARGETS) test-examples.exe +all: $(DEFAULT_TARGETS) benchmark-examples.exe .PHONY: all -test-examples.exe: test-examples.uo +benchmark-examples.exe: benchmark-examples.uo $(HOLMOSMLC) -o $@ $< -test: test-examples.exe - ./test-examples.exe +benchmark: benchmark-examples.exe + ./benchmark-examples.exe +.PHONY: benchmark -EXTRA_CLEANS = test-examples.exe +EXTRA_CLEANS = benchmark-examples.exe diff --git a/examples/compute/examples/test-examples.sml b/examples/compute/examples/benchmark-examples.sml similarity index 100% rename from examples/compute/examples/test-examples.sml rename to examples/compute/examples/benchmark-examples.sml diff --git a/examples/compute/examples/increment/ex_incrementScript.sml b/examples/compute/examples/increment/ex_incrementScript.sml index 2cdeb23d5..e5290afe3 100644 --- a/examples/compute/examples/increment/ex_incrementScript.sml +++ b/examples/compute/examples/increment/ex_incrementScript.sml @@ -5,7 +5,7 @@ open HolKernel Parse boolLib bossLib; open birTheory; open bir_computeTheory; - +open bir_metaTheory; val _ = new_theory "ex_increment"; diff --git a/examples/compute/ott/bir.ott b/examples/compute/ott/bir.ott index 6d3234350..fde25c55c 100644 --- a/examples/compute/ott/bir.ott +++ b/examples/compute/ott/bir.ott @@ -7,32 +7,82 @@ metavar mmap ::= {{ hol (num |-> num) }} metavar ident ::= {{ hol string }} - {{ com Identifier for variable name }} -metavar word_one ::= - {{ hol word1 }} - {{ tex \mathit{word1} }} - {{ com 1-bit word }} -metavar word_eight ::= + {{ com Identifier }} +indexvar k ::= + {{ hol num }} +grammar +b :: b_ ::= + {{ hol bool }} + {{ com boolean }} +| binpred_op ( bir_binpred , word_one , word_one' ) :: M :: binpred_op_word_one + {{ hol ((bir_binpred_get_oper [[bir_binpred]]) [[word_one]] [[word_one']]) }} +| binpred_op ( bir_binpred , word_eight , word_eight' ) :: M :: binpred_op_word_eight + {{ hol ((bir_binpred_get_oper [[bir_binpred]]) [[word_eight]] [[word_eight']]) }} +| binpred_op ( bir_binpred , word_sixteen , word_sixteen' ) :: M :: binpred_op_word_sixteen + {{ hol ((bir_binpred_get_oper [[bir_binpred]]) [[word_sixteen]] [[word_sixteen']]) }} +| binpred_op ( bir_binpred , word_thirtytwo , word_thirtytwo' ) :: M :: binpred_op_word_thirtytwo + {{ hol ((bir_binpred_get_oper [[bir_binpred]]) [[word_thirtytwo]] [[word_thirtytwo']]) }} +| binpred_op ( bir_binpred , word_sixtyfour , word_sixtyfour' ) :: M :: binpred_op_word_sixtyfour + {{ hol ((bir_binpred_get_oper [[bir_binpred]]) [[word_sixtyfour]] [[word_sixtyfour']]) }} +| binpred_op ( bir_binpred , word_hundredtwentyeight , word_hundredtwentyeight' ) :: M :: binpred_op_word_hundredtwentyeight + {{ hol ((bir_binpred_get_oper [[bir_binpred]]) [[word_hundredtwentyeight]] [[word_hundredtwentyeight']]) }} + +word_one :: word_one_ ::= + {{ hol word1 }} + {{ tex \mathit{word1} }} + {{ com 1-bit word }} +| binexp_op ( bir_binexp , word_one , word_one' ) :: M :: binexp_op + {{ hol ((bir_binexp_get_oper [[bir_binexp]]) [[word_one]] [[word_one']]) }} +| unaryexp_op ( bir_unaryexp , word_one ) :: M :: unaryexp_op + {{ hol ((bir_unaryexp_get_oper [[bir_unaryexp]]) [[word_one]]) }} +| b2w ( b ) :: M :: b2w + {{ hol (bool2w [[b]]) }} + +word_eight :: word_eight_ ::= {{ hol word8 }} {{ tex \mathit{word8} }} {{ com 8-bit word }} -metavar word_sixteen ::= +| binexp_op ( bir_binexp , word_eight , word_eight' ) :: M :: binexp_op + {{ hol ((bir_binexp_get_oper [[bir_binexp]]) [[word_eight]] [[word_eight']]) }} +| unaryexp_op ( bir_unaryexp , word_eight ) :: M :: unaryexp_op + {{ hol ((bir_unaryexp_get_oper [[bir_unaryexp]]) [[word_eight]]) }} + +word_sixteen :: word_sixteen_ ::= {{ hol word16 }} {{ tex \mathit{word16} }} {{ com 16-bit word }} -metavar word_thirtytwo ::= +| binexp_op ( bir_binexp , word_sixteen , word_sixteen' ) :: M :: binexp_op + {{ hol ((bir_binexp_get_oper [[bir_binexp]]) [[word_sixteen]] [[word_sixteen']]) }} +| unaryexp_op ( bir_unaryexp , word_sixteen ) :: M :: unaryexp_op + {{ hol ((bir_unaryexp_get_oper [[bir_unaryexp]]) [[word_sixteen]]) }} + +word_thirtytwo :: word_thirtytwo_ ::= {{ hol word32 }} {{ tex \mathit{word32} }} {{ com 32-bit word }} -metavar word_sixtyfour ::= +| binexp_op ( bir_binexp , word_thirtytwo , word_thirtytwo' ) :: M :: binexp_op + {{ hol ((bir_binexp_get_oper [[bir_binexp]]) [[word_thirtytwo]] [[word_thirtytwo']]) }} +| unaryexp_op ( bir_unaryexp , word_thirtytwo ) :: M :: unaryexp_op + {{ hol ((bir_unaryexp_get_oper [[bir_unaryexp]]) [[word_thirtytwo]]) }} + +word_sixtyfour :: word_sixtyfour_ ::= {{ hol word64 }} {{ tex \mathit{word64} }} {{ com 64-bit word }} -metavar word_hundredtwentyeight ::= +| binexp_op ( bir_binexp , word_sixtyfour , word_sixtyfour' ) :: M :: binexp_op + {{ hol ((bir_binexp_get_oper [[bir_binexp]]) [[word_sixtyfour]] [[word_sixtyfour']]) }} +| unaryexp_op ( bir_unaryexp , word_sixtyfour ) :: M :: unaryexp_op + {{ hol ((bir_unaryexp_get_oper [[bir_unaryexp]]) [[word_sixtyfour]]) }} + +word_hundredtwentyeight :: word_hundredtwentyeight_ ::= {{ hol word128 }} {{ tex \mathit{word128} }} {{ com 128-bit word }} -grammar +| binexp_op ( bir_binexp , word_hundredtwentyeight , word_hundredtwentyeight' ) :: M :: binexp_op + {{ hol ((bir_binexp_get_oper [[bir_binexp]]) [[word_hundredtwentyeight]] [[word_hundredtwentyeight']]) }} +| unaryexp_op ( bir_unaryexp , word_hundredtwentyeight ) :: M :: unaryexp_op + {{ hol ((bir_unaryexp_get_oper [[bir_unaryexp]]) [[word_hundredtwentyeight]]) }} + bir_imm_t, bir_imm :: '' ::= {{ com immediates }} | Imm_one ( word_one ) :: :: Imm1 @@ -61,14 +111,18 @@ bir_endian_t, bir_endian :: BEnd_ ::= bir_val_t, bir_val :: BVal_ ::= {{ com values for evaluation relation }} -| Val_Imm ( bir_imm ) :: :: Imm -| Val_Mem ( bir_immtype , bir_immtype' , mmap ) :: :: Mem +| ValImm ( bir_imm ) :: :: Imm +| ValMem ( bir_immtype , bir_immtype' , mmap ) :: :: Mem {{ com address type / value type }} +| birT :: M :: birT + {{ hol birT }} +| birF :: M :: birF + {{ hol birF }} bir_type_t, bir_type :: BType_ ::= {{ com general typing }} -| Type_Imm ( bir_immtype ) :: :: Imm -| Type_Mem ( bir_immtype , bir_immtype' ) :: :: Mem +| TypeImm ( bir_immtype ) :: :: Imm +| TypeMem ( bir_immtype , bir_immtype' ) :: :: Mem | type_of_bir_val ( bir_val ) :: M :: type_of_bir_val {{ hol (type_of_bir_val [[bir_val]]) }} @@ -107,20 +161,53 @@ bir_exp_t, bir_exp :: BExp_ ::= {{ com Memory value / Address Value (Imm) / Endian / Value to store }} terminals :: terminals_ ::= -| Imm_one :: :: imm_one {{ tex \mathbf{Imm1} }} -| Imm_eight :: :: imm_eight {{ tex \mathbf{Imm8} }} -| Imm_sixteen :: :: imm_sixteen {{ tex \mathbf{Imm16} }} -| Imm_thirtytwo :: :: imm_thirtytwo {{ tex \mathbf{Imm32} }} -| Imm_sixtyfour :: :: imm_sixtyfour {{ tex \mathbf{Imm64} }} -| Imm_hundredtwentyeight :: :: imm_hundredtwentyeight {{ tex \mathbf{Imm128} }} +| Imm_one :: :: imm_one {{ tex \mathsf{Imm1} }} +| Imm_eight :: :: imm_eight {{ tex \mathsf{Imm8} }} +| Imm_sixteen :: :: imm_sixteen {{ tex \mathsf{Imm16} }} +| Imm_thirtytwo :: :: imm_thirtytwo {{ tex \mathsf{Imm32} }} +| Imm_sixtyfour :: :: imm_sixtyfour {{ tex \mathsf{Imm64} }} +| Imm_hundredtwentyeight :: :: imm_hundredtwentyeight {{ tex \mathsf{Imm128} }} | Bit_one :: :: Bit_one {{ tex \mathbf{Bit1} }} | Bit_eight :: :: Bit_eight {{ tex \mathbf{Bit8} }} | Bit_sixteen :: :: Bit_sixteen {{ tex \mathbf{Bit16} }} | Bit_thirtytwo :: :: Bit_thirtytwo {{ tex \mathbf{Bit32} }} | Bit_sixtyfour :: :: Bit_sixtyfour {{ tex \mathbf{Bit64} }} | Bit_hundredtwentyeight :: :: Bit_hundredtwentyeight {{ tex \mathbf{Bit128} }} +| ValImm :: :: ValImm {{ tex \mathsf{ValImm} }} +| ValMem :: :: ValMem {{ tex \mathsf{ValMem} }} +| TypeImm :: :: TypeImm {{ tex \mathsf{TypeImm} }} +| TypeMem :: :: TypeMem {{ tex \mathsf{TypeMem} }} +| Var :: :: Var {{ tex \mathsf{Var} }} +| Const :: :: Const {{ tex \mathsf{Const} }} +| MemConst :: :: MemConst {{ tex \mathsf{MemConst} }} +| Den :: :: Den {{ tex \mathsf{Den} }} +| BinExp :: :: BinExp {{ tex \mathsf{BinExp} }} +| UnaryExp :: :: UnaryExp {{ tex \mathsf{UnaryExp} }} +| BinPred :: :: BinPred {{ tex \mathsf{BinPred} }} +| IfThenElse :: :: IfThenElse {{ tex \mathsf{IfThenElse} }} +| Load :: :: Load {{ tex \mathsf{Load} }} +| Store :: :: Store {{ tex \mathsf{Store} }} +| bir_env_lookup_rel :: :: bir_env_lookup_rel {{ tex \mathit{bir\_env\_lookup\_rel} }} +| size_of_bir_immtype :: :: size_of_bir_immtype {{ tex \mathit{size\_of\_bir\_immtype} }} +| type_of_bir_imm :: :: type_of_bir_imm {{ tex \mathit{type\_of\_bir\_imm} }} +| type_of_bir_val :: :: type_of_bir_val {{ tex \mathit{type\_of\_bir\_val} }} +| binexp_op :: :: binexp_op {{ tex \mathit{binexp\_op} }} +| unaryexp_op :: :: unaryexp_op {{ tex \mathit{unaryexp\_op} }} +| binpred_op :: :: binpred_op {{ tex \mathit{binpred\_op} }} | |- :: :: vdash {{ tex \vdash }} | ~> :: :: leadsto {{ tex \leadsto }} +| <= :: :: leq {{ tex \leq }} +| ** :: :: pow {{ tex \mathit{**} }} +| Label :: :: Label {{ tex \mathsf{Label} }} +| Address :: :: Address {{ tex \mathsf{Address} }} +| Exp :: :: Exp {{ tex \mathsf{Exp} }} +| Assign :: :: Assign {{ tex \mathsf{Assign} }} +| Jmp :: :: Jmp {{ tex \mathsf{Jmp} }} +| CJmp :: :: CJmp {{ tex \mathsf{CJmp} }} +| Basic :: :: Basic {{ tex \mathsf{Basic} }} +| End :: :: End {{ tex \mathsf{End} }} +| BirProgram :: :: BirProgram {{ tex \mathsf{BirProgram} }} +| JumpOutside :: :: JumpOutside {{ tex \mathsf{JumpOutside} }} embed {{ hol (* Booleans *) @@ -141,19 +228,6 @@ Definition birF_def: birF = BVal_Imm (Imm1 0w) End -(* Correction Theorems of boolean functions *) -Theorem bool2b_T_eq_birT: - BVal_Imm (bool2b T) = birT -Proof - rw [bool2b_def, bool2w_def, birT_def] -QED - -Theorem bool2b_F_eq_birF: - BVal_Imm (bool2b F) = birF -Proof - rw [bool2b_def, bool2w_def, birF_def] -QED - (* Utility functions *) Definition bir_dest_bool_val_def: (bir_dest_bool_val (BVal_Imm (Imm1 w)) = SOME (w = 1w)) /\ @@ -192,64 +266,6 @@ Definition bir_env_update_def: bir_env_update ((BEnv env):bir_var_environment_t) (BVar id) v = BEnv ((id =+ SOME v) env) End -Theorem bir_env_lookup_empty: - !var v. ~(bir_env_lookup_rel bir_empty_env var v) -Proof - Cases_on `var` >> - rw [bir_empty_env_def, bir_env_lookup_rel_def] -QED - -Theorem bir_env_lookup_rel_update: - !env var v. bir_env_lookup_rel (bir_env_update env var v) var v -Proof - Cases_on `var` >> Cases_on `env` >> - rw [bir_env_update_def, bir_env_lookup_rel_def] -QED - -Theorem bir_env_lookup_update: - !env var v. bir_env_lookup (bir_env_update env var v) var = SOME v -Proof - rpt gen_tac >> - Cases_on `var` >> Cases_on `env` >> - rw [bir_env_update_def, bir_env_lookup_def] -QED - -Theorem bir_env_lookup_update_neq: - !env var1 var2 v. - var1 <> var2 ==> - bir_env_lookup (bir_env_update env var1 v) var2 = bir_env_lookup env var2 -Proof - Cases_on `var1` >> Cases_on `var2` >> - rw [fetch "-" "bir_var_t_11"] >> - Cases_on `env` >> - simp [bir_env_update_def] >> - rw [bir_env_lookup_def] >> - EVAL_TAC >> - metis_tac [] -QED - -(* Lookup and relation are the same *) -Theorem bir_env_lookup_eq_rel: - !env var v. bir_env_lookup_rel env var v <=> bir_env_lookup env var = SOME v -Proof - rpt strip_tac >> - Cases_on `env` >> - Cases_on `var` >> - rw [bir_env_lookup_def, bir_env_lookup_rel_def] -QED - - -(* Injective *) -Theorem bir_env_lookup_rel_inj: - !env var v1 v2. - bir_env_lookup_rel env var v1 ==> - bir_env_lookup_rel env var v2 ==> - v1 = v2 -Proof - Cases_on `env` >> Cases_on `var` >> - simp [bir_env_lookup_rel_def] -QED - (* --------- Typing ------- *) (* Gives the size of an immediate as a number *) @@ -277,6 +293,24 @@ Definition type_of_bir_val_def: (type_of_bir_val (BVal_Imm imm) = (BType_Imm (type_of_bir_imm imm))) /\ (type_of_bir_val (BVal_Mem aty vty mmap) = (BType_Mem aty vty) ) End + +(* Gets the operator for a given binary operation *) +Definition bir_binexp_get_oper_def: + (bir_binexp_get_oper BIExp_And = word_and) /\ + (bir_binexp_get_oper BIExp_Plus = word_add) +End + +(* Gets the operator for a given unary operation *) +Definition bir_unaryexp_get_oper_def: + (bir_unaryexp_get_oper BIExp_Not = word_1comp) /\ + (bir_unaryexp_get_oper BIExp_ChangeSign = word_2comp) +End + +(* Gets the operator for a given binary predicate *) +Definition bir_binpred_get_oper_def: + (bir_binpred_get_oper BIExp_Equal = $=) /\ + (bir_binpred_get_oper BIExp_LessThan = word_lo) +End }} metavar bir_var_environment_t, bir_var_environment, env ::= @@ -292,16 +326,6 @@ formula :: formula_ ::= {{ hol ([[n]] = [[n']]) }} | n '<=' n' :: M :: n_lt {{ hol ([[n]] <= [[n']]) }} -%| bir_binexp bir_imm1 bir_imm2 ~> bir_imm :: M :: bir_eval_binexp_imm -% {{ hol (bir_eval_binexp_imm [[bir_imm1]] [[bir_imm2]] [[bir_imm]]) }} -| bir_binexp bir_val1 bir_val2 ~> bir_val :: M :: bir_eval_binexp - {{ hol (bir_eval_binexp [[bir_binexp]] [[bir_val1]] [[bir_val2]] [[bir_val]]) }} -| bir_unaryexp bir_val ~> bir_val' :: M :: bir_eval_unaryexp - {{ hol (bir_eval_unaryexp [[bir_unaryexp]] [[bir_val]] [[bir_val']]) }} -| bir_binpred bir_val1 bir_val2 ~> bir_val :: M :: bir_eval_binpred - {{ hol (bir_eval_binpred [[bir_binpred]] [[bir_val1]] [[bir_val2]] [[bir_val]]) }} -| bir_val bir_val1 bir_val2 ~> bir_val' :: M :: bir_eval_ifthenelse - {{ hol (bir_eval_ifthenelse [[bir_val]] [[bir_val1]] [[bir_val2]] [[bir_val']]) }} | bir_val1 bir_val2 bir_endian bir_immtype ~> bir_val3 :: M :: bir_eval_load {{ hol (bir_eval_load [[bir_val1]] [[bir_val2]] [[bir_endian]] [[bir_immtype]] [[bir_val3]]) }} | bir_val1 bir_val2 bir_endian bir_val3 ~> bir_val :: M :: bir_eval_store @@ -313,7 +337,7 @@ n :: n_ ::= {{ hol ([[n]] MOD [[n']]) }} | n DIV n' :: M :: div {{ hol ([[n]] DIV [[n']]) }} -| 2 ^ n :: M :: two_pow +| 2 ** n :: M :: two_pow {{ hol (2**[[n]]) }} | 0 :: M :: zero {{ hol 0 }} @@ -329,462 +353,206 @@ defn bir_var_environment |- bir_exp : bir_type :: :: type_of_bir_exp :: Type_BExp_ {{ com typing relation for BIR expressions }} by - --------------- :: Const - env |- Const(bir_imm) : Type_Imm(type_of_bir_imm(bir_imm)) + --------------------------------------------------------- :: Const + env |- Const(bir_imm) : TypeImm(type_of_bir_imm(bir_imm)) - ----------------- :: MemConst - env |- MemConst(bir_immtype1,bir_immtype2,mmap) : Type_Mem(bir_immtype1,bir_immtype2) + ------------------------------------------------------------------------------------- :: MemConst + env |- MemConst(bir_immtype1,bir_immtype2,mmap) : TypeMem(bir_immtype1,bir_immtype2) bir_env_lookup_rel(env,bir_var,bir_val) - -------------------------------------- :: Den + ---------------------------------------------- :: Den env |- Den(bir_var) : type_of_bir_val(bir_val) - env |- bir_exp1 : Type_Imm(bir_immtype) - env |- bir_exp2 : Type_Imm(bir_immtype) - ------------------------------ :: BinExp - env |- BinExp(bir_binexp,bir_exp1,bir_exp2) : Type_Imm(bir_immtype) + env |- bir_exp1 : TypeImm(bir_immtype) + env |- bir_exp2 : TypeImm(bir_immtype) + ------------------------------------------------------------------ :: BinExp + env |- BinExp(bir_binexp,bir_exp1,bir_exp2) : TypeImm(bir_immtype) - env |- bir_exp : Type_Imm(bir_immtype) - -------------------------------------- :: UnaryExp - env |- UnaryExp(bir_unaryexp,bir_exp) : Type_Imm(bir_immtype) + env |- bir_exp : TypeImm(bir_immtype) + ------------------------------------------------------------ :: UnaryExp + env |- UnaryExp(bir_unaryexp,bir_exp) : TypeImm(bir_immtype) - env |- bir_exp1 : Type_Imm(bir_immtype) - env |- bir_exp2 : Type_Imm(bir_immtype) - ------------------------------ :: BinPred - env |- BinPred(bir_binpred,bir_exp1,bir_exp2) : Type_Imm(Bit_one) + env |- bir_exp1 : TypeImm(bir_immtype) + env |- bir_exp2 : TypeImm(bir_immtype) + ----------------------------------------------------------------- :: BinPred + env |- BinPred(bir_binpred,bir_exp1,bir_exp2) : TypeImm(Bit_one) env |- bir_exp1 : bir_type env |- bir_exp2 : bir_type - env |- bir_exp : Type_Imm(Bit_one) - ------------------------------ :: IfThenElse + env |- bir_exp : TypeImm(Bit_one) + ------------------------------------------------------- :: IfThenElse env |- IfThenElse(bir_exp,bir_exp1,bir_exp2) : bir_type - env |- bir_exp1 : Type_Mem(bir_immtype1,bir_immtype2) - env |- bir_exp2 : Type_Imm(bir_immtype1) + env |- bir_exp1 : TypeMem(bir_immtype1,bir_immtype2) + env |- bir_exp2 : TypeImm(bir_immtype1) size_of_bir_immtype(bir_immtype) MOD size_of_bir_immtype(bir_immtype2) = 0 - size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2^size_of_bir_immtype(bir_immtype1) + size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2**size_of_bir_immtype(bir_immtype1) size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) = 1 - ----------------------------------- :: Load_NoEndian - env |- Load(bir_exp1,bir_exp2,NoEndian,bir_immtype) : Type_Imm(bir_immtype) + -------------------------------------------------------------------------- :: Load_NoEndian + env |- Load(bir_exp1,bir_exp2,NoEndian,bir_immtype) : TypeImm(bir_immtype) - env |- bir_exp1 : Type_Mem(bir_immtype1,bir_immtype2) - env |- bir_exp2 : Type_Imm(bir_immtype1) + env |- bir_exp1 : TypeMem(bir_immtype1,bir_immtype2) + env |- bir_exp2 : TypeImm(bir_immtype1) size_of_bir_immtype(bir_immtype) MOD size_of_bir_immtype(bir_immtype2) = 0 - size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2^size_of_bir_immtype(bir_immtype1) - -------- :: Load_BigEndian - env |- Load(bir_exp1,bir_exp2,BigEndian,bir_immtype) : Type_Imm(bir_immtype) + size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2**size_of_bir_immtype(bir_immtype1) + --------------------------------------------------------------------------- :: Load_BigEndian + env |- Load(bir_exp1,bir_exp2,BigEndian,bir_immtype) : TypeImm(bir_immtype) - env |- bir_exp1 : Type_Mem(bir_immtype1,bir_immtype2) - env |- bir_exp2 : Type_Imm(bir_immtype1) + env |- bir_exp1 : TypeMem(bir_immtype1,bir_immtype2) + env |- bir_exp2 : TypeImm(bir_immtype1) size_of_bir_immtype(bir_immtype) MOD size_of_bir_immtype(bir_immtype2) = 0 - size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2^size_of_bir_immtype(bir_immtype1) - -------- :: Load_LittleEndian - env |- Load(bir_exp1,bir_exp2,LittleEndian,bir_immtype) : Type_Imm(bir_immtype) + size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2**size_of_bir_immtype(bir_immtype1) + ------------------------------------------------------------------------------ :: Load_LittleEndian + env |- Load(bir_exp1,bir_exp2,LittleEndian,bir_immtype) : TypeImm(bir_immtype) - env |- bir_exp1 : Type_Mem(bir_immtype1,bir_immtype2) - env |- bir_exp2 : Type_Imm(bir_immtype1) - env |- bir_exp3 : Type_Imm(bir_immtype) + env |- bir_exp1 : TypeMem(bir_immtype1,bir_immtype2) + env |- bir_exp2 : TypeImm(bir_immtype1) + env |- bir_exp3 : TypeImm(bir_immtype) size_of_bir_immtype(bir_immtype) MOD size_of_bir_immtype(bir_immtype2) = 0 - size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2^size_of_bir_immtype(bir_immtype1) + size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2**size_of_bir_immtype(bir_immtype1) size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) = 1 ------------------------------------------------------------ :: Store_NoEndian - env |- Store(bir_exp1,bir_exp2,NoEndian,bir_exp3) : Type_Mem(bir_immtype1,bir_immtype2) + env |- Store(bir_exp1,bir_exp2,NoEndian,bir_exp3) : TypeMem(bir_immtype1,bir_immtype2) - env |- bir_exp1 : Type_Mem(bir_immtype1,bir_immtype2) - env |- bir_exp2 : Type_Imm(bir_immtype1) - env |- bir_exp3 : Type_Imm(bir_immtype) + env |- bir_exp1 : TypeMem(bir_immtype1,bir_immtype2) + env |- bir_exp2 : TypeImm(bir_immtype1) + env |- bir_exp3 : TypeImm(bir_immtype) size_of_bir_immtype(bir_immtype) MOD size_of_bir_immtype(bir_immtype2) = 0 - size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2^size_of_bir_immtype(bir_immtype1) + size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2**size_of_bir_immtype(bir_immtype1) ------------------------------------------------------------ :: Store_BigEndian - env |- Store(bir_exp1,bir_exp2,BigEndian,bir_exp3) : Type_Mem(bir_immtype1,bir_immtype2) + env |- Store(bir_exp1,bir_exp2,BigEndian,bir_exp3) : TypeMem(bir_immtype1,bir_immtype2) - env |- bir_exp1 : Type_Mem(bir_immtype1,bir_immtype2) - env |- bir_exp2 : Type_Imm(bir_immtype1) - env |- bir_exp3 : Type_Imm(bir_immtype) + env |- bir_exp1 : TypeMem(bir_immtype1,bir_immtype2) + env |- bir_exp2 : TypeImm(bir_immtype1) + env |- bir_exp3 : TypeImm(bir_immtype) size_of_bir_immtype(bir_immtype) MOD size_of_bir_immtype(bir_immtype2) = 0 - size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2^size_of_bir_immtype(bir_immtype1) - ------------------------------------------------------------ :: Store_LittleEndian - env |- Store(bir_exp1,bir_exp2,LittleEndian,bir_exp3) : Type_Mem(bir_immtype1,bir_immtype2) - -embed {{ hol + size_of_bir_immtype(bir_immtype) DIV size_of_bir_immtype(bir_immtype2) <= 2**size_of_bir_immtype(bir_immtype1) + ------------------------------------------------------------------------------------------- :: Store_LittleEndian + env |- Store(bir_exp1,bir_exp2,LittleEndian,bir_exp3) : TypeMem(bir_immtype1,bir_immtype2) -Definition is_exp_well_typed_def: - is_exp_well_typed env exp = ?ty. type_of_bir_exp env exp ty -End +defns + bir_eval_binexp_imm :: '' ::= -(* 1 bit values are booleans *) -Theorem bit1_is_boolean: - !v. type_of_bir_val v = (BType_Imm Bit1) ==> (v = birT \/ v = birF) -Proof - Cases_on `v` >> - Cases_on `b` >> - rw [birT_def, birF_def, type_of_bir_val_def, type_of_bir_imm_def] >> - Cases_on `c` >> - fs [dimword_1] -QED +defn + bir_binexp_t bir_imm_t bir_imm_t' ~> bir_imm_t'' :: :: bir_eval_binexp_imm :: Eval_BinExp_Imm_ + {{ com evaluation of a binary expression of two immediates }} by -(* Gets the operator for a given binary operation *) -Definition bir_binexp_get_oper_def: - (bir_binexp_get_oper BIExp_And = word_and) /\ - (bir_binexp_get_oper BIExp_Plus = word_add) -End -(* Evaluates a binary expression of two immediates *) -Inductive bir_eval_binexp_imm: - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm1 w1) (Imm1 w2) (Imm1 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm8 w1) (Imm8 w2) (Imm8 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm16 w1) (Imm16 w2) (Imm16 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm32 w1) (Imm32 w2) (Imm32 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm64 w1) (Imm64 w2) (Imm64 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm128 w1) (Imm128 w2) (Imm128 ((bir_binexp_get_oper binexp) w1 w2))) -End + -------------------------------------------------------- :: One + bir_binexp Imm_one(word_one) Imm_one(word_one') ~> Imm_one(binexp_op(bir_binexp,word_one,word_one')) -(* Evaluates a general binary expression with values as parameters *) -Definition bir_eval_binexp_def: - (bir_eval_binexp binexp (BVal_Imm imm1) (BVal_Imm imm2) (BVal_Imm imm) = - (bir_eval_binexp_imm binexp imm1 imm2 imm)) /\ - (bir_eval_binexp _ _ _ _ = F) -End + ------------------------------------------------------------------------------------------------------------------ :: Eight + bir_binexp Imm_eight(word_eight) Imm_eight(word_eight') ~> Imm_eight(binexp_op(bir_binexp,word_eight,word_eight')) -(* Computes a binary expression of two immediates *) -Definition bir_compute_binexp_imm_def: - (bir_compute_binexp_imm BIExp_And (Imm1 w1) (Imm1 w2) = SOME (Imm1 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm8 w1) (Imm8 w2) = SOME (Imm8 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm16 w1) (Imm16 w2) = SOME (Imm16 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm32 w1) (Imm32 w2) = SOME (Imm32 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm64 w1) (Imm64 w2) = SOME (Imm64 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm128 w1) (Imm128 w2) = SOME (Imm128 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm1 w1) (Imm1 w2) = SOME (Imm1 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm8 w1) (Imm8 w2) = SOME (Imm8 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm16 w1) (Imm16 w2) = SOME (Imm16 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm32 w1) (Imm32 w2) = SOME (Imm32 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm64 w1) (Imm64 w2) = SOME (Imm64 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm128 w1) (Imm128 w2) = SOME (Imm128 (word_add w1 w2))) /\ - (bir_compute_binexp_imm binexp _ _ = NONE) -End + ------------------------------------------------------------------------------------------------------------------ :: Sixteen + bir_binexp Imm_sixteen(word_sixteen) Imm_sixteen(word_sixteen') ~> Imm_sixteen(binexp_op(bir_binexp,word_sixteen,word_sixteen')) + ------------------------------------------------------------------------------------------------------------------ :: Thirtytwo + bir_binexp Imm_thirtytwo(word_thirtytwo) Imm_thirtytwo(word_thirtytwo') ~> Imm_thirtytwo(binexp_op(bir_binexp,word_thirtytwo,word_thirtytwo')) -(* Computes a general binary expression with values as parameters *) -Definition bir_compute_binexp_def: - (bir_compute_binexp binexp (SOME (BVal_Imm imm1)) (SOME (BVal_Imm imm2)) = - val_from_imm_option (bir_compute_binexp_imm binexp imm1 imm2)) /\ - (bir_compute_binexp _ _ _ = NONE) -End + ------------------------------------------------------------------------------------------------------------------ :: Sixtyfour + bir_binexp Imm_sixtyfour(word_sixtyfour) Imm_sixtyfour(word_sixtyfour') ~> Imm_sixtyfour(binexp_op(bir_binexp,word_sixtyfour,word_sixtyfour')) -(* Eval and compute are similar *) -Theorem bir_eval_binexp_eq_compute_binexp: - !binexp v1 v2 v. bir_eval_binexp binexp v1 v2 v <=> - bir_compute_binexp binexp (SOME v1) (SOME v2) = SOME v -Proof - Cases_on `binexp` >> - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - rw [bir_eval_binexp_def, bir_compute_binexp_def] >> - rw [bir_eval_binexp_imm_cases, bir_compute_binexp_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> - rw [bir_compute_binexp_imm_def, fetch "-" "bir_imm_t_nchotomy", bir_binexp_get_oper_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - - -(* If the operands are typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_binexp: - !binexp v1 v2 ty. - ((type_of_bir_val v1 = BType_Imm ty) /\ (type_of_bir_val v2 = BType_Imm ty)) ==> - ?v. bir_eval_binexp binexp v1 v2 v -Proof - Cases_on `binexp` >> - Cases_on `v1` >> Cases_on `v2` >> - Cases_on `b` >> Cases_on `b'` >> - rw [bir_eval_binexp_eq_compute_binexp] >> - rw [bir_compute_binexp_def, bir_compute_binexp_imm_def] >> - rw [val_from_imm_option_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] -QED - - -(* Type conservation Theorem *) -Theorem bir_eval_binexp_keep_type: - !binexp v1 v2 v ty. - bir_eval_binexp binexp v1 v2 v ==> - ((type_of_bir_val v1 = ty /\ type_of_bir_val v2 = ty) <=> - type_of_bir_val v = ty) -Proof - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> - rw [type_of_bir_val_def, bir_eval_binexp_def, type_of_bir_imm_def, bir_eval_binexp_imm_cases] -QED + ------------------------------------------------------------------------------------------------------------------ :: Hundredtwentyeight + bir_binexp Imm_hundredtwentyeight(word_hundredtwentyeight) Imm_hundredtwentyeight(word_hundredtwentyeight') ~> Imm_hundredtwentyeight(binexp_op(bir_binexp,word_hundredtwentyeight,word_hundredtwentyeight')) -(* Gets the operator for a given unary operation *) -Definition bir_unaryexp_get_oper_def: - (bir_unaryexp_get_oper BIExp_Not = word_1comp) /\ - (bir_unaryexp_get_oper BIExp_ChangeSign = word_2comp) -End +defns + bir_eval_unaryexp_imm :: '' ::= +defn + bir_unaryexp_t bir_imm_t ~> bir_imm_t' :: :: bir_eval_unaryexp_imm :: Eval_UnaryExp_Imm_ + {{ com evaluation of a unary expression of one immediate }} by -(* Evaluates a binary expression of an immediate *) -Inductive bir_eval_unaryexp_imm: - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm1 w1) (Imm1 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm8 w1) (Imm8 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm16 w1) (Imm16 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm32 w1) (Imm32 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm64 w1) (Imm64 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm128 w1) (Imm128 ((bir_unaryexp_get_oper unaryexp) w1))) -End + --------------------------------------------------------------------------- :: One + bir_unaryexp Imm_one(word_one) ~> Imm_one(unaryexp_op(bir_unaryexp,word_one)) + --------------------------------------------------------------------------- :: Eight + bir_unaryexp Imm_eight(word_eight) ~> Imm_eight(unaryexp_op(bir_unaryexp,word_eight)) -(* Evaluates a general unary expression with values as parameters *) -Definition bir_eval_unaryexp_def: - (bir_eval_unaryexp unaryexp (BVal_Imm imm1) (BVal_Imm imm) = - (bir_eval_unaryexp_imm unaryexp imm1 imm)) /\ - (bir_eval_unaryexp _ _ _ = F) -End + --------------------------------------------------------------------------- :: Sixteen + bir_unaryexp Imm_sixteen(word_sixteen) ~> Imm_sixteen(unaryexp_op(bir_unaryexp,word_sixteen)) -(* Computes a binary expression of an immediate *) -Definition bir_compute_unaryexp_imm_def: - (bir_compute_unaryexp_imm BIExp_Not (Imm1 w1) = SOME (Imm1 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm8 w1) = SOME (Imm8 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm16 w1) = SOME (Imm16 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm32 w1) = SOME (Imm32 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm64 w1) = SOME (Imm64 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm128 w1) = SOME (Imm128 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm1 w1) = SOME (Imm1 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm8 w1) = SOME (Imm8 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm16 w1) = SOME (Imm16 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm32 w1) = SOME (Imm32 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm64 w1) = SOME (Imm64 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm128 w1) = SOME (Imm128 (word_2comp w1))) -End + --------------------------------------------------------------------------- :: Thirtytwo + bir_unaryexp Imm_thirtytwo(word_thirtytwo) ~> Imm_thirtytwo(unaryexp_op(bir_unaryexp,word_thirtytwo)) -(* Computes Unary expression *) -Definition bir_compute_unaryexp_def: - (bir_compute_unaryexp unaryexp (SOME (BVal_Imm imm1)) = - val_from_imm_option (bir_compute_unaryexp_imm unaryexp imm1)) /\ - (bir_compute_unaryexp _ _ = NONE) -End + --------------------------------------------------------------------------- :: Sixtyfour + bir_unaryexp Imm_sixtyfour(word_sixtyfour) ~> Imm_sixtyfour(unaryexp_op(bir_unaryexp,word_sixtyfour)) -(* Eval and Compute are similar *) -Theorem bir_eval_unaryexp_eq_compute_unaryexp: - !unaryexp v1 v. bir_eval_unaryexp unaryexp v1 v <=> - bir_compute_unaryexp unaryexp (SOME v1) = SOME v -Proof - Cases_on `unaryexp` >> - Cases_on `v1` >> Cases_on `v` >> - rw [bir_eval_unaryexp_def, bir_compute_unaryexp_def] >> - rw [bir_eval_unaryexp_imm_cases, bir_compute_unaryexp_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> - rw [bir_compute_unaryexp_imm_def, fetch "-" "bir_imm_t_nchotomy", bir_unaryexp_get_oper_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - - -(* Unary_exp always evaluates *) -Theorem type_of_bir_val_imp_bir_eval_unaryexp: - !unaryexp v ty. - (type_of_bir_val v = BType_Imm ty) ==> - ?v'. bir_eval_unaryexp unaryexp v v' -Proof - Cases_on `unaryexp` >> - Cases_on `v` >> - Cases_on `b` >> - rw [bir_eval_unaryexp_eq_compute_unaryexp, type_of_bir_val_def] >> - rw [bir_compute_unaryexp_def, bir_compute_unaryexp_imm_def] >> - rw [val_from_imm_option_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] -QED - -(* Type conservation theorem *) -Theorem bir_eval_unaryexp_keep_type: - !unaryexp v1 v2 ty. - bir_eval_unaryexp unaryexp v1 v2 ==> - (type_of_bir_val v1 = type_of_bir_val v2) -Proof - Cases_on `v1` >> Cases_on `v2` >> - Cases_on `b` >> Cases_on `b'` >> - rw [type_of_bir_val_def, bir_eval_unaryexp_def, type_of_bir_imm_def, bir_eval_unaryexp_imm_cases] -QED + --------------------------------------------------------------------------- :: Hundredtwentyeight + bir_unaryexp Imm_hundredtwentyeight(word_hundredtwentyeight) ~> Imm_hundredtwentyeight(unaryexp_op(bir_unaryexp,word_hundredtwentyeight)) -(* Gets the operator for a given binary predicate *) -Definition bir_binpred_get_oper_def: - (bir_binpred_get_oper BIExp_Equal = $=) /\ - (bir_binpred_get_oper BIExp_LessThan = word_lo) -End +defns + bir_eval_binpred_imm :: '' ::= +defn + bir_binpred_t bir_imm_t bir_imm_t' ~> b :: :: bir_eval_binpred_imm :: Eval_BinPred_Imm_ + {{ com evaluation of a binary predicate of two immediates }} by -(* Evaluates a binary predicate of two immediates *) -Inductive bir_eval_binpred_imm: - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm1 w1) (Imm1 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm8 w1) (Imm8 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm16 w1) (Imm16 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm32 w1) (Imm32 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm64 w1) (Imm64 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm128 w1) (Imm128 w2) ((bir_binpred_get_oper binpred) w1 w2)) -End + -------------------------------------------------------- :: One + bir_binpred Imm_one(word_one) Imm_one(word_one') ~> binpred_op(bir_binpred,word_one,word_one') + ------------------------------------------------------------------------------------------------------------------ :: Eight + bir_binpred Imm_eight(word_eight) Imm_eight(word_eight') ~> binpred_op(bir_binpred,word_eight,word_eight') -(* Evaluates a general binary predicate with values as parameters *) -Inductive bir_eval_binpred: - (!binpred imm1 imm2 b. - (bir_eval_binpred_imm binpred imm1 imm2 b) ==> - (bir_eval_binpred binpred (BVal_Imm imm1) (BVal_Imm imm2) (BVal_Imm (bool2b b)))) -End + ------------------------------------------------------------------------------------------------------------------ :: Sixteen + bir_binpred Imm_sixteen(word_sixteen) Imm_sixteen(word_sixteen') ~> binpred_op(bir_binpred,word_sixteen,word_sixteen') -(* Computes a binary predicate of two immediates *) -Definition bir_compute_binpred_imm_def: - (bir_compute_binpred_imm BIExp_Equal (Imm1 w1) (Imm1 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm8 w1) (Imm8 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm16 w1) (Imm16 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm32 w1) (Imm32 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm64 w1) (Imm64 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm128 w1) (Imm128 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm1 w1) (Imm1 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm8 w1) (Imm8 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm16 w1) (Imm16 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm32 w1) (Imm32 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm64 w1) (Imm64 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm128 w1) (Imm128 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm binpred _ _ = F) -End + ------------------------------------------------------------------------------------------------------------------ :: Thirtytwo + bir_binpred Imm_thirtytwo(word_thirtytwo) Imm_thirtytwo(word_thirtytwo') ~> binpred_op(bir_binpred,word_thirtytwo,word_thirtytwo') + ------------------------------------------------------------------------------------------------------------------ :: Sixtyfour + bir_binpred Imm_sixtyfour(word_sixtyfour) Imm_sixtyfour(word_sixtyfour') ~> binpred_op(bir_binpred,word_sixtyfour,word_sixtyfour') -(* Computes a general binary predicate with values as parameters *) -Definition bir_compute_binpred_def: - (bir_compute_binpred binpred (SOME (BVal_Imm imm1)) (SOME (BVal_Imm imm2)) = - SOME (BVal_Imm (bool2b (bir_compute_binpred_imm binpred imm1 imm2)))) /\ - (bir_compute_binpred _ _ _ = NONE) -End + ------------------------------------------------------------------------------------------------------------------ :: Hundredtwentyeight + bir_binpred Imm_hundredtwentyeight(word_hundredtwentyeight) Imm_hundredtwentyeight(word_hundredtwentyeight') ~> binpred_op(bir_binpred,word_hundredtwentyeight,word_hundredtwentyeight') -Theorem bir_eval_binpred_imp_compute_binpred: - !binpred v1 v2 v. bir_eval_binpred binpred v1 v2 v ==> - bir_compute_binpred binpred (SOME v1) (SOME v2) = SOME v -Proof - Cases_on `binpred` >> - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - rw [bir_eval_binpred_cases, bir_compute_binpred_def] >> - rw [bir_eval_binpred_imm_cases, bir_compute_binpred_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> - rw [bool2b_def, bool2w_def, bir_compute_binpred_imm_def, fetch "-" "bir_imm_t_nchotomy"] >> - fs [bir_eval_binpred_imm_cases, bir_binpred_get_oper_def] >> - metis_tac [] -QED - -(* If the term is well typed, then eval and compute are the same *) -Theorem well_typed_bir_eval_binpred_eq_compute_binpred: - !binpred v1 v2 v. - (type_of_bir_val v1 = type_of_bir_val v2) ==> - ( bir_eval_binpred binpred v1 v2 v <=> - bir_compute_binpred binpred (SOME v1) (SOME v2) = SOME v) -Proof - Cases_on `binpred` >> - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - rw [bir_eval_binpred_cases, bir_compute_binpred_def] >> - rw [bir_eval_binpred_imm_cases, bir_compute_binpred_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> - rw [bool2b_def, bool2w_def, bir_compute_binpred_imm_def, fetch "-" "bir_imm_t_nchotomy"] >> - fs [bir_eval_binpred_imm_cases, type_of_bir_val_def, type_of_bir_imm_def, - bir_binpred_get_oper_def] >> - metis_tac [] -QED - - -(* If the operands are typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_binpred: - !binpred v1 v2 ty. - ((type_of_bir_val v1 = BType_Imm ty) /\ (type_of_bir_val v2 = BType_Imm ty)) ==> - ?v. bir_eval_binpred binpred v1 v2 v -Proof - Cases_on `v1` >> Cases_on `v2` >> - Cases_on `b` >> Cases_on `b'` >> - rw [well_typed_bir_eval_binpred_eq_compute_binpred] >> - rw [bir_compute_binpred_def, bir_compute_binpred_imm_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] -QED - - -(* Type conservation theorem *) -Theorem bir_eval_binpred_correct_type: - !binpred v1 v2 v ty. - bir_eval_binpred binpred v1 v2 v ==> - ((type_of_bir_val v1 = type_of_bir_val v2) /\ type_of_bir_val v = (BType_Imm Bit1)) -Proof - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> - rw [type_of_bir_val_def, bir_eval_binpred_cases, type_of_bir_imm_def, bir_eval_binpred_imm_cases, bool2b_def] -QED - -(* Evaluates a general ifthenelse expression with values as parameters *) -Inductive bir_eval_ifthenelse: -[~BExp_IfThenElseT:] - bir_eval_ifthenelse birT (v1:bir_val_t) (v2:bir_val_t) v1 - -[~BExp_IfThenElseF:] - bir_eval_ifthenelse birF v1 v2 v2 -End +defns + bir_eval_binpred :: '' ::= -(* Computes an ifthenelse expression of two values *) -Definition bir_compute_ifthenelse_def: - bir_compute_ifthenelse b v1 v2 = - if b = SOME birT then v1 - else if b = SOME birF then v2 - else NONE -End -(* Eval and compute are similar *) -Theorem bir_eval_ifthenelse_eq_compute_ifthenelse: - !v (v1:bir_val_t) (v2:bir_val_t) (v3:bir_val_t). - (bir_eval_ifthenelse v v1 v2 v3 <=> - bir_compute_ifthenelse (SOME v) (SOME v1) (SOME v2) = SOME v3) -Proof - Cases_on `v` >> Cases_on `v1` >> Cases_on `v2` >> Cases_on `v3` >> - rw [bir_eval_ifthenelse_cases, bir_compute_ifthenelse_def, birT_def, birF_def] >> - metis_tac [] -QED - -(* If the condition is typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_ifthenelse: - !v v1 v2. - (type_of_bir_val v = (BType_Imm Bit1)) ==> - ?v3. bir_eval_ifthenelse v v1 v2 v3 -Proof - rw [bir_eval_ifthenelse_eq_compute_ifthenelse] >> - Cases_on `v` >| [ - Cases_on `b` >> - Cases_on `c` >> - metis_tac [bir_compute_ifthenelse_def, bit1_is_boolean], - - fs [type_of_bir_val_def] - ] -QED - -(* Type conservation Theorem *) -Theorem bir_eval_ifthenelse_keep_type: - !v v1 v2 v3 ty. - bir_eval_ifthenelse v v1 v2 v3 ==> - (type_of_bir_val v1 = ty /\ type_of_bir_val v2 = ty) ==> - (type_of_bir_val v = (BType_Imm Bit1) <=> type_of_bir_val v3 = ty) -Proof - Cases_on `v` >> Cases_on `v1` >> Cases_on `v2` >> Cases_on `v3` >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> Cases_on `b'''` >> - rw [type_of_bir_val_def, bir_eval_ifthenelse_cases, type_of_bir_imm_def, - birT_def, birF_def] -QED +defn + bir_binpred_t bir_val_t bir_val_t' ~> bir_val_t'' :: :: bir_eval_binpred :: Eval_BinPred_ + {{ com evaluation of a binary predicate of two bir values }} by + + bir_binpred bir_imm bir_imm' ~> b + ----------------------------------------------------------------------- :: Val + bir_binpred ValImm(bir_imm) ValImm(bir_imm') ~> ValImm(Imm_one(b2w(b))) + +defns + bir_eval_binexp :: '' ::= + +defn + bir_binexp_t bir_val_t bir_val_t' ~> bir_val_t'' :: :: bir_eval_binexp :: Eval_BinExp_ + {{ com evaluation of a binary expression of two bir values }} by + + bir_binexp bir_imm1 bir_imm2 ~> bir_imm + --------------------------------------------------------------- :: Val + bir_binexp ValImm(bir_imm1) ValImm(bir_imm2) ~> ValImm(bir_imm) + +defns + bir_eval_unaryexp :: '' ::= + +defn + bir_unaryexp_t bir_val_t ~> bir_val_t' :: :: bir_eval_unaryexp :: Eval_UnExp_ + {{ com evaluation of a unary expression of one bir value }} by + + bir_unaryexp bir_imm1 ~> bir_imm + ------------------------------------------------ :: Val + bir_unaryexp ValImm(bir_imm1) ~> ValImm(bir_imm) + +defns + bir_eval_ifthenelse :: '' ::= + +defn + bir_val bir_val1 bir_val2 ~> bir_val' :: :: bir_eval_ifthenelse :: Eval_IfThenElse_ + {{ com evaluation of if-then-else expression with values as parameters }} by + + ---------------------------------- :: T + birT bir_val1 bir_val2 ~> bir_val1 + + ---------------------------------- :: F + birF bir_val1 bir_val2 ~> bir_val2 + +embed +{{ hol (* Number to Bitstring *) Definition n2bs_def: @@ -801,7 +569,6 @@ Definition v2bs_def: v2bs v s = n2bs (v2n v) s End - (* Immediate to number *) Definition b2n_def: (b2n ( Imm1 w ) = w2n w) /\ @@ -837,11 +604,9 @@ Definition bitstring_split_def: bitstring_split n bs = bitstring_split_aux n [] bs End - -(* ------------------------------------------ *) -(* ------------------ LOAD ------------------ *) -(* ------------------------------------------ *) - +Definition is_exp_well_typed_def: + is_exp_well_typed env exp = ?ty. type_of_bir_exp env exp ty +End (* Load a value from the mmap at the given address *) Definition bir_load_mmap_def: @@ -851,7 +616,6 @@ Definition bir_load_mmap_def: | SOME v => v End - (* Concatenate multiple bitstrings to a number on the correct number of bits *) Definition bir_mem_concat_def: bir_mem_concat vl rty = v2bs (FLAT vl) rty @@ -873,7 +637,6 @@ Definition bir_number_of_mem_splits_def: else NONE End - (* Load a bitstring at the given address from a mmap and pad it *) Definition bir_load_bitstring_from_mmap_def: bir_load_bitstring_from_mmap vty mmap (a:num) = @@ -886,7 +649,6 @@ Definition bir_load_splits_from_mmap_def: (MAP (\k. bir_load_bitstring_from_mmap vty mmap (bir_mem_addr aty (addr + k))) (COUNT_LIST n)) End - (* Eval an already unpacked load expression *) Inductive bir_eval_load_from_mem: [~BEnd_BigEndian:] @@ -917,35 +679,6 @@ Definition bir_eval_load_def: (bir_eval_load _ _ _ _ _ = F) End -(* Computes an already unpacked load expression *) -Definition bir_compute_load_from_mem_def: - bir_compute_load_from_mem - (vty : bir_immtype_t) (rty : bir_immtype_t) (aty : bir_immtype_t) (mmap : num |-> num) (en: bir_endian_t) (addr:num) = - - case (bir_number_of_mem_splits vty rty aty) of - | NONE => NONE - | SOME (n:num) => ( - let vs = bir_load_splits_from_mmap aty vty mmap addr n in - let vs' = (case en of BEnd_LittleEndian => SOME (REVERSE vs) - | BEnd_BigEndian => SOME vs - | BEnd_NoEndian => if (n = 1) then SOME vs else NONE) in - case vs' of NONE => NONE - | SOME vs'' => SOME (bir_mem_concat vs'' rty) - ) -End - -Definition bir_compute_load_def: - (bir_compute_load (SOME (BVal_Mem aty vty mmap)) (SOME (BVal_Imm addr)) en rty = - val_from_imm_option (bir_compute_load_from_mem vty rty aty mmap en (b2n addr))) /\ - (bir_compute_load _ _ _ _ = NONE) -End - - -(* ----------------------------------------- *) -(* ----------------- STORE ----------------- *) -(* ----------------------------------------- *) - - (* Add all the bitstrings in the mmap at address a *) Definition bir_update_mmap_def: (bir_update_mmap aty mmap a [] = mmap) /\ @@ -953,7 +686,6 @@ Definition bir_update_mmap_def: bir_update_mmap aty (FUPDATE mmap ((bir_mem_addr aty a), v2n v)) (SUC a) vs) End - Inductive bir_eval_store_in_mem: [~BEnd_BigEndian:] !vty aty result mmap addr ll. @@ -978,7 +710,6 @@ Inductive bir_eval_store_in_mem: ==> bir_eval_store_in_mem vty aty result mmap BEnd_NoEndian addr (BVal_Mem aty vty (bir_update_mmap aty mmap addr ll)) - End Definition bir_eval_store_def: @@ -986,248 +717,6 @@ Definition bir_eval_store_def: bir_eval_store_in_mem vty aty result mmap en (b2n addr) v) /\ (bir_eval_store _ _ _ _ _ = F) End - -(* Compute an already unpacked store expression *) -Definition bir_compute_store_in_mem_def: - bir_compute_store_in_mem - (vty : bir_immtype_t) (aty : bir_immtype_t) (result : bir_imm_t) (mmap : num |-> num) (en: bir_endian_t) (addr:num) = - - let rty = type_of_bir_imm result in - case (bir_number_of_mem_splits vty rty aty) of - | NONE => NONE - | SOME (n:num) => ( - case (bitstring_split (size_of_bir_immtype vty) (b2v result)) of - | NONE => NONE - | SOME vs => - let vs' = (case en of BEnd_LittleEndian => SOME (REVERSE vs) - | BEnd_BigEndian => SOME vs - | BEnd_NoEndian => if (n = 1) then SOME vs else NONE) in - - case vs' of NONE => NONE - | SOME vs'' => SOME (BVal_Mem aty vty (bir_update_mmap aty mmap addr vs'')) - ) -End - - -Definition bir_compute_store_def: - (bir_compute_store (SOME (BVal_Mem aty vty mmap)) (SOME (BVal_Imm addr)) en (SOME (BVal_Imm result)) = - bir_compute_store_in_mem vty aty result mmap en (b2n addr)) /\ - (bir_compute_store _ _ _ _ = NONE) -End - -Theorem size_of_bir_immtype_leq_1: - !b. 1 <= 2 ** (size_of_bir_immtype b) -Proof - Cases_on `b` >> - rw [size_of_bir_immtype_def] -QED - -(* Eval and compute are similar *) -Theorem bir_eval_load_eq_compute_load: - !v_mem v_addr en rty v. - bir_eval_load v_mem v_addr en rty v <=> - (bir_compute_load (SOME v_mem) (SOME v_addr) en rty = SOME v) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `en` >> - rw [bir_eval_load_def, bir_eval_load_from_mem_cases] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def] >> - CASE_TAC >> - simp [] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - - - -(* If the operands are correctly typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_load_bigendian: - !aty vty v_mem v_addr rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_load v_mem v_addr BEnd_BigEndian rty v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - rw [bir_eval_load_eq_compute_load] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - -Theorem type_of_bir_val_imp_bir_eval_load_littleendian: - !aty vty v_mem v_addr rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_load v_mem v_addr BEnd_LittleEndian rty v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - rw [bir_eval_load_eq_compute_load] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - -Theorem type_of_bir_val_imp_bir_eval_load_noendian: - !aty vty v_mem v_addr rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty)) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) = 1)) - ==> - ?v. bir_eval_load v_mem v_addr BEnd_NoEndian rty v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - rw [bir_eval_load_eq_compute_load] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - rw [val_from_imm_option_def] >> - metis_tac [size_of_bir_immtype_leq_1] -QED - - -(* Type of bir_mem_concat *) -Theorem type_of_bir_imm_bir_mem_concat: - !vl rty. type_of_bir_imm (bir_mem_concat vl rty) = rty -Proof - Cases_on `rty` >> - rw [bir_mem_concat_def, v2bs_def, n2bs_def] >> - rw [type_of_bir_imm_def] -QED - - -(* Type conservation theorem *) -Theorem bir_eval_load_correct_type: - !v_mem v_addr en rty v. - bir_eval_load v_mem v_addr en rty v ==> - (type_of_bir_val v = (BType_Imm rty)) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - Cases_on `en` >> - - simp [bir_eval_load_def, bir_eval_load_from_mem_cases] >> - metis_tac [type_of_bir_val_def, type_of_bir_imm_def, type_of_bir_imm_bir_mem_concat] -QED - -(* bitstring_split will never be NONE *) -Theorem bitstring_split_aux_size_of_bir_immtype: - !ty acc bs. ?ll. bitstring_split_aux (size_of_bir_immtype ty) acc bs = SOME ll -Proof - gen_tac >> - `?n. size_of_bir_immtype ty = SUC n` by (Cases_on `ty` >> simp [size_of_bir_immtype_def]) >> - measureInduct_on `LENGTH bs` >> - Cases_on `bs` >> - fs [bitstring_split_def, bitstring_split_aux_def] >> - `LENGTH (DROP n t) < SUC (LENGTH t)` by rw [listTheory.LENGTH_DROP] >> - metis_tac [bitstring_split_aux_def, listTheory.LENGTH_DROP] -QED - -Theorem bitstring_split_size_of_bir_immtype: - !ty bs. bitstring_split (size_of_bir_immtype ty) bs <> NONE -Proof - simp [bitstring_split_def] >> - metis_tac [bitstring_split_aux_size_of_bir_immtype, optionTheory.NOT_SOME_NONE] -QED - -(* Eval and compute are similar *) -Theorem bir_eval_store_eq_compute_store: - !v_mem v_addr en result v. - bir_eval_store v_mem v_addr en result v <=> - (bir_compute_store (SOME v_mem) (SOME v_addr) en (SOME result) = SOME v) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `en` >> Cases_on `result` >> - rw [bir_eval_store_def, bir_eval_store_in_mem_cases] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def] >> - CASE_TAC >> CASE_TAC >> TRY CASE_TAC >> - simp [] >> - metis_tac [] -QED - -(* If the operands are correctly typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_store_bigendian: - !aty vty v_mem v_addr v_result rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - (type_of_bir_val v_result = BType_Imm rty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_store v_mem v_addr BEnd_BigEndian v_result v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - rw [bir_eval_store_eq_compute_store] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - TRY CASE_TAC >> - fs [bitstring_split_size_of_bir_immtype, bitstring_split_def] >> - metis_tac [bitstring_split_aux_size_of_bir_immtype] -QED - -Theorem type_of_bir_val_imp_bir_eval_store_littleendian: - !aty vty v_mem v_addr v_result rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - (type_of_bir_val v_result = BType_Imm rty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_store v_mem v_addr BEnd_LittleEndian v_result v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - rw [bir_eval_store_eq_compute_store] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - TRY CASE_TAC >> - fs [bitstring_split_size_of_bir_immtype] >> - metis_tac [] -QED - -Theorem type_of_bir_val_imp_bir_eval_store_noendian: - !aty vty v_mem v_addr v_result rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - (type_of_bir_val v_result = BType_Imm rty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty)) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) = 1)) - ==> - ?v. bir_eval_store v_mem v_addr BEnd_NoEndian v_result v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - rw [bir_eval_store_eq_compute_store] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - TRY CASE_TAC >> - fs [bitstring_split_size_of_bir_immtype] >> - metis_tac [size_of_bir_immtype_leq_1] -QED - -(* Type conservation theorem *) -Theorem bir_eval_store_correct_type: - !v_mem v_addr en v_result v. - bir_eval_store v_mem v_addr en v_result v ==> - (type_of_bir_val v = type_of_bir_val v_mem) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - Cases_on `en` >> - - simp [bir_eval_store_def, bir_eval_store_in_mem_cases] >> - rw [type_of_bir_val_def, type_of_bir_imm_def] >> - metis_tac [type_of_bir_val_def, type_of_bir_imm_def] -QED }} defns @@ -1235,13 +724,13 @@ defns defn bir_var_environment |- bir_exp ~> bir_val :: :: bir_eval_exp :: Eval_BExp_ - {{ com typing relation for BIR expressions }} by + {{ com evaluation of BIR expressions }} by ----------- :: Const - env |- Const(bir_imm) ~> Val_Imm(bir_imm) + env |- Const(bir_imm) ~> ValImm(bir_imm) ------------ :: MemConst - env |- MemConst(bir_immtype1,bir_immtype2,mmap) ~> Val_Mem(bir_immtype1,bir_immtype2,mmap) + env |- MemConst(bir_immtype1,bir_immtype2,mmap) ~> ValMem(bir_immtype1,bir_immtype2,mmap) bir_env_lookup_rel(env,bir_var,bir_val) --------- :: Den @@ -1283,3 +772,194 @@ defn bir_val1 bir_val2 bir_endian bir_val3 ~> bir_val ----- :: Store env |- Store(bir_exp1,bir_exp2,bir_endian,bir_exp3) ~> bir_val + +grammar +bir_label_t, bir_label :: BL_ ::= +{{ com Label values for jumps }} +| Label ( ident ) :: :: Label +| Address ( bir_imm ) :: :: Address + +bir_label_exp_t, bir_label_exp :: BLE_ ::= +{{ com Label expressions that may be computed }} +| Label ( bir_label ) :: :: Label +| Exp ( bir_exp ) :: :: Exp + +bir_stmt_basic_t, bir_stmt_basic :: BStmt_ ::= +{{ com Statements inside a program block }} +| Assign ( bir_var , bir_exp ) :: :: Assign + +bir_stmt_end_t, bir_stmt_end :: BStmt_ ::= +{{ com Statements at the end of a block }} +| Jmp ( bir_label_exp ) :: :: Jmp +| CJmp ( bir_exp , bir_label_exp1 , bir_label_exp2 ) :: :: CJmp + +bir_stmt_t, bir_stmt :: BStmt ::= +{{ com General statement }} +| Basic ( bir_stmt_basic ) :: :: B +| End ( bir_stmt_end ) :: :: E + +embed {{ hol + +(* Block type : a label, basic statements and an end statement *) +Datatype: + bir_block_t = <| + bb_label : bir_label_t; + bb_statements : bir_stmt_basic_t list; + bb_last_statement : bir_stmt_end_t |> +End + +(* Program counter : label of the current block and the offset inside the block *) +Datatype: + bir_programcounter_t = <| bpc_label:bir_label_t; bpc_index:num |> +End +}} + +metavar bir_block_t, bir_block ::= + {{ hol bir_block_t }} + +grammar +bir_program_t, bir_program :: '' ::= +| BirProgram ( bir_block1 , ... , bir_blockk ) :: :: BirProgram + +bir_status_t, bir_status :: BST_ ::= +{{ com Program state }} +| Running :: :: Running + {{ com still running }} +| TypeError :: :: TypeError + {{ com execution encountered a type error }} +| Failed :: :: Failed + {{ com execution failed }} +| JumpOutside ( bir_label ) :: :: JumpOutside + {{ com execution jumped to unknown label }} + +embed {{ hol + +(* Program state *) +Datatype: + bir_state_t = <| + bst_pc : bir_programcounter_t; + bst_environ : bir_var_environment_t; + bst_status : bir_status_t +|> +End + +(* Increment a program counter *) +Definition bir_pc_next_def: + bir_pc_next pc = pc with bpc_index updated_by SUC +End + +(* Get the index and block at the given label *) +Definition bir_get_program_block_info_by_label_def: + bir_get_program_block_info_by_label + (BirProgram p) l = INDEX_FIND 0 (\(x:bir_block_t). x.bb_label = l) p +End + +(* Checks whether a state is still running *) +Definition bir_state_is_terminated_def: + bir_state_is_terminated st = + (st.bst_status <> BST_Running) +End + +(* Set the program state to Failed *) +Definition bir_state_set_failed_def: + bir_state_set_failed st = + (st with bst_status := BST_Failed) +End + +(* Set the program state to TypeError *) +Definition bir_state_set_typeerror_def: + bir_state_set_typeerror st = + (st with bst_status := BST_TypeError) +End + +(* Get the statement of a program at the given program counter *) +Definition bir_get_current_statement_def: + bir_get_current_statement p pc = + case (bir_get_program_block_info_by_label p pc.bpc_label) of + | NONE => NONE + | SOME (_, bl) => if (pc.bpc_index < LENGTH bl.bb_statements) + then SOME (BStmtB (EL (pc.bpc_index) bl.bb_statements)) + else (if pc.bpc_index = LENGTH bl.bb_statements + then SOME (BStmtE bl.bb_last_statement) + else NONE) +End + +(* Get all the labels of a program *) +Definition bir_labels_of_program_def: + bir_labels_of_program (BirProgram p) = + MAP (\bl. bl.bb_label) p +End + +Definition bir_stmts_of_block_def: + bir_stmts_of_block b = + (BStmtE b.bb_last_statement) :: MAP (\bst. (BStmtB bst)) b.bb_statements +End + +Definition bir_stmts_of_program_def: + bir_stmts_of_program (BirProgram blist) = + FLAT (MAP (\bl. bir_stmts_of_block bl) blist) +End + +(* Return the program counter at the start of the block *) +Definition bir_block_pc_def: + bir_block_pc l = <| bpc_label := l; bpc_index := 0 |> +End + +(* Increment pc in a state if necessary *) +Definition bir_state_next_def: + bir_state_next st = + if (bir_state_is_terminated st) then st else st with bst_pc updated_by bir_pc_next +End + +(* Jump to a label *) +Definition bir_jmp_to_label_def: + bir_jmp_to_label p + (l : bir_label_t) (st : bir_state_t) = + if (MEM l (bir_labels_of_program p)) then + st with bst_pc := bir_block_pc l + else (st with bst_status := (BST_JumpOutside l)) +End + +(* Eval a label expression *) +Definition bir_eval_label_exp_def: + (bir_eval_label_exp (BLE_Label l) env l' = (l = l')) /\ + (bir_eval_label_exp (BLE_Exp e) env (BL_Address i) = bir_eval_exp env e (BVal_Imm i)) /\ + (bir_eval_label_exp _ _ _ = F) +End + +(* Eval a basic statement *) +Definition bir_eval_stmtB_def: + (bir_eval_stmtB (BStmt_Assign v ex) st st' = + (?va. (bir_eval_exp st.bst_environ ex va) + /\ (st' = (st with bst_environ := (bir_env_update st.bst_environ v va))))) +End + +(* Eval a Jmp statement *) +Definition bir_eval_stmt_jmp_def: + bir_eval_stmt_jmp p le (st : bir_state_t) st' = + (?l. bir_eval_label_exp le st.bst_environ l + /\ bir_jmp_to_label p l st = st') +End + +(* Eval a CJmp statement *) +Definition bir_eval_stmt_cjmp_def: + bir_eval_stmt_cjmp p ec l1 l2 (st : bir_state_t) st' = + (if bir_eval_exp st.bst_environ ec birT then + bir_eval_stmt_jmp p l1 st st' + else if bir_eval_exp st.bst_environ ec birF then + bir_eval_stmt_jmp p l2 st st' + else F) +End + +(* Eval an end statement *) +Definition bir_eval_stmtE_def: + (bir_eval_stmtE p (BStmt_Jmp le) st st' = bir_eval_stmt_jmp p le st st') /\ + (bir_eval_stmtE p (BStmt_CJmp e l1 l2) st st' = bir_eval_stmt_cjmp p e l1 l2 st st') +End +}} + +grammar +bir_state_t, bir_state :: '' ::= + {{ hol bir_state_t }} +| bir_state_set_failed ( bir_state ) :: M :: bir_state_set_failed + {{ hol (bir_state_set_failed [[bir_state]]) }} diff --git a/examples/compute/src/shared/cv/bir_cv_binexpScript.sml b/examples/compute/src/shared/cv/bir_cv_binexpScript.sml index 07cdffdb6..19f52dc6f 100644 --- a/examples/compute/src/shared/cv/bir_cv_binexpScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_binexpScript.sml @@ -3,7 +3,7 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse bossLib boolLib; -open birTheory bir_cv_basicTheory; +open birTheory bir_computeTheory bir_cv_basicTheory; open wordsTheory; diff --git a/examples/compute/src/shared/cv/bir_cv_binpredScript.sml b/examples/compute/src/shared/cv/bir_cv_binpredScript.sml index 8744db906..d5ab12a3f 100644 --- a/examples/compute/src/shared/cv/bir_cv_binpredScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_binpredScript.sml @@ -4,7 +4,7 @@ open HolKernel Parse boolLib bossLib; open bir_cv_basicTheory; -open birTheory; +open birTheory bir_computeTheory; val _ = new_theory "bir_cv_binpred"; diff --git a/examples/compute/src/shared/cv/bir_cv_envScript.sml b/examples/compute/src/shared/cv/bir_cv_envScript.sml index 3a74588c2..f86cc6d37 100644 --- a/examples/compute/src/shared/cv/bir_cv_envScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_envScript.sml @@ -3,7 +3,7 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse bossLib boolLib; -open birTheory bir_cv_basicTheory; +open birTheory bir_metaTheory bir_cv_basicTheory; open alistTheory; val _ = new_theory "bir_cv_env"; diff --git a/examples/compute/src/shared/cv/bir_cv_ifthenelseScript.sml b/examples/compute/src/shared/cv/bir_cv_ifthenelseScript.sml index c74a469d5..eb5063047 100644 --- a/examples/compute/src/shared/cv/bir_cv_ifthenelseScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_ifthenelseScript.sml @@ -3,7 +3,7 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse bossLib boolLib; -open birTheory bir_cv_basicTheory; +open birTheory bir_computeTheory bir_cv_basicTheory; val _ = new_theory "bir_cv_ifthenelse"; diff --git a/examples/compute/src/shared/cv/bir_cv_memScript.sml b/examples/compute/src/shared/cv/bir_cv_memScript.sml index 5c7bc0d20..555a885db 100644 --- a/examples/compute/src/shared/cv/bir_cv_memScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_memScript.sml @@ -3,7 +3,7 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse boolLib bossLib; -open birTheory bir_cv_basicTheory; +open birTheory bir_computeTheory bir_cv_basicTheory; open bitstringTheory numeral_bitTheory numposrepTheory; diff --git a/examples/compute/src/shared/cv/bir_cv_programScript.sml b/examples/compute/src/shared/cv/bir_cv_programScript.sml index a9eefeb31..eb208ad6c 100644 --- a/examples/compute/src/shared/cv/bir_cv_programScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_programScript.sml @@ -3,8 +3,8 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse bossLib boolLib; +open birTheory bir_programTheory; open bir_cv_basicTheory bir_cv_envTheory; -open bir_programTheory; open bir_cv_computeTheory; open listTheory; open optionTheory; diff --git a/examples/compute/src/shared/cv/bir_cv_unaryexpScript.sml b/examples/compute/src/shared/cv/bir_cv_unaryexpScript.sml index 39091efd1..2818e80d8 100644 --- a/examples/compute/src/shared/cv/bir_cv_unaryexpScript.sml +++ b/examples/compute/src/shared/cv/bir_cv_unaryexpScript.sml @@ -4,7 +4,7 @@ open HolKernel Parse bossLib boolLib; open bir_cv_basicTheory; -open birTheory; +open birTheory bir_computeTheory; open wordsTheory; diff --git a/examples/compute/src/theory/birScript.sml b/examples/compute/src/theory/birScript.sml index fff3b854d..ba2cb5054 100644 --- a/examples/compute/src/theory/birScript.sml +++ b/examples/compute/src/theory/birScript.sml @@ -1,4 +1,4 @@ -(* generated by Ott 0.33 from: ../../ott/bir.ott *) +(* generated by Ott 0.34 from: ../../ott/bir.ott *) (* to compile: Holmake birTheory.uo *) (* for interactive use: app load ["pred_setTheory","finite_mapTheory","stringTheory","containerTheory","ottLib"]; @@ -15,13 +15,20 @@ open wordsTheory; open bitstringTheory numeral_bitTheory; Type mmap = ``:(num |-> num)`` (* BIR memory map *) -Type ident = ``:string`` (* Identifier for variable name *) -Type word_one = ``:word1`` (* 1-bit word *) -Type word_eight = ``:word8`` (* 8-bit word *) -Type word_sixteen = ``:word16`` (* 16-bit word *) -Type word_thirtytwo = ``:word32`` (* 32-bit word *) -Type word_sixtyfour = ``:word64`` (* 64-bit word *) -Type word_hundredtwentyeight = ``:word128`` (* 128-bit word *) +Type ident = ``:string`` (* Identifier *) +Type k = ``:num`` + +Type word_one = ``:word1`` + +Type word_eight = ``:word8`` + +Type word_sixteen = ``:word16`` + +Type word_thirtytwo = ``:word32`` + +Type word_sixtyfour = ``:word64`` + +Type word_hundredtwentyeight = ``:word128`` val _ = Hol_datatype ` bir_imm_t = (* immediates *) Imm1 of word_one @@ -82,6 +89,8 @@ bir_exp_t = (* BIR expressions *) | BExp_Load of bir_exp_t => bir_exp_t => bir_endian_t => bir_immtype_t (* Memory value / Address Value (Imm) / Endian / Type of where to load *) | BExp_Store of bir_exp_t => bir_exp_t => bir_endian_t => bir_exp_t (* Memory value / Address Value (Imm) / Endian / Value to store *) `; + +Type b = ``:bool`` val _ = Hol_datatype ` bir_type_t = (* general typing *) BType_Imm of bir_immtype_t @@ -105,19 +114,6 @@ Definition birF_def: birF = BVal_Imm (Imm1 0w) End -(* Correction Theorems of boolean functions *) -Theorem bool2b_T_eq_birT: - BVal_Imm (bool2b T) = birT -Proof - rw [bool2b_def, bool2w_def, birT_def] -QED - -Theorem bool2b_F_eq_birF: - BVal_Imm (bool2b F) = birF -Proof - rw [bool2b_def, bool2w_def, birF_def] -QED - (* Utility functions *) Definition bir_dest_bool_val_def: (bir_dest_bool_val (BVal_Imm (Imm1 w)) = SOME (w = 1w)) /\ @@ -156,64 +152,6 @@ Definition bir_env_update_def: bir_env_update ((BEnv env):bir_var_environment_t) (BVar id) v = BEnv ((id =+ SOME v) env) End -Theorem bir_env_lookup_empty: - !var v. ~(bir_env_lookup_rel bir_empty_env var v) -Proof - Cases_on `var` >> - rw [bir_empty_env_def, bir_env_lookup_rel_def] -QED - -Theorem bir_env_lookup_rel_update: - !env var v. bir_env_lookup_rel (bir_env_update env var v) var v -Proof - Cases_on `var` >> Cases_on `env` >> - rw [bir_env_update_def, bir_env_lookup_rel_def] -QED - -Theorem bir_env_lookup_update: - !env var v. bir_env_lookup (bir_env_update env var v) var = SOME v -Proof - rpt gen_tac >> - Cases_on `var` >> Cases_on `env` >> - rw [bir_env_update_def, bir_env_lookup_def] -QED - -Theorem bir_env_lookup_update_neq: - !env var1 var2 v. - var1 <> var2 ==> - bir_env_lookup (bir_env_update env var1 v) var2 = bir_env_lookup env var2 -Proof - Cases_on `var1` >> Cases_on `var2` >> - rw [fetch "-" "bir_var_t_11"] >> - Cases_on `env` >> - simp [bir_env_update_def] >> - rw [bir_env_lookup_def] >> - EVAL_TAC >> - metis_tac [] -QED - -(* Lookup and relation are the same *) -Theorem bir_env_lookup_eq_rel: - !env var v. bir_env_lookup_rel env var v <=> bir_env_lookup env var = SOME v -Proof - rpt strip_tac >> - Cases_on `env` >> - Cases_on `var` >> - rw [bir_env_lookup_def, bir_env_lookup_rel_def] -QED - - -(* Injective *) -Theorem bir_env_lookup_rel_inj: - !env var v1 v2. - bir_env_lookup_rel env var v1 ==> - bir_env_lookup_rel env var v2 ==> - v1 = v2 -Proof - Cases_on `env` >> Cases_on `var` >> - simp [bir_env_lookup_rel_def] -QED - (* --------- Typing ------- *) (* Gives the size of an immediate as a number *) @@ -242,6 +180,24 @@ Definition type_of_bir_val_def: (type_of_bir_val (BVal_Mem aty vty mmap) = (BType_Mem aty vty) ) End +(* Gets the operator for a given binary operation *) +Definition bir_binexp_get_oper_def: + (bir_binexp_get_oper BIExp_And = word_and) /\ + (bir_binexp_get_oper BIExp_Plus = word_add) +End + +(* Gets the operator for a given unary operation *) +Definition bir_unaryexp_get_oper_def: + (bir_unaryexp_get_oper BIExp_Not = word_1comp) /\ + (bir_unaryexp_get_oper BIExp_ChangeSign = word_2comp) +End + +(* Gets the operator for a given binary predicate *) +Definition bir_binpred_get_oper_def: + (bir_binpred_get_oper BIExp_Equal = $=) /\ + (bir_binpred_get_oper BIExp_LessThan = word_lo) +End + Type bir_var_environment_t = ``:bir_var_environment_t`` Type n = ``:num`` @@ -354,384 +310,166 @@ Inductive type_of_bir_exp: ==> ( ( type_of_bir_exp env (BExp_Store bir_exp1 bir_exp2 BEnd_LittleEndian bir_exp3) (BType_Mem bir_immtype1 bir_immtype2) ))) End +(** definitions *) -Definition is_exp_well_typed_def: - is_exp_well_typed env exp = ?ty. type_of_bir_exp env exp ty +(* defns bir_eval_binexp_imm *) +Inductive bir_eval_binexp_imm: +(* defn bir_eval_binexp_imm *) + +[Eval_BinExp_Imm_One:] (! (bir_binexp:bir_binexp_t) (word_one:word_one) (word_one':word_one) . +(clause_name "Eval_BinExp_Imm_One") + ==> +( ( bir_eval_binexp_imm bir_binexp (Imm1 word_one) (Imm1 word_one') (Imm1 ((bir_binexp_get_oper bir_binexp ) word_one word_one' ) ) ))) + +[Eval_BinExp_Imm_Eight:] (! (bir_binexp:bir_binexp_t) (word_eight:word_eight) (word_eight':word_eight) . +(clause_name "Eval_BinExp_Imm_Eight") + ==> +( ( bir_eval_binexp_imm bir_binexp (Imm8 word_eight) (Imm8 word_eight') (Imm8 ((bir_binexp_get_oper bir_binexp ) word_eight word_eight' ) ) ))) + +[Eval_BinExp_Imm_Sixteen:] (! (bir_binexp:bir_binexp_t) (word_sixteen:word_sixteen) (word_sixteen':word_sixteen) . +(clause_name "Eval_BinExp_Imm_Sixteen") + ==> +( ( bir_eval_binexp_imm bir_binexp (Imm16 word_sixteen) (Imm16 word_sixteen') (Imm16 ((bir_binexp_get_oper bir_binexp ) word_sixteen word_sixteen' ) ) ))) + +[Eval_BinExp_Imm_Thirtytwo:] (! (bir_binexp:bir_binexp_t) (word_thirtytwo:word_thirtytwo) (word_thirtytwo':word_thirtytwo) . +(clause_name "Eval_BinExp_Imm_Thirtytwo") + ==> +( ( bir_eval_binexp_imm bir_binexp (Imm32 word_thirtytwo) (Imm32 word_thirtytwo') (Imm32 ((bir_binexp_get_oper bir_binexp ) word_thirtytwo word_thirtytwo' ) ) ))) + +[Eval_BinExp_Imm_Sixtyfour:] (! (bir_binexp:bir_binexp_t) (word_sixtyfour:word_sixtyfour) (word_sixtyfour':word_sixtyfour) . +(clause_name "Eval_BinExp_Imm_Sixtyfour") + ==> +( ( bir_eval_binexp_imm bir_binexp (Imm64 word_sixtyfour) (Imm64 word_sixtyfour') (Imm64 ((bir_binexp_get_oper bir_binexp ) word_sixtyfour word_sixtyfour' ) ) ))) + +[Eval_BinExp_Imm_Hundredtwentyeight:] (! (bir_binexp:bir_binexp_t) (word_hundredtwentyeight:word_hundredtwentyeight) (word_hundredtwentyeight':word_hundredtwentyeight) . +(clause_name "Eval_BinExp_Imm_Hundredtwentyeight") + ==> +( ( bir_eval_binexp_imm bir_binexp (Imm128 word_hundredtwentyeight) (Imm128 word_hundredtwentyeight') (Imm128 ((bir_binexp_get_oper bir_binexp ) word_hundredtwentyeight word_hundredtwentyeight' ) ) ))) End +(** definitions *) -(* 1 bit values are booleans *) -Theorem bit1_is_boolean: - !v. type_of_bir_val v = (BType_Imm Bit1) ==> (v = birT \/ v = birF) -Proof - Cases_on `v` >> - Cases_on `b` >> - rw [birT_def, birF_def, type_of_bir_val_def, type_of_bir_imm_def] >> - Cases_on `c` >> - fs [dimword_1] -QED +(* defns bir_eval_unaryexp_imm *) +Inductive bir_eval_unaryexp_imm: +(* defn bir_eval_unaryexp_imm *) -(* Gets the operator for a given binary operation *) -Definition bir_binexp_get_oper_def: - (bir_binexp_get_oper BIExp_And = word_and) /\ - (bir_binexp_get_oper BIExp_Plus = word_add) +[Eval_UnaryExp_Imm_One:] (! (bir_unaryexp:bir_unaryexp_t) (word_one:word_one) . +(clause_name "Eval_UnaryExp_Imm_One") + ==> +( ( bir_eval_unaryexp_imm bir_unaryexp (Imm1 word_one) (Imm1 ((bir_unaryexp_get_oper bir_unaryexp ) word_one ) ) ))) + +[Eval_UnaryExp_Imm_Eight:] (! (bir_unaryexp:bir_unaryexp_t) (word_eight:word_eight) . +(clause_name "Eval_UnaryExp_Imm_Eight") + ==> +( ( bir_eval_unaryexp_imm bir_unaryexp (Imm8 word_eight) (Imm8 ((bir_unaryexp_get_oper bir_unaryexp ) word_eight ) ) ))) + +[Eval_UnaryExp_Imm_Sixteen:] (! (bir_unaryexp:bir_unaryexp_t) (word_sixteen:word_sixteen) . +(clause_name "Eval_UnaryExp_Imm_Sixteen") + ==> +( ( bir_eval_unaryexp_imm bir_unaryexp (Imm16 word_sixteen) (Imm16 ((bir_unaryexp_get_oper bir_unaryexp ) word_sixteen ) ) ))) + +[Eval_UnaryExp_Imm_Thirtytwo:] (! (bir_unaryexp:bir_unaryexp_t) (word_thirtytwo:word_thirtytwo) . +(clause_name "Eval_UnaryExp_Imm_Thirtytwo") + ==> +( ( bir_eval_unaryexp_imm bir_unaryexp (Imm32 word_thirtytwo) (Imm32 ((bir_unaryexp_get_oper bir_unaryexp ) word_thirtytwo ) ) ))) + +[Eval_UnaryExp_Imm_Sixtyfour:] (! (bir_unaryexp:bir_unaryexp_t) (word_sixtyfour:word_sixtyfour) . +(clause_name "Eval_UnaryExp_Imm_Sixtyfour") + ==> +( ( bir_eval_unaryexp_imm bir_unaryexp (Imm64 word_sixtyfour) (Imm64 ((bir_unaryexp_get_oper bir_unaryexp ) word_sixtyfour ) ) ))) + +[Eval_UnaryExp_Imm_Hundredtwentyeight:] (! (bir_unaryexp:bir_unaryexp_t) (word_hundredtwentyeight:word_hundredtwentyeight) . +(clause_name "Eval_UnaryExp_Imm_Hundredtwentyeight") + ==> +( ( bir_eval_unaryexp_imm bir_unaryexp (Imm128 word_hundredtwentyeight) (Imm128 ((bir_unaryexp_get_oper bir_unaryexp ) word_hundredtwentyeight ) ) ))) End -(* Evaluates a binary expression of two immediates *) -Inductive bir_eval_binexp_imm: - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm1 w1) (Imm1 w2) (Imm1 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm8 w1) (Imm8 w2) (Imm8 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm16 w1) (Imm16 w2) (Imm16 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm32 w1) (Imm32 w2) (Imm32 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm64 w1) (Imm64 w2) (Imm64 ((bir_binexp_get_oper binexp) w1 w2))) /\ - (!binexp w1 w2. - bir_eval_binexp_imm binexp (Imm128 w1) (Imm128 w2) (Imm128 ((bir_binexp_get_oper binexp) w1 w2))) -End - -(* Evaluates a general binary expression with values as parameters *) -Definition bir_eval_binexp_def: - (bir_eval_binexp binexp (BVal_Imm imm1) (BVal_Imm imm2) (BVal_Imm imm) = - (bir_eval_binexp_imm binexp imm1 imm2 imm)) /\ - (bir_eval_binexp _ _ _ _ = F) -End - -(* Computes a binary expression of two immediates *) -Definition bir_compute_binexp_imm_def: - (bir_compute_binexp_imm BIExp_And (Imm1 w1) (Imm1 w2) = SOME (Imm1 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm8 w1) (Imm8 w2) = SOME (Imm8 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm16 w1) (Imm16 w2) = SOME (Imm16 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm32 w1) (Imm32 w2) = SOME (Imm32 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm64 w1) (Imm64 w2) = SOME (Imm64 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_And (Imm128 w1) (Imm128 w2) = SOME (Imm128 (word_and w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm1 w1) (Imm1 w2) = SOME (Imm1 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm8 w1) (Imm8 w2) = SOME (Imm8 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm16 w1) (Imm16 w2) = SOME (Imm16 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm32 w1) (Imm32 w2) = SOME (Imm32 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm64 w1) (Imm64 w2) = SOME (Imm64 (word_add w1 w2))) /\ - (bir_compute_binexp_imm BIExp_Plus (Imm128 w1) (Imm128 w2) = SOME (Imm128 (word_add w1 w2))) /\ - (bir_compute_binexp_imm binexp _ _ = NONE) -End - - -(* Computes a general binary expression with values as parameters *) -Definition bir_compute_binexp_def: - (bir_compute_binexp binexp (SOME (BVal_Imm imm1)) (SOME (BVal_Imm imm2)) = - val_from_imm_option (bir_compute_binexp_imm binexp imm1 imm2)) /\ - (bir_compute_binexp _ _ _ = NONE) -End - -(* Eval and compute are similar *) -Theorem bir_eval_binexp_eq_compute_binexp: - !binexp v1 v2 v. bir_eval_binexp binexp v1 v2 v <=> - bir_compute_binexp binexp (SOME v1) (SOME v2) = SOME v -Proof - Cases_on `binexp` >> - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - rw [bir_eval_binexp_def, bir_compute_binexp_def] >> - rw [bir_eval_binexp_imm_cases, bir_compute_binexp_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> - rw [bir_compute_binexp_imm_def, fetch "-" "bir_imm_t_nchotomy", bir_binexp_get_oper_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - - -(* If the operands are typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_binexp: - !binexp v1 v2 ty. - ((type_of_bir_val v1 = BType_Imm ty) /\ (type_of_bir_val v2 = BType_Imm ty)) ==> - ?v. bir_eval_binexp binexp v1 v2 v -Proof - Cases_on `binexp` >> - Cases_on `v1` >> Cases_on `v2` >> - Cases_on `b` >> Cases_on `b'` >> - rw [bir_eval_binexp_eq_compute_binexp] >> - rw [bir_compute_binexp_def, bir_compute_binexp_imm_def] >> - rw [val_from_imm_option_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] -QED - - -(* Type conservation Theorem *) -Theorem bir_eval_binexp_keep_type: - !binexp v1 v2 v ty. - bir_eval_binexp binexp v1 v2 v ==> - ((type_of_bir_val v1 = ty /\ type_of_bir_val v2 = ty) <=> - type_of_bir_val v = ty) -Proof - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> - rw [type_of_bir_val_def, bir_eval_binexp_def, type_of_bir_imm_def, bir_eval_binexp_imm_cases] -QED +(** definitions *) -(* Gets the operator for a given unary operation *) -Definition bir_unaryexp_get_oper_def: - (bir_unaryexp_get_oper BIExp_Not = word_1comp) /\ - (bir_unaryexp_get_oper BIExp_ChangeSign = word_2comp) +(* defns bir_eval_binpred_imm *) +Inductive bir_eval_binpred_imm: +(* defn bir_eval_binpred_imm *) + +[Eval_BinPred_Imm_One:] (! (bir_binpred:bir_binpred_t) (word_one:word_one) (word_one':word_one) . +(clause_name "Eval_BinPred_Imm_One") + ==> +( ( bir_eval_binpred_imm bir_binpred (Imm1 word_one) (Imm1 word_one') ((bir_binpred_get_oper bir_binpred ) word_one word_one' ) ))) + +[Eval_BinPred_Imm_Eight:] (! (bir_binpred:bir_binpred_t) (word_eight:word_eight) (word_eight':word_eight) . +(clause_name "Eval_BinPred_Imm_Eight") + ==> +( ( bir_eval_binpred_imm bir_binpred (Imm8 word_eight) (Imm8 word_eight') ((bir_binpred_get_oper bir_binpred ) word_eight word_eight' ) ))) + +[Eval_BinPred_Imm_Sixteen:] (! (bir_binpred:bir_binpred_t) (word_sixteen:word_sixteen) (word_sixteen':word_sixteen) . +(clause_name "Eval_BinPred_Imm_Sixteen") + ==> +( ( bir_eval_binpred_imm bir_binpred (Imm16 word_sixteen) (Imm16 word_sixteen') ((bir_binpred_get_oper bir_binpred ) word_sixteen word_sixteen' ) ))) + +[Eval_BinPred_Imm_Thirtytwo:] (! (bir_binpred:bir_binpred_t) (word_thirtytwo:word_thirtytwo) (word_thirtytwo':word_thirtytwo) . +(clause_name "Eval_BinPred_Imm_Thirtytwo") + ==> +( ( bir_eval_binpred_imm bir_binpred (Imm32 word_thirtytwo) (Imm32 word_thirtytwo') ((bir_binpred_get_oper bir_binpred ) word_thirtytwo word_thirtytwo' ) ))) + +[Eval_BinPred_Imm_Sixtyfour:] (! (bir_binpred:bir_binpred_t) (word_sixtyfour:word_sixtyfour) (word_sixtyfour':word_sixtyfour) . +(clause_name "Eval_BinPred_Imm_Sixtyfour") + ==> +( ( bir_eval_binpred_imm bir_binpred (Imm64 word_sixtyfour) (Imm64 word_sixtyfour') ((bir_binpred_get_oper bir_binpred ) word_sixtyfour word_sixtyfour' ) ))) + +[Eval_BinPred_Imm_Hundredtwentyeight:] (! (bir_binpred:bir_binpred_t) (word_hundredtwentyeight:word_hundredtwentyeight) (word_hundredtwentyeight':word_hundredtwentyeight) . +(clause_name "Eval_BinPred_Imm_Hundredtwentyeight") + ==> +( ( bir_eval_binpred_imm bir_binpred (Imm128 word_hundredtwentyeight) (Imm128 word_hundredtwentyeight') ((bir_binpred_get_oper bir_binpred ) word_hundredtwentyeight word_hundredtwentyeight' ) ))) End +(** definitions *) +(* defns bir_eval_binpred *) +Inductive bir_eval_binpred: +(* defn bir_eval_binpred *) -(* Evaluates a binary expression of an immediate *) -Inductive bir_eval_unaryexp_imm: - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm1 w1) (Imm1 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm8 w1) (Imm8 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm16 w1) (Imm16 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm32 w1) (Imm32 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm64 w1) (Imm64 ((bir_unaryexp_get_oper unaryexp) w1))) /\ - (!unaryexp w1. - bir_eval_unaryexp_imm unaryexp (Imm128 w1) (Imm128 ((bir_unaryexp_get_oper unaryexp) w1))) -End - - -(* Evaluates a general unary expression with values as parameters *) -Definition bir_eval_unaryexp_def: - (bir_eval_unaryexp unaryexp (BVal_Imm imm1) (BVal_Imm imm) = - (bir_eval_unaryexp_imm unaryexp imm1 imm)) /\ - (bir_eval_unaryexp _ _ _ = F) -End - -(* Computes a binary expression of an immediate *) -Definition bir_compute_unaryexp_imm_def: - (bir_compute_unaryexp_imm BIExp_Not (Imm1 w1) = SOME (Imm1 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm8 w1) = SOME (Imm8 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm16 w1) = SOME (Imm16 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm32 w1) = SOME (Imm32 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm64 w1) = SOME (Imm64 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_Not (Imm128 w1) = SOME (Imm128 (word_1comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm1 w1) = SOME (Imm1 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm8 w1) = SOME (Imm8 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm16 w1) = SOME (Imm16 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm32 w1) = SOME (Imm32 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm64 w1) = SOME (Imm64 (word_2comp w1))) /\ - (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm128 w1) = SOME (Imm128 (word_2comp w1))) -End - -(* Computes Unary expression *) -Definition bir_compute_unaryexp_def: - (bir_compute_unaryexp unaryexp (SOME (BVal_Imm imm1)) = - val_from_imm_option (bir_compute_unaryexp_imm unaryexp imm1)) /\ - (bir_compute_unaryexp _ _ = NONE) -End - -(* Eval and Compute are similar *) -Theorem bir_eval_unaryexp_eq_compute_unaryexp: - !unaryexp v1 v. bir_eval_unaryexp unaryexp v1 v <=> - bir_compute_unaryexp unaryexp (SOME v1) = SOME v -Proof - Cases_on `unaryexp` >> - Cases_on `v1` >> Cases_on `v` >> - rw [bir_eval_unaryexp_def, bir_compute_unaryexp_def] >> - rw [bir_eval_unaryexp_imm_cases, bir_compute_unaryexp_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> - rw [bir_compute_unaryexp_imm_def, fetch "-" "bir_imm_t_nchotomy", bir_unaryexp_get_oper_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - - -(* Unary_exp always evaluates *) -Theorem type_of_bir_val_imp_bir_eval_unaryexp: - !unaryexp v ty. - (type_of_bir_val v = BType_Imm ty) ==> - ?v'. bir_eval_unaryexp unaryexp v v' -Proof - Cases_on `unaryexp` >> - Cases_on `v` >> - Cases_on `b` >> - rw [bir_eval_unaryexp_eq_compute_unaryexp, type_of_bir_val_def] >> - rw [bir_compute_unaryexp_def, bir_compute_unaryexp_imm_def] >> - rw [val_from_imm_option_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] -QED - -(* Type conservation theorem *) -Theorem bir_eval_unaryexp_keep_type: - !unaryexp v1 v2 ty. - bir_eval_unaryexp unaryexp v1 v2 ==> - (type_of_bir_val v1 = type_of_bir_val v2) -Proof - Cases_on `v1` >> Cases_on `v2` >> - Cases_on `b` >> Cases_on `b'` >> - rw [type_of_bir_val_def, bir_eval_unaryexp_def, type_of_bir_imm_def, bir_eval_unaryexp_imm_cases] -QED +[Eval_BinPred_Val:] (! (bir_binpred:bir_binpred_t) (bir_imm:bir_imm_t) (bir_imm':bir_imm_t) (b:b) . +(clause_name "Eval_BinPred_Val") /\ +(( ( bir_eval_binpred_imm bir_binpred bir_imm bir_imm' b ))) + ==> +( ( bir_eval_binpred bir_binpred (BVal_Imm bir_imm) (BVal_Imm bir_imm') (BVal_Imm (Imm1 (bool2w b ) )) ))) +End +(** definitions *) -(* Gets the operator for a given binary predicate *) -Definition bir_binpred_get_oper_def: - (bir_binpred_get_oper BIExp_Equal = $=) /\ - (bir_binpred_get_oper BIExp_LessThan = word_lo) +(* defns bir_eval_binexp *) +Inductive bir_eval_binexp: +(* defn bir_eval_binexp *) + +[Eval_BinExp_Val:] (! (bir_binexp:bir_binexp_t) (bir_imm1:bir_imm_t) (bir_imm2:bir_imm_t) (bir_imm:bir_imm_t) . +(clause_name "Eval_BinExp_Val") /\ +(( ( bir_eval_binexp_imm bir_binexp bir_imm1 bir_imm2 bir_imm ))) + ==> +( ( bir_eval_binexp bir_binexp (BVal_Imm bir_imm1) (BVal_Imm bir_imm2) (BVal_Imm bir_imm) ))) End +(** definitions *) +(* defns bir_eval_unaryexp *) +Inductive bir_eval_unaryexp: +(* defn bir_eval_unaryexp *) -(* Evaluates a binary predicate of two immediates *) -Inductive bir_eval_binpred_imm: - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm1 w1) (Imm1 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm8 w1) (Imm8 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm16 w1) (Imm16 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm32 w1) (Imm32 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm64 w1) (Imm64 w2) ((bir_binpred_get_oper binpred) w1 w2)) /\ - (!binpred w1 w2. - bir_eval_binpred_imm binpred (Imm128 w1) (Imm128 w2) ((bir_binpred_get_oper binpred) w1 w2)) -End - - -(* Evaluates a general binary predicate with values as parameters *) -Inductive bir_eval_binpred: - (!binpred imm1 imm2 b. - (bir_eval_binpred_imm binpred imm1 imm2 b) ==> - (bir_eval_binpred binpred (BVal_Imm imm1) (BVal_Imm imm2) (BVal_Imm (bool2b b)))) -End - -(* Computes a binary predicate of two immediates *) -Definition bir_compute_binpred_imm_def: - (bir_compute_binpred_imm BIExp_Equal (Imm1 w1) (Imm1 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm8 w1) (Imm8 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm16 w1) (Imm16 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm32 w1) (Imm32 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm64 w1) (Imm64 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_Equal (Imm128 w1) (Imm128 w2) = $= w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm1 w1) (Imm1 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm8 w1) (Imm8 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm16 w1) (Imm16 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm32 w1) (Imm32 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm64 w1) (Imm64 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm BIExp_LessThan (Imm128 w1) (Imm128 w2) = word_lo w1 w2) /\ - (bir_compute_binpred_imm binpred _ _ = F) -End - - -(* Computes a general binary predicate with values as parameters *) -Definition bir_compute_binpred_def: - (bir_compute_binpred binpred (SOME (BVal_Imm imm1)) (SOME (BVal_Imm imm2)) = - SOME (BVal_Imm (bool2b (bir_compute_binpred_imm binpred imm1 imm2)))) /\ - (bir_compute_binpred _ _ _ = NONE) -End - -Theorem bir_eval_binpred_imp_compute_binpred: - !binpred v1 v2 v. bir_eval_binpred binpred v1 v2 v ==> - bir_compute_binpred binpred (SOME v1) (SOME v2) = SOME v -Proof - Cases_on `binpred` >> - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - rw [bir_eval_binpred_cases, bir_compute_binpred_def] >> - rw [bir_eval_binpred_imm_cases, bir_compute_binpred_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> - rw [bool2b_def, bool2w_def, bir_compute_binpred_imm_def, fetch "-" "bir_imm_t_nchotomy"] >> - fs [bir_eval_binpred_imm_cases, bir_binpred_get_oper_def] >> - metis_tac [] -QED - -(* If the term is well typed, then eval and compute are the same *) -Theorem well_typed_bir_eval_binpred_eq_compute_binpred: - !binpred v1 v2 v. - (type_of_bir_val v1 = type_of_bir_val v2) ==> - ( bir_eval_binpred binpred v1 v2 v <=> - bir_compute_binpred binpred (SOME v1) (SOME v2) = SOME v) -Proof - Cases_on `binpred` >> - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - rw [bir_eval_binpred_cases, bir_compute_binpred_def] >> - rw [bir_eval_binpred_imm_cases, bir_compute_binpred_imm_def] >> - Cases_on `b` >> Cases_on `b'` >> - rw [bool2b_def, bool2w_def, bir_compute_binpred_imm_def, fetch "-" "bir_imm_t_nchotomy"] >> - fs [bir_eval_binpred_imm_cases, type_of_bir_val_def, type_of_bir_imm_def, - bir_binpred_get_oper_def] >> - metis_tac [] -QED - - -(* If the operands are typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_binpred: - !binpred v1 v2 ty. - ((type_of_bir_val v1 = BType_Imm ty) /\ (type_of_bir_val v2 = BType_Imm ty)) ==> - ?v. bir_eval_binpred binpred v1 v2 v -Proof - Cases_on `v1` >> Cases_on `v2` >> - Cases_on `b` >> Cases_on `b'` >> - rw [well_typed_bir_eval_binpred_eq_compute_binpred] >> - rw [bir_compute_binpred_def, bir_compute_binpred_imm_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] -QED - - -(* Type conservation theorem *) -Theorem bir_eval_binpred_correct_type: - !binpred v1 v2 v ty. - bir_eval_binpred binpred v1 v2 v ==> - ((type_of_bir_val v1 = type_of_bir_val v2) /\ type_of_bir_val v = (BType_Imm Bit1)) -Proof - Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> - rw [type_of_bir_val_def, bir_eval_binpred_cases, type_of_bir_imm_def, bir_eval_binpred_imm_cases, bool2b_def] -QED - -(* Evaluates a general ifthenelse expression with values as parameters *) +[Eval_UnExp_Val:] (! (bir_unaryexp:bir_unaryexp_t) (bir_imm1:bir_imm_t) (bir_imm:bir_imm_t) . +(clause_name "Eval_UnExp_Val") /\ +(( ( bir_eval_unaryexp_imm bir_unaryexp bir_imm1 bir_imm ))) + ==> +( ( bir_eval_unaryexp bir_unaryexp (BVal_Imm bir_imm1) (BVal_Imm bir_imm) ))) +End +(** definitions *) + +(* defns bir_eval_ifthenelse *) Inductive bir_eval_ifthenelse: -[~BExp_IfThenElseT:] - bir_eval_ifthenelse birT (v1:bir_val_t) (v2:bir_val_t) v1 +(* defn bir_eval_ifthenelse *) -[~BExp_IfThenElseF:] - bir_eval_ifthenelse birF v1 v2 v2 -End +[Eval_IfThenElse_T:] (! (bir_val1:bir_val_t) (bir_val2:bir_val_t) . +(clause_name "Eval_IfThenElse_T") + ==> +( ( bir_eval_ifthenelse birT bir_val1 bir_val2 bir_val1 ))) -(* Computes an ifthenelse expression of two values *) -Definition bir_compute_ifthenelse_def: - bir_compute_ifthenelse b v1 v2 = - if b = SOME birT then v1 - else if b = SOME birF then v2 - else NONE +[Eval_IfThenElse_F:] (! (bir_val1:bir_val_t) (bir_val2:bir_val_t) . +(clause_name "Eval_IfThenElse_F") + ==> +( ( bir_eval_ifthenelse birF bir_val1 bir_val2 bir_val2 ))) End -(* Eval and compute are similar *) -Theorem bir_eval_ifthenelse_eq_compute_ifthenelse: - !v (v1:bir_val_t) (v2:bir_val_t) (v3:bir_val_t). - (bir_eval_ifthenelse v v1 v2 v3 <=> - bir_compute_ifthenelse (SOME v) (SOME v1) (SOME v2) = SOME v3) -Proof - Cases_on `v` >> Cases_on `v1` >> Cases_on `v2` >> Cases_on `v3` >> - rw [bir_eval_ifthenelse_cases, bir_compute_ifthenelse_def, birT_def, birF_def] >> - metis_tac [] -QED - -(* If the condition is typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_ifthenelse: - !v v1 v2. - (type_of_bir_val v = (BType_Imm Bit1)) ==> - ?v3. bir_eval_ifthenelse v v1 v2 v3 -Proof - rw [bir_eval_ifthenelse_eq_compute_ifthenelse] >> - Cases_on `v` >| [ - Cases_on `b` >> - Cases_on `c` >> - metis_tac [bir_compute_ifthenelse_def, bit1_is_boolean], - - fs [type_of_bir_val_def] - ] -QED - -(* Type conservation Theorem *) -Theorem bir_eval_ifthenelse_keep_type: - !v v1 v2 v3 ty. - bir_eval_ifthenelse v v1 v2 v3 ==> - (type_of_bir_val v1 = ty /\ type_of_bir_val v2 = ty) ==> - (type_of_bir_val v = (BType_Imm Bit1) <=> type_of_bir_val v3 = ty) -Proof - Cases_on `v` >> Cases_on `v1` >> Cases_on `v2` >> Cases_on `v3` >> - Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> Cases_on `b'''` >> - rw [type_of_bir_val_def, bir_eval_ifthenelse_cases, type_of_bir_imm_def, - birT_def, birF_def] -QED (* Number to Bitstring *) Definition n2bs_def: @@ -748,7 +486,6 @@ Definition v2bs_def: v2bs v s = n2bs (v2n v) s End - (* Immediate to number *) Definition b2n_def: (b2n ( Imm1 w ) = w2n w) /\ @@ -784,11 +521,9 @@ Definition bitstring_split_def: bitstring_split n bs = bitstring_split_aux n [] bs End - -(* ------------------------------------------ *) -(* ------------------ LOAD ------------------ *) -(* ------------------------------------------ *) - +Definition is_exp_well_typed_def: + is_exp_well_typed env exp = ?ty. type_of_bir_exp env exp ty +End (* Load a value from the mmap at the given address *) Definition bir_load_mmap_def: @@ -798,7 +533,6 @@ Definition bir_load_mmap_def: | SOME v => v End - (* Concatenate multiple bitstrings to a number on the correct number of bits *) Definition bir_mem_concat_def: bir_mem_concat vl rty = v2bs (FLAT vl) rty @@ -820,7 +554,6 @@ Definition bir_number_of_mem_splits_def: else NONE End - (* Load a bitstring at the given address from a mmap and pad it *) Definition bir_load_bitstring_from_mmap_def: bir_load_bitstring_from_mmap vty mmap (a:num) = @@ -833,7 +566,6 @@ Definition bir_load_splits_from_mmap_def: (MAP (\k. bir_load_bitstring_from_mmap vty mmap (bir_mem_addr aty (addr + k))) (COUNT_LIST n)) End - (* Eval an already unpacked load expression *) Inductive bir_eval_load_from_mem: [~BEnd_BigEndian:] @@ -864,35 +596,6 @@ Definition bir_eval_load_def: (bir_eval_load _ _ _ _ _ = F) End -(* Computes an already unpacked load expression *) -Definition bir_compute_load_from_mem_def: - bir_compute_load_from_mem - (vty : bir_immtype_t) (rty : bir_immtype_t) (aty : bir_immtype_t) (mmap : num |-> num) (en: bir_endian_t) (addr:num) = - - case (bir_number_of_mem_splits vty rty aty) of - | NONE => NONE - | SOME (n:num) => ( - let vs = bir_load_splits_from_mmap aty vty mmap addr n in - let vs' = (case en of BEnd_LittleEndian => SOME (REVERSE vs) - | BEnd_BigEndian => SOME vs - | BEnd_NoEndian => if (n = 1) then SOME vs else NONE) in - case vs' of NONE => NONE - | SOME vs'' => SOME (bir_mem_concat vs'' rty) - ) -End - -Definition bir_compute_load_def: - (bir_compute_load (SOME (BVal_Mem aty vty mmap)) (SOME (BVal_Imm addr)) en rty = - val_from_imm_option (bir_compute_load_from_mem vty rty aty mmap en (b2n addr))) /\ - (bir_compute_load _ _ _ _ = NONE) -End - - -(* ----------------------------------------- *) -(* ----------------- STORE ----------------- *) -(* ----------------------------------------- *) - - (* Add all the bitstrings in the mmap at address a *) Definition bir_update_mmap_def: (bir_update_mmap aty mmap a [] = mmap) /\ @@ -900,7 +603,6 @@ Definition bir_update_mmap_def: bir_update_mmap aty (FUPDATE mmap ((bir_mem_addr aty a), v2n v)) (SUC a) vs) End - Inductive bir_eval_store_in_mem: [~BEnd_BigEndian:] !vty aty result mmap addr ll. @@ -925,7 +627,6 @@ Inductive bir_eval_store_in_mem: ==> bir_eval_store_in_mem vty aty result mmap BEnd_NoEndian addr (BVal_Mem aty vty (bir_update_mmap aty mmap addr ll)) - End Definition bir_eval_store_def: @@ -934,248 +635,6 @@ Definition bir_eval_store_def: (bir_eval_store _ _ _ _ _ = F) End -(* Compute an already unpacked store expression *) -Definition bir_compute_store_in_mem_def: - bir_compute_store_in_mem - (vty : bir_immtype_t) (aty : bir_immtype_t) (result : bir_imm_t) (mmap : num |-> num) (en: bir_endian_t) (addr:num) = - - let rty = type_of_bir_imm result in - case (bir_number_of_mem_splits vty rty aty) of - | NONE => NONE - | SOME (n:num) => ( - case (bitstring_split (size_of_bir_immtype vty) (b2v result)) of - | NONE => NONE - | SOME vs => - let vs' = (case en of BEnd_LittleEndian => SOME (REVERSE vs) - | BEnd_BigEndian => SOME vs - | BEnd_NoEndian => if (n = 1) then SOME vs else NONE) in - - case vs' of NONE => NONE - | SOME vs'' => SOME (BVal_Mem aty vty (bir_update_mmap aty mmap addr vs'')) - ) -End - - -Definition bir_compute_store_def: - (bir_compute_store (SOME (BVal_Mem aty vty mmap)) (SOME (BVal_Imm addr)) en (SOME (BVal_Imm result)) = - bir_compute_store_in_mem vty aty result mmap en (b2n addr)) /\ - (bir_compute_store _ _ _ _ = NONE) -End - -Theorem size_of_bir_immtype_leq_1: - !b. 1 <= 2 ** (size_of_bir_immtype b) -Proof - Cases_on `b` >> - rw [size_of_bir_immtype_def] -QED - -(* Eval and compute are similar *) -Theorem bir_eval_load_eq_compute_load: - !v_mem v_addr en rty v. - bir_eval_load v_mem v_addr en rty v <=> - (bir_compute_load (SOME v_mem) (SOME v_addr) en rty = SOME v) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `en` >> - rw [bir_eval_load_def, bir_eval_load_from_mem_cases] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def] >> - CASE_TAC >> - simp [] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - - - -(* If the operands are correctly typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_load_bigendian: - !aty vty v_mem v_addr rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_load v_mem v_addr BEnd_BigEndian rty v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - rw [bir_eval_load_eq_compute_load] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - -Theorem type_of_bir_val_imp_bir_eval_load_littleendian: - !aty vty v_mem v_addr rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_load v_mem v_addr BEnd_LittleEndian rty v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - rw [bir_eval_load_eq_compute_load] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - rw [val_from_imm_option_def] >> - metis_tac [] -QED - -Theorem type_of_bir_val_imp_bir_eval_load_noendian: - !aty vty v_mem v_addr rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty)) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) = 1)) - ==> - ?v. bir_eval_load v_mem v_addr BEnd_NoEndian rty v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - rw [bir_eval_load_eq_compute_load] >> - rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - rw [val_from_imm_option_def] >> - metis_tac [size_of_bir_immtype_leq_1] -QED - - -(* Type of bir_mem_concat *) -Theorem type_of_bir_imm_bir_mem_concat: - !vl rty. type_of_bir_imm (bir_mem_concat vl rty) = rty -Proof - Cases_on `rty` >> - rw [bir_mem_concat_def, v2bs_def, n2bs_def] >> - rw [type_of_bir_imm_def] -QED - - -(* Type conservation theorem *) -Theorem bir_eval_load_correct_type: - !v_mem v_addr en rty v. - bir_eval_load v_mem v_addr en rty v ==> - (type_of_bir_val v = (BType_Imm rty)) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> - Cases_on `en` >> - - simp [bir_eval_load_def, bir_eval_load_from_mem_cases] >> - metis_tac [type_of_bir_val_def, type_of_bir_imm_def, type_of_bir_imm_bir_mem_concat] -QED - -(* bitstring_split will never be NONE *) -Theorem bitstring_split_aux_size_of_bir_immtype: - !ty acc bs. ?ll. bitstring_split_aux (size_of_bir_immtype ty) acc bs = SOME ll -Proof - gen_tac >> - `?n. size_of_bir_immtype ty = SUC n` by (Cases_on `ty` >> simp [size_of_bir_immtype_def]) >> - measureInduct_on `LENGTH bs` >> - Cases_on `bs` >> - fs [bitstring_split_def, bitstring_split_aux_def] >> - `LENGTH (DROP n t) < SUC (LENGTH t)` by rw [listTheory.LENGTH_DROP] >> - metis_tac [bitstring_split_aux_def, listTheory.LENGTH_DROP] -QED - -Theorem bitstring_split_size_of_bir_immtype: - !ty bs. bitstring_split (size_of_bir_immtype ty) bs <> NONE -Proof - simp [bitstring_split_def] >> - metis_tac [bitstring_split_aux_size_of_bir_immtype, optionTheory.NOT_SOME_NONE] -QED - -(* Eval and compute are similar *) -Theorem bir_eval_store_eq_compute_store: - !v_mem v_addr en result v. - bir_eval_store v_mem v_addr en result v <=> - (bir_compute_store (SOME v_mem) (SOME v_addr) en (SOME result) = SOME v) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `en` >> Cases_on `result` >> - rw [bir_eval_store_def, bir_eval_store_in_mem_cases] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def] >> - CASE_TAC >> CASE_TAC >> TRY CASE_TAC >> - simp [] >> - metis_tac [] -QED - -(* If the operands are correctly typed, then the expression evaluates *) -Theorem type_of_bir_val_imp_bir_eval_store_bigendian: - !aty vty v_mem v_addr v_result rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - (type_of_bir_val v_result = BType_Imm rty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_store v_mem v_addr BEnd_BigEndian v_result v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - rw [bir_eval_store_eq_compute_store] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - TRY CASE_TAC >> - fs [bitstring_split_size_of_bir_immtype, bitstring_split_def] >> - metis_tac [bitstring_split_aux_size_of_bir_immtype] -QED - -Theorem type_of_bir_val_imp_bir_eval_store_littleendian: - !aty vty v_mem v_addr v_result rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - (type_of_bir_val v_result = BType_Imm rty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty))) - ==> - ?v. bir_eval_store v_mem v_addr BEnd_LittleEndian v_result v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - rw [bir_eval_store_eq_compute_store] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - TRY CASE_TAC >> - fs [bitstring_split_size_of_bir_immtype] >> - metis_tac [] -QED - -Theorem type_of_bir_val_imp_bir_eval_store_noendian: - !aty vty v_mem v_addr v_result rty. - ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ - (type_of_bir_val v_addr = BType_Imm aty) /\ - (type_of_bir_val v_result = BType_Imm rty) /\ - ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= - 2 **(size_of_bir_immtype aty)) /\ - ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) = 1)) - ==> - ?v. bir_eval_store v_mem v_addr BEnd_NoEndian v_result v -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - rw [bir_eval_store_eq_compute_store] >> - rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> - fs [type_of_bir_val_def, type_of_bir_imm_def] >> - TRY CASE_TAC >> - fs [bitstring_split_size_of_bir_immtype] >> - metis_tac [size_of_bir_immtype_leq_1] -QED - -(* Type conservation theorem *) -Theorem bir_eval_store_correct_type: - !v_mem v_addr en v_result v. - bir_eval_store v_mem v_addr en v_result v ==> - (type_of_bir_val v = type_of_bir_val v_mem) -Proof - Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> - Cases_on `en` >> - - simp [bir_eval_store_def, bir_eval_store_in_mem_cases] >> - rw [type_of_bir_val_def, type_of_bir_imm_def] >> - metis_tac [type_of_bir_val_def, type_of_bir_imm_def] -QED - (** definitions *) (* defns bir_eval_exp *) @@ -1202,14 +661,14 @@ Inductive bir_eval_exp: (clause_name "Eval_BExp_BinExp") /\ (( ( bir_eval_exp env bir_exp1 bir_val1 )) /\ ( ( bir_eval_exp env bir_exp2 bir_val2 )) /\ -( (bir_eval_binexp bir_binexp bir_val1 bir_val2 bir_val ) )) +( ( bir_eval_binexp bir_binexp bir_val1 bir_val2 bir_val ))) ==> ( ( bir_eval_exp env (BExp_BinExp bir_binexp bir_exp1 bir_exp2) bir_val ))) [Eval_BExp_UnaryExp:] (! (env:bir_var_environment_t) (bir_unaryexp:bir_unaryexp_t) (bir_exp:bir_exp_t) (bir_val':bir_val_t) (bir_val:bir_val_t) . (clause_name "Eval_BExp_UnaryExp") /\ (( ( bir_eval_exp env bir_exp bir_val )) /\ -( (bir_eval_unaryexp bir_unaryexp bir_val bir_val' ) )) +( ( bir_eval_unaryexp bir_unaryexp bir_val bir_val' ))) ==> ( ( bir_eval_exp env (BExp_UnaryExp bir_unaryexp bir_exp) bir_val' ))) @@ -1217,7 +676,7 @@ Inductive bir_eval_exp: (clause_name "Eval_BExp_BinPred") /\ (( ( bir_eval_exp env bir_exp1 bir_val1 )) /\ ( ( bir_eval_exp env bir_exp2 bir_val2 )) /\ -( (bir_eval_binpred bir_binpred bir_val1 bir_val2 bir_val ) )) +( ( bir_eval_binpred bir_binpred bir_val1 bir_val2 bir_val ))) ==> ( ( bir_eval_exp env (BExp_BinPred bir_binpred bir_exp1 bir_exp2) bir_val ))) @@ -1226,7 +685,7 @@ Inductive bir_eval_exp: (( ( bir_eval_exp env bir_exp bir_val )) /\ ( ( bir_eval_exp env bir_exp1 bir_val1 )) /\ ( ( bir_eval_exp env bir_exp2 bir_val2 )) /\ -( (bir_eval_ifthenelse bir_val bir_val1 bir_val2 bir_val3 ) )) +( ( bir_eval_ifthenelse bir_val bir_val1 bir_val2 bir_val3 ))) ==> ( ( bir_eval_exp env (BExp_IfThenElse bir_exp bir_exp1 bir_exp2) bir_val3 ))) @@ -1247,6 +706,182 @@ Inductive bir_eval_exp: ==> ( ( bir_eval_exp env (BExp_Store bir_exp1 bir_exp2 bir_endian bir_exp3) bir_val ))) End +val _ = Hol_datatype ` +bir_label_t = (* Label values for jumps *) + BL_Label of ident + | BL_Address of bir_imm_t +`; +val _ = Hol_datatype ` +bir_label_exp_t = (* Label expressions that may be computed *) + BLE_Label of bir_label_t + | BLE_Exp of bir_exp_t +`; +val _ = Hol_datatype ` +bir_stmt_basic_t = (* Statements inside a program block *) + BStmt_Assign of bir_var_t => bir_exp_t +`; +val _ = Hol_datatype ` +bir_stmt_end_t = (* Statements at the end of a block *) + BStmt_Jmp of bir_label_exp_t + | BStmt_CJmp of bir_exp_t => bir_label_exp_t => bir_label_exp_t +`; +val _ = Hol_datatype ` +bir_stmt_t = (* General statement *) + BStmtB of bir_stmt_basic_t + | BStmtE of bir_stmt_end_t +`; + +(* Block type : a label, basic statements and an end statement *) +Datatype: + bir_block_t = <| + bb_label : bir_label_t; + bb_statements : bir_stmt_basic_t list; + bb_last_statement : bir_stmt_end_t |> +End + +(* Program counter : label of the current block and the offset inside the block *) +Datatype: + bir_programcounter_t = <| bpc_label:bir_label_t; bpc_index:num |> +End + +Type bir_block_t = ``:bir_block_t`` +val _ = Hol_datatype ` +bir_program_t = + BirProgram of bir_block_t list +`; +val _ = Hol_datatype ` +bir_status_t = (* Program state *) + BST_Running (* still running *) + | BST_TypeError (* execution encountered a type error *) + | BST_Failed (* execution failed *) + | BST_JumpOutside of bir_label_t (* execution jumped to unknown label *) +`; + +(* Program state *) +Datatype: + bir_state_t = <| + bst_pc : bir_programcounter_t; + bst_environ : bir_var_environment_t; + bst_status : bir_status_t +|> +End + +(* Increment a program counter *) +Definition bir_pc_next_def: + bir_pc_next pc = pc with bpc_index updated_by SUC +End + +(* Get the index and block at the given label *) +Definition bir_get_program_block_info_by_label_def: + bir_get_program_block_info_by_label + (BirProgram p) l = INDEX_FIND 0 (\(x:bir_block_t). x.bb_label = l) p +End + +(* Checks whether a state is still running *) +Definition bir_state_is_terminated_def: + bir_state_is_terminated st = + (st.bst_status <> BST_Running) +End + +(* Set the program state to Failed *) +Definition bir_state_set_failed_def: + bir_state_set_failed st = + (st with bst_status := BST_Failed) +End + +(* Set the program state to TypeError *) +Definition bir_state_set_typeerror_def: + bir_state_set_typeerror st = + (st with bst_status := BST_TypeError) +End + +(* Get the statement of a program at the given program counter *) +Definition bir_get_current_statement_def: + bir_get_current_statement p pc = + case (bir_get_program_block_info_by_label p pc.bpc_label) of + | NONE => NONE + | SOME (_, bl) => if (pc.bpc_index < LENGTH bl.bb_statements) + then SOME (BStmtB (EL (pc.bpc_index) bl.bb_statements)) + else (if pc.bpc_index = LENGTH bl.bb_statements + then SOME (BStmtE bl.bb_last_statement) + else NONE) +End + +(* Get all the labels of a program *) +Definition bir_labels_of_program_def: + bir_labels_of_program (BirProgram p) = + MAP (\bl. bl.bb_label) p +End + +Definition bir_stmts_of_block_def: + bir_stmts_of_block b = + (BStmtE b.bb_last_statement) :: MAP (\bst. (BStmtB bst)) b.bb_statements +End + +Definition bir_stmts_of_program_def: + bir_stmts_of_program (BirProgram blist) = + FLAT (MAP (\bl. bir_stmts_of_block bl) blist) +End + +(* Return the program counter at the start of the block *) +Definition bir_block_pc_def: + bir_block_pc l = <| bpc_label := l; bpc_index := 0 |> +End + +(* Increment pc in a state if necessary *) +Definition bir_state_next_def: + bir_state_next st = + if (bir_state_is_terminated st) then st else st with bst_pc updated_by bir_pc_next +End + +(* Jump to a label *) +Definition bir_jmp_to_label_def: + bir_jmp_to_label p + (l : bir_label_t) (st : bir_state_t) = + if (MEM l (bir_labels_of_program p)) then + st with bst_pc := bir_block_pc l + else (st with bst_status := (BST_JumpOutside l)) +End + +(* Eval a label expression *) +Definition bir_eval_label_exp_def: + (bir_eval_label_exp (BLE_Label l) env l' = (l = l')) /\ + (bir_eval_label_exp (BLE_Exp e) env (BL_Address i) = bir_eval_exp env e (BVal_Imm i)) /\ + (bir_eval_label_exp _ _ _ = F) +End + +(* Eval a basic statement *) +Definition bir_eval_stmtB_def: + (bir_eval_stmtB (BStmt_Assign v ex) st st' = + (?va. (bir_eval_exp st.bst_environ ex va) + /\ (st' = (st with bst_environ := (bir_env_update st.bst_environ v va))))) +End + +(* Eval a Jmp statement *) +Definition bir_eval_stmt_jmp_def: + bir_eval_stmt_jmp p le (st : bir_state_t) st' = + (?l. bir_eval_label_exp le st.bst_environ l + /\ bir_jmp_to_label p l st = st') +End + +(* Eval a CJmp statement *) +Definition bir_eval_stmt_cjmp_def: + bir_eval_stmt_cjmp p ec l1 l2 (st : bir_state_t) st' = + (if bir_eval_exp st.bst_environ ec birT then + bir_eval_stmt_jmp p l1 st st' + else if bir_eval_exp st.bst_environ ec birF then + bir_eval_stmt_jmp p l2 st st' + else F) +End + +(* Eval an end statement *) +Definition bir_eval_stmtE_def: + (bir_eval_stmtE p (BStmt_Jmp le) st st' = bir_eval_stmt_jmp p le st st') /\ + (bir_eval_stmtE p (BStmt_CJmp e l1 l2) st st' = bir_eval_stmt_cjmp p e l1 l2 st st') +End + + +Type bir_state_t = ``:bir_state_t`` val _ = export_theory (); diff --git a/examples/compute/src/theory/bir_computeScript.sml b/examples/compute/src/theory/bir_computeScript.sml index 4acd61228..b58656840 100644 --- a/examples/compute/src/theory/bir_computeScript.sml +++ b/examples/compute/src/theory/bir_computeScript.sml @@ -3,11 +3,138 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse bossLib boolLib; -open birTheory; - +open ottTheory birTheory; val _ = new_theory "bir_compute"; +(* Computes a binary expression of two immediates *) +Definition bir_compute_binexp_imm_def: + (bir_compute_binexp_imm BIExp_And (Imm1 w1) (Imm1 w2) = SOME (Imm1 (word_and w1 w2))) /\ + (bir_compute_binexp_imm BIExp_And (Imm8 w1) (Imm8 w2) = SOME (Imm8 (word_and w1 w2))) /\ + (bir_compute_binexp_imm BIExp_And (Imm16 w1) (Imm16 w2) = SOME (Imm16 (word_and w1 w2))) /\ + (bir_compute_binexp_imm BIExp_And (Imm32 w1) (Imm32 w2) = SOME (Imm32 (word_and w1 w2))) /\ + (bir_compute_binexp_imm BIExp_And (Imm64 w1) (Imm64 w2) = SOME (Imm64 (word_and w1 w2))) /\ + (bir_compute_binexp_imm BIExp_And (Imm128 w1) (Imm128 w2) = SOME (Imm128 (word_and w1 w2))) /\ + (bir_compute_binexp_imm BIExp_Plus (Imm1 w1) (Imm1 w2) = SOME (Imm1 (word_add w1 w2))) /\ + (bir_compute_binexp_imm BIExp_Plus (Imm8 w1) (Imm8 w2) = SOME (Imm8 (word_add w1 w2))) /\ + (bir_compute_binexp_imm BIExp_Plus (Imm16 w1) (Imm16 w2) = SOME (Imm16 (word_add w1 w2))) /\ + (bir_compute_binexp_imm BIExp_Plus (Imm32 w1) (Imm32 w2) = SOME (Imm32 (word_add w1 w2))) /\ + (bir_compute_binexp_imm BIExp_Plus (Imm64 w1) (Imm64 w2) = SOME (Imm64 (word_add w1 w2))) /\ + (bir_compute_binexp_imm BIExp_Plus (Imm128 w1) (Imm128 w2) = SOME (Imm128 (word_add w1 w2))) /\ + (bir_compute_binexp_imm binexp _ _ = NONE) +End + +(* Computes a general binary expression with values as parameters *) +Definition bir_compute_binexp_def: + (bir_compute_binexp binexp (SOME (BVal_Imm imm1)) (SOME (BVal_Imm imm2)) = + val_from_imm_option (bir_compute_binexp_imm binexp imm1 imm2)) /\ + (bir_compute_binexp _ _ _ = NONE) +End + +(* Computes a binary expression of an immediate *) +Definition bir_compute_unaryexp_imm_def: + (bir_compute_unaryexp_imm BIExp_Not (Imm1 w1) = SOME (Imm1 (word_1comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_Not (Imm8 w1) = SOME (Imm8 (word_1comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_Not (Imm16 w1) = SOME (Imm16 (word_1comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_Not (Imm32 w1) = SOME (Imm32 (word_1comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_Not (Imm64 w1) = SOME (Imm64 (word_1comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_Not (Imm128 w1) = SOME (Imm128 (word_1comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm1 w1) = SOME (Imm1 (word_2comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm8 w1) = SOME (Imm8 (word_2comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm16 w1) = SOME (Imm16 (word_2comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm32 w1) = SOME (Imm32 (word_2comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm64 w1) = SOME (Imm64 (word_2comp w1))) /\ + (bir_compute_unaryexp_imm BIExp_ChangeSign (Imm128 w1) = SOME (Imm128 (word_2comp w1))) +End + +(* Computes Unary expression *) +Definition bir_compute_unaryexp_def: + (bir_compute_unaryexp unaryexp (SOME (BVal_Imm imm1)) = + val_from_imm_option (bir_compute_unaryexp_imm unaryexp imm1)) /\ + (bir_compute_unaryexp _ _ = NONE) +End + +(* Computes a binary predicate of two immediates *) +Definition bir_compute_binpred_imm_def: + (bir_compute_binpred_imm BIExp_Equal (Imm1 w1) (Imm1 w2) = $= w1 w2) /\ + (bir_compute_binpred_imm BIExp_Equal (Imm8 w1) (Imm8 w2) = $= w1 w2) /\ + (bir_compute_binpred_imm BIExp_Equal (Imm16 w1) (Imm16 w2) = $= w1 w2) /\ + (bir_compute_binpred_imm BIExp_Equal (Imm32 w1) (Imm32 w2) = $= w1 w2) /\ + (bir_compute_binpred_imm BIExp_Equal (Imm64 w1) (Imm64 w2) = $= w1 w2) /\ + (bir_compute_binpred_imm BIExp_Equal (Imm128 w1) (Imm128 w2) = $= w1 w2) /\ + (bir_compute_binpred_imm BIExp_LessThan (Imm1 w1) (Imm1 w2) = word_lo w1 w2) /\ + (bir_compute_binpred_imm BIExp_LessThan (Imm8 w1) (Imm8 w2) = word_lo w1 w2) /\ + (bir_compute_binpred_imm BIExp_LessThan (Imm16 w1) (Imm16 w2) = word_lo w1 w2) /\ + (bir_compute_binpred_imm BIExp_LessThan (Imm32 w1) (Imm32 w2) = word_lo w1 w2) /\ + (bir_compute_binpred_imm BIExp_LessThan (Imm64 w1) (Imm64 w2) = word_lo w1 w2) /\ + (bir_compute_binpred_imm BIExp_LessThan (Imm128 w1) (Imm128 w2) = word_lo w1 w2) /\ + (bir_compute_binpred_imm binpred _ _ = F) +End + +(* Computes a general binary predicate with values as parameters *) +Definition bir_compute_binpred_def: + (bir_compute_binpred binpred (SOME (BVal_Imm imm1)) (SOME (BVal_Imm imm2)) = + SOME (BVal_Imm (bool2b (bir_compute_binpred_imm binpred imm1 imm2)))) /\ + (bir_compute_binpred _ _ _ = NONE) +End + +(* Computes an ifthenelse expression of two values *) +Definition bir_compute_ifthenelse_def: + bir_compute_ifthenelse b v1 v2 = + if b = SOME birT then v1 + else if b = SOME birF then v2 + else NONE +End + +(* Computes an already unpacked load expression *) +Definition bir_compute_load_from_mem_def: + bir_compute_load_from_mem + (vty : bir_immtype_t) (rty : bir_immtype_t) (aty : bir_immtype_t) (mmap : num |-> num) (en: bir_endian_t) (addr:num) = + + case (bir_number_of_mem_splits vty rty aty) of + | NONE => NONE + | SOME (n:num) => ( + let vs = bir_load_splits_from_mmap aty vty mmap addr n in + let vs' = (case en of BEnd_LittleEndian => SOME (REVERSE vs) + | BEnd_BigEndian => SOME vs + | BEnd_NoEndian => if (n = 1) then SOME vs else NONE) in + case vs' of NONE => NONE + | SOME vs'' => SOME (bir_mem_concat vs'' rty) + ) +End + +Definition bir_compute_load_def: + (bir_compute_load (SOME (BVal_Mem aty vty mmap)) (SOME (BVal_Imm addr)) en rty = + val_from_imm_option (bir_compute_load_from_mem vty rty aty mmap en (b2n addr))) /\ + (bir_compute_load _ _ _ _ = NONE) +End + +(* Compute an already unpacked store expression *) +Definition bir_compute_store_in_mem_def: + bir_compute_store_in_mem + (vty : bir_immtype_t) (aty : bir_immtype_t) (result : bir_imm_t) (mmap : num |-> num) (en: bir_endian_t) (addr:num) = + + let rty = type_of_bir_imm result in + case (bir_number_of_mem_splits vty rty aty) of + | NONE => NONE + | SOME (n:num) => ( + case (bitstring_split (size_of_bir_immtype vty) (b2v result)) of + | NONE => NONE + | SOME vs => + let vs' = (case en of BEnd_LittleEndian => SOME (REVERSE vs) + | BEnd_BigEndian => SOME vs + | BEnd_NoEndian => if (n = 1) then SOME vs else NONE) in + + case vs' of NONE => NONE + | SOME vs'' => SOME (BVal_Mem aty vty (bir_update_mmap aty mmap addr vs'')) + ) +End + +Definition bir_compute_store_def: + (bir_compute_store (SOME (BVal_Mem aty vty mmap)) (SOME (BVal_Imm addr)) en (SOME (BVal_Imm result)) = + bir_compute_store_in_mem vty aty result mmap en (b2n addr)) /\ + (bir_compute_store _ _ _ _ = NONE) +End (* General Computation function *) Definition bir_compute_exp_def: @@ -44,5 +171,106 @@ Definition bir_compute_exp_def: bir_compute_store (bir_compute_exp mem_e env) (bir_compute_exp a_e env) en (bir_compute_exp v_e env)) End +(* Eval and compute are similar *) +Theorem bir_eval_binexp_eq_compute_binexp: + !binexp v1 v2 v. bir_eval_binexp binexp v1 v2 v <=> + bir_compute_binexp binexp (SOME v1) (SOME v2) = SOME v +Proof + Cases_on `binexp` >> + Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> + rw [bir_eval_binexp_cases, bir_compute_binexp_def] >> + rw [bir_eval_binexp_imm_cases, bir_compute_binexp_imm_def] >> + Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> + rw [bir_compute_binexp_imm_def, fetch "bir" "bir_imm_t_nchotomy", bir_binexp_get_oper_def] >> + rw [val_from_imm_option_def,clause_name_def] >> + metis_tac [] +QED + +(* Eval and Compute are similar *) +Theorem bir_eval_unaryexp_eq_compute_unaryexp: + !unaryexp v1 v. bir_eval_unaryexp unaryexp v1 v <=> + bir_compute_unaryexp unaryexp (SOME v1) = SOME v +Proof + Cases_on `unaryexp` >> + Cases_on `v1` >> Cases_on `v` >> + rw [bir_eval_unaryexp_cases, bir_compute_unaryexp_def] >> + rw [bir_eval_unaryexp_imm_cases, bir_compute_unaryexp_imm_def] >> + Cases_on `b` >> Cases_on `b'` >> + rw [bir_compute_unaryexp_imm_def, fetch "bir" "bir_imm_t_nchotomy", bir_unaryexp_get_oper_def] >> + rw [val_from_imm_option_def,clause_name_def] >> + metis_tac [] +QED + +Theorem bir_eval_binpred_imp_compute_binpred: + !binpred v1 v2 v. bir_eval_binpred binpred v1 v2 v ==> + bir_compute_binpred binpred (SOME v1) (SOME v2) = SOME v +Proof + Cases_on `binpred` >> + Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> + rw [bir_eval_binpred_cases, bir_compute_binpred_def] >> + rw [bir_eval_binpred_imm_cases, bir_compute_binpred_imm_def] >> + Cases_on `b` >> Cases_on `b'` >> + rw [bool2b_def, bool2w_def, bir_compute_binpred_imm_def, fetch "bir" "bir_imm_t_nchotomy"] >> + fs [bir_eval_binpred_imm_cases, bir_binpred_get_oper_def] >> + metis_tac [] +QED + +(* If the term is well typed, then eval and compute are the same *) +Theorem well_typed_bir_eval_binpred_eq_compute_binpred: + !binpred v1 v2 v. + (type_of_bir_val v1 = type_of_bir_val v2) ==> + ( bir_eval_binpred binpred v1 v2 v <=> + bir_compute_binpred binpred (SOME v1) (SOME v2) = SOME v) +Proof + Cases_on `binpred` >> + Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> + rw [bir_eval_binpred_cases, bir_compute_binpred_def] >> + rw [bir_eval_binpred_imm_cases, bir_compute_binpred_imm_def] >> + Cases_on `b` >> Cases_on `b'` >> + rw [bool2b_def, bool2w_def, bir_compute_binpred_imm_def, fetch "bir" "bir_imm_t_nchotomy"] >> + fs [bir_eval_binpred_imm_cases, type_of_bir_val_def, + type_of_bir_imm_def, bir_binpred_get_oper_def,clause_name_def] >> + metis_tac [] +QED + +(* Eval and compute are similar *) +Theorem bir_eval_ifthenelse_eq_compute_ifthenelse: + !v (v1:bir_val_t) (v2:bir_val_t) (v3:bir_val_t). + (bir_eval_ifthenelse v v1 v2 v3 <=> + bir_compute_ifthenelse (SOME v) (SOME v1) (SOME v2) = SOME v3) +Proof + Cases_on `v` >> Cases_on `v1` >> Cases_on `v2` >> Cases_on `v3` >> + rw [bir_eval_ifthenelse_cases, bir_compute_ifthenelse_def, birT_def, birF_def,clause_name_def] >> + metis_tac [] +QED + +(* Eval and compute are similar *) +Theorem bir_eval_load_eq_compute_load: + !v_mem v_addr en rty v. + bir_eval_load v_mem v_addr en rty v <=> + (bir_compute_load (SOME v_mem) (SOME v_addr) en rty = SOME v) +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `en` >> + rw [bir_eval_load_def, bir_eval_load_from_mem_cases] >> + rw [bir_compute_load_def, bir_compute_load_from_mem_def] >> + CASE_TAC >> + simp [] >> + rw [val_from_imm_option_def] >> + metis_tac [] +QED + +(* Eval and compute are similar *) +Theorem bir_eval_store_eq_compute_store: + !v_mem v_addr en result v. + bir_eval_store v_mem v_addr en result v <=> + (bir_compute_store (SOME v_mem) (SOME v_addr) en (SOME result) = SOME v) +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `en` >> Cases_on `result` >> + rw [bir_eval_store_def, bir_eval_store_in_mem_cases] >> + rw [bir_compute_store_def, bir_compute_store_in_mem_def] >> + CASE_TAC >> CASE_TAC >> TRY CASE_TAC >> + simp [] >> + metis_tac [] +QED val _ = export_theory (); diff --git a/examples/compute/src/theory/bir_metaScript.sml b/examples/compute/src/theory/bir_metaScript.sml index ec434c48e..feb59d1bf 100644 --- a/examples/compute/src/theory/bir_metaScript.sml +++ b/examples/compute/src/theory/bir_metaScript.sml @@ -3,13 +3,381 @@ (* --------------------------------------------------------------------------- *) open HolKernel Parse boolLib bossLib; +open wordsTheory; open birTheory bir_computeTheory; open bir_programTheory bir_typing_programTheory; open ottTheory; - val _ = new_theory "bir_meta"; +(* Correction Theorems of boolean functions *) +Theorem bool2w_T_eq_birT: + BVal_Imm (Imm1 (bool2w T)) = birT +Proof + rw [bool2w_def, birT_def] +QED + +Theorem bool2w_F_eq_birF: + BVal_Imm (Imm1 (bool2w F)) = birF +Proof + rw [bool2w_def, birF_def] +QED + +(* 1 bit values are booleans *) +Theorem bit1_is_boolean: + !v. type_of_bir_val v = (BType_Imm Bit1) ==> (v = birT \/ v = birF) +Proof + Cases_on `v` >> + Cases_on `b` >> + rw [birT_def, birF_def, type_of_bir_val_def, type_of_bir_imm_def] >> + Cases_on `c` >> + fs [dimword_1] +QED + +Theorem size_of_bir_immtype_leq_1: + !b. 1 <= 2 ** (size_of_bir_immtype b) +Proof + Cases_on `b` >> + rw [size_of_bir_immtype_def] +QED + +Theorem bir_env_lookup_empty: + !var v. ~(bir_env_lookup_rel bir_empty_env var v) +Proof + Cases_on `var` >> + rw [bir_empty_env_def, bir_env_lookup_rel_def] +QED + +Theorem bir_env_lookup_rel_update: + !env var v. bir_env_lookup_rel (bir_env_update env var v) var v +Proof + Cases_on `var` >> Cases_on `env` >> + rw [bir_env_update_def, bir_env_lookup_rel_def] +QED + +Theorem bir_env_lookup_update: + !env var v. bir_env_lookup (bir_env_update env var v) var = SOME v +Proof + rpt gen_tac >> + Cases_on `var` >> Cases_on `env` >> + rw [bir_env_update_def, bir_env_lookup_def] +QED + +Theorem bir_env_lookup_update_neq: + !env var1 var2 v. + var1 <> var2 ==> + bir_env_lookup (bir_env_update env var1 v) var2 = bir_env_lookup env var2 +Proof + Cases_on `var1` >> Cases_on `var2` >> + rw [fetch "bir" "bir_var_t_11"] >> + Cases_on `env` >> + simp [bir_env_update_def] >> + rw [bir_env_lookup_def] >> + EVAL_TAC >> + metis_tac [] +QED + +(* Lookup and relation are the same *) +Theorem bir_env_lookup_eq_rel: + !env var v. bir_env_lookup_rel env var v <=> bir_env_lookup env var = SOME v +Proof + rpt strip_tac >> + Cases_on `env` >> + Cases_on `var` >> + rw [bir_env_lookup_def, bir_env_lookup_rel_def] +QED + +(* Injective *) +Theorem bir_env_lookup_rel_inj: + !env var v1 v2. + bir_env_lookup_rel env var v1 ==> + bir_env_lookup_rel env var v2 ==> + v1 = v2 +Proof + Cases_on `env` >> Cases_on `var` >> + simp [bir_env_lookup_rel_def] +QED + +(* bitstring_split will never be NONE *) +Theorem bitstring_split_aux_size_of_bir_immtype: + !ty acc bs. ?ll. bitstring_split_aux (size_of_bir_immtype ty) acc bs = SOME ll +Proof + gen_tac >> + `?n. size_of_bir_immtype ty = SUC n` by (Cases_on `ty` >> simp [size_of_bir_immtype_def]) >> + measureInduct_on `LENGTH bs` >> + Cases_on `bs` >> + fs [bitstring_split_def, bitstring_split_aux_def] >> + `LENGTH (DROP n t) < SUC (LENGTH t)` by rw [listTheory.LENGTH_DROP] >> + metis_tac [bitstring_split_aux_def, listTheory.LENGTH_DROP] +QED + +Theorem bitstring_split_size_of_bir_immtype: + !ty bs. bitstring_split (size_of_bir_immtype ty) bs <> NONE +Proof + simp [bitstring_split_def] >> + metis_tac [bitstring_split_aux_size_of_bir_immtype, optionTheory.NOT_SOME_NONE] +QED + +(* If the operands are typed, then the expression evaluates *) +Theorem type_of_bir_val_imp_bir_eval_binexp: + !binexp v1 v2 ty. + ((type_of_bir_val v1 = BType_Imm ty) /\ (type_of_bir_val v2 = BType_Imm ty)) ==> + ?v. bir_eval_binexp binexp v1 v2 v +Proof + Cases_on `binexp` >> + Cases_on `v1` >> Cases_on `v2` >> + Cases_on `b` >> Cases_on `b'` >> + rw [bir_eval_binexp_eq_compute_binexp] >> + rw [bir_compute_binexp_def, bir_compute_binexp_imm_def] >> + rw [val_from_imm_option_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] +QED + +(* Type conservation Theorem *) +Theorem bir_eval_binexp_keep_type: + !binexp v1 v2 v ty. + bir_eval_binexp binexp v1 v2 v ==> + ((type_of_bir_val v1 = ty /\ type_of_bir_val v2 = ty) <=> + type_of_bir_val v = ty) +Proof + Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> + Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> + rw [type_of_bir_val_def, bir_eval_binexp_cases, type_of_bir_imm_def, bir_eval_binexp_imm_cases] +QED + +(* Unary_exp always evaluates *) +Theorem type_of_bir_val_imp_bir_eval_unaryexp: + !unaryexp v ty. + (type_of_bir_val v = BType_Imm ty) ==> + ?v'. bir_eval_unaryexp unaryexp v v' +Proof + Cases_on `unaryexp` >> + Cases_on `v` >> + Cases_on `b` >> + rw [bir_eval_unaryexp_eq_compute_unaryexp, type_of_bir_val_def] >> + rw [bir_compute_unaryexp_def, bir_compute_unaryexp_imm_def] >> + rw [val_from_imm_option_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] +QED + +(* Type conservation theorem *) +Theorem bir_eval_unaryexp_keep_type: + !unaryexp v1 v2 ty. + bir_eval_unaryexp unaryexp v1 v2 ==> + (type_of_bir_val v1 = type_of_bir_val v2) +Proof + Cases_on `v1` >> Cases_on `v2` >> + Cases_on `b` >> Cases_on `b'` >> + rw [type_of_bir_val_def, bir_eval_unaryexp_cases, type_of_bir_imm_def, bir_eval_unaryexp_imm_cases] +QED + +(* If the operands are typed, then the expression evaluates *) +Theorem type_of_bir_val_imp_bir_eval_binpred: + !binpred v1 v2 ty. + ((type_of_bir_val v1 = BType_Imm ty) /\ (type_of_bir_val v2 = BType_Imm ty)) ==> + ?v. bir_eval_binpred binpred v1 v2 v +Proof + Cases_on `v1` >> Cases_on `v2` >> + Cases_on `b` >> Cases_on `b'` >> + rw [well_typed_bir_eval_binpred_eq_compute_binpred] >> + rw [bir_compute_binpred_def, bir_compute_binpred_imm_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] +QED + +(* Type conservation theorem *) +Theorem bir_eval_binpred_correct_type: + !binpred v1 v2 v ty. + bir_eval_binpred binpred v1 v2 v ==> + ((type_of_bir_val v1 = type_of_bir_val v2) /\ type_of_bir_val v = (BType_Imm Bit1)) +Proof + Cases_on `v1` >> Cases_on `v2` >> Cases_on `v` >> + Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> + rw [type_of_bir_val_def, bir_eval_binpred_cases, type_of_bir_imm_def, bir_eval_binpred_imm_cases, bool2b_def] +QED + +(* If the condition is typed, then the expression evaluates *) +Theorem type_of_bir_val_imp_bir_eval_ifthenelse: + !v v1 v2. + (type_of_bir_val v = (BType_Imm Bit1)) ==> + ?v3. bir_eval_ifthenelse v v1 v2 v3 +Proof + rw [bir_eval_ifthenelse_eq_compute_ifthenelse] >> + Cases_on `v` >| [ + Cases_on `b` >> + Cases_on `c` >> + metis_tac [bir_compute_ifthenelse_def, bit1_is_boolean], + + fs [type_of_bir_val_def] + ] +QED + +(* Type conservation Theorem *) +Theorem bir_eval_ifthenelse_keep_type: + !v v1 v2 v3 ty. + bir_eval_ifthenelse v v1 v2 v3 ==> + (type_of_bir_val v1 = ty /\ type_of_bir_val v2 = ty) ==> + (type_of_bir_val v = (BType_Imm Bit1) <=> type_of_bir_val v3 = ty) +Proof + Cases_on `v` >> Cases_on `v1` >> Cases_on `v2` >> Cases_on `v3` >> + Cases_on `b` >> Cases_on `b'` >> Cases_on `b''` >> Cases_on `b'''` >> + rw [type_of_bir_val_def, bir_eval_ifthenelse_cases, type_of_bir_imm_def, + birT_def, birF_def] +QED + +(* If the operands are correctly typed, then the expression evaluates *) +Theorem type_of_bir_val_imp_bir_eval_load_bigendian: + !aty vty v_mem v_addr rty. + ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ + (type_of_bir_val v_addr = BType_Imm aty) /\ + ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= + 2 **(size_of_bir_immtype aty))) + ==> + ?v. bir_eval_load v_mem v_addr BEnd_BigEndian rty v +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> + rw [bir_eval_load_eq_compute_load] >> + rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] >> + rw [val_from_imm_option_def] >> + metis_tac [] +QED + +Theorem type_of_bir_val_imp_bir_eval_load_littleendian: + !aty vty v_mem v_addr rty. + ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ + (type_of_bir_val v_addr = BType_Imm aty) /\ + ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= + 2 **(size_of_bir_immtype aty))) + ==> + ?v. bir_eval_load v_mem v_addr BEnd_LittleEndian rty v +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> + rw [bir_eval_load_eq_compute_load] >> + rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] >> + rw [val_from_imm_option_def] >> + metis_tac [] +QED + +Theorem type_of_bir_val_imp_bir_eval_load_noendian: + !aty vty v_mem v_addr rty. + ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ + (type_of_bir_val v_addr = BType_Imm aty) /\ + ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= + 2 **(size_of_bir_immtype aty)) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) = 1)) + ==> + ?v. bir_eval_load v_mem v_addr BEnd_NoEndian rty v +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> + rw [bir_eval_load_eq_compute_load] >> + rw [bir_compute_load_def, bir_compute_load_from_mem_def, bir_number_of_mem_splits_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] >> + rw [val_from_imm_option_def] >> + metis_tac [size_of_bir_immtype_leq_1] +QED + + +(* Type of bir_mem_concat *) +Theorem type_of_bir_imm_bir_mem_concat: + !vl rty. type_of_bir_imm (bir_mem_concat vl rty) = rty +Proof + Cases_on `rty` >> + rw [bir_mem_concat_def, v2bs_def, n2bs_def] >> + rw [type_of_bir_imm_def] +QED + +(* Type conservation theorem *) +Theorem bir_eval_load_correct_type: + !v_mem v_addr en rty v. + bir_eval_load v_mem v_addr en rty v ==> + (type_of_bir_val v = (BType_Imm rty)) +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> + Cases_on `en` >> + + simp [bir_eval_load_def, bir_eval_load_from_mem_cases] >> + metis_tac [type_of_bir_val_def, type_of_bir_imm_def, type_of_bir_imm_bir_mem_concat] +QED + +(* If the operands are correctly typed, then the expression evaluates *) +Theorem type_of_bir_val_imp_bir_eval_store_bigendian: + !aty vty v_mem v_addr v_result rty. + ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ + (type_of_bir_val v_addr = BType_Imm aty) /\ + (type_of_bir_val v_result = BType_Imm rty) /\ + ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= + 2 **(size_of_bir_immtype aty))) + ==> + ?v. bir_eval_store v_mem v_addr BEnd_BigEndian v_result v +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> + rw [bir_eval_store_eq_compute_store] >> + rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] >> + TRY CASE_TAC >> + fs [bitstring_split_size_of_bir_immtype, bitstring_split_def] >> + metis_tac [bitstring_split_aux_size_of_bir_immtype] +QED + +Theorem type_of_bir_val_imp_bir_eval_store_littleendian: + !aty vty v_mem v_addr v_result rty. + ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ + (type_of_bir_val v_addr = BType_Imm aty) /\ + (type_of_bir_val v_result = BType_Imm rty) /\ + ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= + 2 **(size_of_bir_immtype aty))) + ==> + ?v. bir_eval_store v_mem v_addr BEnd_LittleEndian v_result v +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> + rw [bir_eval_store_eq_compute_store] >> + rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] >> + TRY CASE_TAC >> + fs [bitstring_split_size_of_bir_immtype] >> + metis_tac [] +QED + +Theorem type_of_bir_val_imp_bir_eval_store_noendian: + !aty vty v_mem v_addr v_result rty. + ((type_of_bir_val v_mem = (BType_Mem aty vty)) /\ + (type_of_bir_val v_addr = BType_Imm aty) /\ + (type_of_bir_val v_result = BType_Imm rty) /\ + ((size_of_bir_immtype rty) MOD (size_of_bir_immtype vty) = 0) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) <= + 2 **(size_of_bir_immtype aty)) /\ + ((size_of_bir_immtype rty) DIV (size_of_bir_immtype vty) = 1)) + ==> + ?v. bir_eval_store v_mem v_addr BEnd_NoEndian v_result v +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> + rw [bir_eval_store_eq_compute_store] >> + rw [bir_compute_store_def, bir_compute_store_in_mem_def, bir_number_of_mem_splits_def] >> + fs [type_of_bir_val_def, type_of_bir_imm_def] >> + TRY CASE_TAC >> + fs [bitstring_split_size_of_bir_immtype] >> + metis_tac [size_of_bir_immtype_leq_1] +QED + +(* Type conservation theorem *) +Theorem bir_eval_store_correct_type: + !v_mem v_addr en v_result v. + bir_eval_store v_mem v_addr en v_result v ==> + (type_of_bir_val v = type_of_bir_val v_mem) +Proof + Cases_on `v_mem` >> Cases_on `v_addr` >> Cases_on `v_result` >> + Cases_on `en` >> + + simp [bir_eval_store_def, bir_eval_store_in_mem_cases] >> + rw [type_of_bir_val_def, type_of_bir_imm_def] >> + metis_tac [type_of_bir_val_def, type_of_bir_imm_def] +QED (* ----------------------------------------------- *) (* --------------------- EXP --------------------- *) @@ -37,11 +405,11 @@ Proof (* BExp_BinExp *) simp [Once type_of_bir_exp_cases, Once bir_eval_exp_cases, type_of_bir_val_def] >> - metis_tac [bir_eval_binexp_def, bir_eval_binexp_keep_type, type_of_bir_val_def], + metis_tac [bir_eval_binexp_cases, bir_eval_binexp_keep_type, type_of_bir_val_def], (* BExp_UnaryExp *) simp [Once type_of_bir_exp_cases, Once bir_eval_exp_cases, type_of_bir_val_def] >> - metis_tac [bir_eval_unaryexp_def, bir_eval_unaryexp_keep_type, type_of_bir_val_def], + metis_tac [bir_eval_unaryexp_cases, bir_eval_unaryexp_keep_type, type_of_bir_val_def], (* BExp_BinPred *) simp [Once type_of_bir_exp_cases, Once bir_eval_exp_cases, type_of_bir_val_def] >> @@ -130,8 +498,6 @@ Proof ] QED - - (* Eval and compute are similar *) Theorem bir_eval_exp_eq_compute_exp: !env e v ty. type_of_bir_exp env e ty ==> @@ -191,7 +557,7 @@ Proof Cases_on `bir_compute_exp e'' (BEnv f)` >> rw [Once type_of_bir_exp_cases, bir_compute_ifthenelse_def] >> metis_tac [well_typed_bir_eval_exp_value, bir_eval_ifthenelse_eq_compute_ifthenelse, - bir_eval_exp_correct_type, bir_eval_ifthenelse_cases], + bir_eval_exp_correct_type, bir_eval_ifthenelse_cases,clause_name_def], (* BExp_Load *) simp [Once bir_eval_exp_cases, bir_compute_exp_def,clause_name_def] >> @@ -327,7 +693,6 @@ Proof ] QED - Theorem bir_eval_step_eq_compute_step: !p st st'. (~bir_state_is_terminated st) ==> @@ -348,6 +713,4 @@ Proof ] QED - - val _ = export_theory (); diff --git a/examples/compute/src/theory/bir_programScript.sml b/examples/compute/src/theory/bir_programScript.sml index 3fa03937f..ac9ca7069 100644 --- a/examples/compute/src/theory/bir_programScript.sml +++ b/examples/compute/src/theory/bir_programScript.sml @@ -8,177 +8,8 @@ open birTheory; open bir_computeTheory; open listTheory; - val _ = new_theory "bir_program"; - -(* Label values for jumps *) -Datatype: - bir_label_t = - BL_Label string - | BL_Address bir_imm_t -End - -(* Label expressions that may be computed *) -Datatype: - bir_label_exp_t = - BLE_Label bir_label_t - | BLE_Exp bir_exp_t -End - - - -(* Statements inside a program block *) -Datatype: - bir_stmt_basic_t = - | BStmt_Assign bir_var_t bir_exp_t -End - -(* Statements at the end of a block *) -Datatype: - bir_stmt_end_t = - | BStmt_Jmp bir_label_exp_t - | BStmt_CJmp bir_exp_t bir_label_exp_t bir_label_exp_t -End - -(* General statement type *) -Datatype: - bir_stmt_t = - | BStmtB bir_stmt_basic_t - | BStmtE bir_stmt_end_t -End - - - -(* Block type : a label, basic statements and an end statement *) -Datatype: - bir_block_t = <| - bb_label : bir_label_t; - bb_statements : bir_stmt_basic_t list; - bb_last_statement : bir_stmt_end_t |> -End - -(* A program : a list of blocks *) -Datatype: - bir_program_t = BirProgram (bir_block_t list) -End - -(* Program counter : label of the current block and the offset inside the block *) -Datatype: - bir_programcounter_t = <| bpc_label:bir_label_t; bpc_index:num |> -End - - -(* Program state *) -Datatype: - bir_status_t = - BST_Running (* BIR program is still running *) - | BST_TypeError (* BIR program execution encountered a type error *) - | BST_Failed (* BIR program execution failed, should not happen when starting in a state where pc is available in the program to execute *) - | BST_JumpOutside bir_label_t (* Jump to unknown label *) -End - -Datatype: - bir_state_t = <| - bst_pc : bir_programcounter_t; - bst_environ : bir_var_environment_t; - bst_status : bir_status_t -|> -End - - -(* ----------------------------------------------- *) -(* ----------------- DEFINITIONS ----------------- *) -(* ----------------------------------------------- *) - - -(* Increment a program counter *) -Definition bir_pc_next_def: - bir_pc_next pc = pc with bpc_index updated_by SUC -End - -(* Get the index and block at the given label *) -Definition bir_get_program_block_info_by_label_def: - bir_get_program_block_info_by_label - (BirProgram p) l = INDEX_FIND 0 (\(x:bir_block_t). x.bb_label = l) p -End - -(* Checks whether a state is still running *) -Definition bir_state_is_terminated_def: - bir_state_is_terminated st = - (st.bst_status <> BST_Running) -End - -(* Set the program state to Failed *) -Definition bir_state_set_failed_def: - bir_state_set_failed st = - (st with bst_status := BST_Failed) -End - -(* Set the program state to TypeError *) -Definition bir_state_set_typeerror_def: - bir_state_set_typeerror st = - (st with bst_status := BST_TypeError) -End - -(* Get the statement of a program at the given program counter *) -Definition bir_get_current_statement_def: - bir_get_current_statement p pc = - case (bir_get_program_block_info_by_label p pc.bpc_label) of - | NONE => NONE - | SOME (_, bl) => if (pc.bpc_index < LENGTH bl.bb_statements) - then SOME (BStmtB (EL (pc.bpc_index) bl.bb_statements)) - else (if pc.bpc_index = LENGTH bl.bb_statements - then SOME (BStmtE bl.bb_last_statement) - else NONE) -End - -(* Get all the labels of a program *) -Definition bir_labels_of_program_def: - bir_labels_of_program (BirProgram p) = - MAP (\bl. bl.bb_label) p -End - -Definition bir_stmts_of_block_def: - bir_stmts_of_block b = - (BStmtE b.bb_last_statement) :: MAP (\bst. (BStmtB bst)) b.bb_statements -End - -Definition bir_stmts_of_program_def: - bir_stmts_of_program (BirProgram blist) = - FLAT (MAP (\bl. bir_stmts_of_block bl) blist) -End - -(* Return the program counter at the start of the block *) -Definition bir_block_pc_def: - bir_block_pc l = <| bpc_label := l; bpc_index := 0 |> -End - -(* Increment pc in a state if necessary *) -Definition bir_state_next_def: - bir_state_next st = - if (bir_state_is_terminated st) then st else st with bst_pc updated_by bir_pc_next -End - -(* Jump to a label *) -Definition bir_jmp_to_label_def: - bir_jmp_to_label p - (l : bir_label_t) (st : bir_state_t) = - if (MEM l (bir_labels_of_program p)) then - st with bst_pc := bir_block_pc l - else (st with bst_status := (BST_JumpOutside l)) -End - - -(* ----------------------------------------------- *) -(* ------------------- COMPUTE ------------------- *) -(* ----------------------------------------------- *) - - -(* ----------------------------------------------- *) -(* ------------------- LABELS -------------------- *) -(* ----------------------------------------------- *) - (* Compute a label expression *) Definition bir_compute_label_exp_def: (bir_compute_label_exp (BLE_Label l) env = SOME l) /\ @@ -188,12 +19,6 @@ Definition bir_compute_label_exp_def: ) End - -(* ----------------------------------------------- *) -(* --------------- BASIC STATEMENTS -------------- *) -(* ----------------------------------------------- *) - - (* Compute an Assign statement *) Definition bir_compute_stmt_assign_def: bir_compute_stmt_assign v ex (st : bir_state_t) = @@ -207,11 +32,6 @@ Definition bir_compute_stmtB_def: (bir_compute_stmtB (BStmt_Assign v ex) st = (bir_compute_stmt_assign v ex st)) End -(* ----------------------------------------------- *) -(* --------------- END STATEMENTS ---------------- *) -(* ----------------------------------------------- *) - - (* Compute a Jmp statement *) Definition bir_compute_stmt_jmp_def: bir_compute_stmt_jmp p le (st : bir_state_t) = @@ -238,10 +58,6 @@ Definition bir_compute_stmtE_def: (bir_compute_stmtE p (BStmt_CJmp e l1 l2) st = bir_compute_stmt_cjmp p e l1 l2 st) End -(* ----------------------------------------------- *) -(* ----------------- STATEMENTS ------------------ *) -(* ----------------------------------------------- *) - (* Execute a statement given a program and a state *) Definition bir_compute_stmt_def: (bir_compute_stmt (p:bir_program_t) (BStmtB (bst:bir_stmt_basic_t)) st = @@ -258,69 +74,6 @@ Definition bir_compute_step_def: | SOME stm => (bir_compute_stmt p stm state) End - -(* ----------------------------------------------- *) -(* --------------------- EVAL -------------------- *) -(* ----------------------------------------------- *) - -(* ----------------------------------------------- *) -(* ------------------- LABELS -------------------- *) -(* ----------------------------------------------- *) - -(* Eval a label expression *) -Definition bir_eval_label_exp_def: - (bir_eval_label_exp (BLE_Label l) env l' = (l = l')) /\ - (bir_eval_label_exp (BLE_Exp e) env (BL_Address i) = bir_eval_exp env e (BVal_Imm i)) /\ - (bir_eval_label_exp _ _ _ = F) -End - - - -(* ----------------------------------------------- *) -(* --------------- BASIC STATEMENTS -------------- *) -(* ----------------------------------------------- *) - - -(* Eval a basic statement *) -Definition bir_eval_stmtB_def: - (bir_eval_stmtB (BStmt_Assign v ex) st st' = - (?va. (bir_eval_exp st.bst_environ ex va) - /\ (st' = (st with bst_environ := (bir_env_update st.bst_environ v va))))) -End - -(* ----------------------------------------------- *) -(* --------------- END STATEMENTS ---------------- *) -(* ----------------------------------------------- *) - - -(* Eval a Jmp statement *) -Definition bir_eval_stmt_jmp_def: - bir_eval_stmt_jmp p le (st : bir_state_t) st' = - (?l. bir_eval_label_exp le st.bst_environ l - /\ bir_jmp_to_label p l st = st') -End - -(* Eval a CJmp statement *) -Definition bir_eval_stmt_cjmp_def: - bir_eval_stmt_cjmp p ec l1 l2 (st : bir_state_t) st' = - (if bir_eval_exp st.bst_environ ec birT then - bir_eval_stmt_jmp p l1 st st' - else if bir_eval_exp st.bst_environ ec birF then - bir_eval_stmt_jmp p l2 st st' - else F) -End - -(* Eval an end statement *) -Definition bir_eval_stmtE_def: - (bir_eval_stmtE p (BStmt_Jmp le) st st' = bir_eval_stmt_jmp p le st st') /\ - (bir_eval_stmtE p (BStmt_CJmp e l1 l2) st st' = bir_eval_stmt_cjmp p e l1 l2 st st') -End - - -(* ----------------------------------------------- *) -(* ----------------- STATEMENTS ------------------ *) -(* ----------------------------------------------- *) - Inductive bir_eval_step: [~BStmtB:] !p state bst. @@ -346,8 +99,6 @@ Inductive bir_eval_step: (bir_eval_step p state (bir_state_set_failed state)) End - - (* ----------------------------------------------- *) (* ------------------ THEOREMS ------------------- *) (* ----------------------------------------------- *) diff --git a/examples/compute/src/theory/bir_programSyntax.sml b/examples/compute/src/theory/bir_programSyntax.sml index 77cca891d..fff54b155 100644 --- a/examples/compute/src/theory/bir_programSyntax.sml +++ b/examples/compute/src/theory/bir_programSyntax.sml @@ -24,12 +24,12 @@ fun dest_tri_record (ty : hol_type) (err : exn) (tm: term) = | _ => raise err end -val le_label_tm = prim_mk_const{Name="BLE_Label", Thy="bir_program"}; -val le_exp_tm = prim_mk_const{Name="BLE_Exp", Thy="bir_program"}; -val stmt_assign_tm = prim_mk_const{Name="BStmt_Assign", Thy="bir_program"}; -val stmt_jmp_tm = prim_mk_const{Name="BStmt_Jmp", Thy="bir_program"}; -val stmt_cjmp_tm = prim_mk_const{Name="BStmt_CJmp", Thy="bir_program"}; -val program_tm = prim_mk_const{Name="BirProgram", Thy="bir_program"}; +val le_label_tm = prim_mk_const{Name="BLE_Label", Thy="bir"}; +val le_exp_tm = prim_mk_const{Name="BLE_Exp", Thy="bir"}; +val stmt_assign_tm = prim_mk_const{Name="BStmt_Assign", Thy="bir"}; +val stmt_jmp_tm = prim_mk_const{Name="BStmt_Jmp", Thy="bir"}; +val stmt_cjmp_tm = prim_mk_const{Name="BStmt_CJmp", Thy="bir"}; +val program_tm = prim_mk_const{Name="BirProgram", Thy="bir"}; fun mk_le_label tm = diff --git a/examples/compute/test-compute.sml b/examples/compute/test-compute.sml index b3abd2e1f..50d56ad64 100644 --- a/examples/compute/test-compute.sml +++ b/examples/compute/test-compute.sml @@ -3,7 +3,7 @@ (* ------------------------------------------------------------------------- *) open HolKernel Parse bossLib boolLib; -open ottTheory birTheory; +open ottTheory birTheory bir_metaTheory; open bir_cv_basicLib; open bir_cv_envLib; open bir_cv_programLib; @@ -64,8 +64,8 @@ val _ = prove (`` (BExp_BinExp BIExp_Plus (BExp_Const (Imm64 imm1)) (BExp_Const (Imm64 imm2))) (BVal_Imm (Imm64 (imm1 + imm2)))``, - rw [Ntimes bir_eval_exp_cases 3, bir_eval_binexp_def, bir_eval_binexp_imm_cases, bir_binexp_get_oper_def] >> - rw [Once bir_eval_exp_cases, bir_eval_binexp_def, bir_eval_binexp_imm_cases, bir_binexp_get_oper_def,clause_name_def]); + rw [Ntimes bir_eval_exp_cases 3, bir_eval_binexp_cases, bir_eval_binexp_imm_cases, bir_binexp_get_oper_def] >> + rw [Once bir_eval_exp_cases, bir_eval_binexp_cases, bir_eval_binexp_imm_cases, bir_binexp_get_oper_def,clause_name_def]); (* ------------------------------------------------- *) @@ -77,8 +77,8 @@ val _ = prove (`` !env v. bir_eval_binpred BIExp_Equal (BVal_Imm v) (BVal_Imm v) birT``, Cases_on `v` >> - rw [Once bir_eval_binpred_cases, bir_eval_binpred_imm_cases, bir_binpred_get_oper_def] >> - rw [bool2b_T_eq_birT, bool2b_F_eq_birF]); + rw [Once bir_eval_binpred_cases, bir_eval_binpred_imm_cases, bir_binpred_get_oper_def,clause_name_def] >> + rw [bool2w_T_eq_birT, bool2w_F_eq_birF]); (* ------------------------------------------------- *)