| Example verifier that only supports memory operations that use the stack |
Require Import List TheoryList.
Require Import Asm.Util.ArithUtil.
Require Import Asm.Bitvector.Bitvector.
Require Import Asm.X86.X86.
Require Import ProofOS.AbsInt.Sal.
Require Import ProofOS.AbsInt.TypeSystem.
Require Import ProofOS.AbsInt.StackTypes.
Require Import ProofOS.AbsInt.TopOnly.
Set Implicit Arguments.
Module Type VANILLA_PARAM.
Parameter minitMem : mem.
Parameter codeStart : int32.
Parameter codeLength : nat.
Axiom codeHigh : bvec_to_nat codeStart >= 4.
Axiom codeFits : bvec_to_nat codeStart + codeLength < pow2 32 - 3.
Axiom codeBigEnough : longestInstr + 1 <= codeLength.
Parameter stackStart : int32.
Parameter stackLength : nat.
Axiom stackHigh : bvec_to_nat stackStart >= 4.
Axiom stackBig : stackLength > 8.
Axiom stackFits : bvec_to_nat stackStart + stackLength < pow2 32 - 3.
Axiom stackCodeSeparate : disjointRegions codeStart codeLength stackStart stackLength.
Axiom stackLongEnough : stackLength >= 4.
End VANILLA_PARAM.
Module Verifier (Param : VANILLA_PARAM).
Import Param.
Module StackParam <: M86_PARAM_FIXED_CODE_AND_STACK.
Definition minitState st := stPc st = codeStart /\ stMem st = minitMem.
Definition minitMem := minitMem.
Definition codeStart := codeStart.
Definition codeLength := codeLength.
Definition codeHigh := codeHigh.
Definition codeFits := codeFits.
Theorem pcInRange : forall st, minitState st
-> bvec_to_nat codeStart
<= bvec_to_nat (stPc st)
< bvec_to_nat codeStart + codeLength - longestInstr.
Theorem codeUniform : forall st, minitState st
-> agree_range (stMem st) minitMem codeStart codeLength.
Definition stackStart := stackStart.
Definition stackLength := stackLength.
Definition stackHigh := stackHigh.
Definition stackFits := stackFits.
Definition stackCodeSeparate := stackCodeSeparate.
End StackParam.
Module TopOnly := TopOnly.Make(StackParam).
Import TopOnly.
Import Stack.
Import TySys.
Import Fixed.
Import MySal.
Specify the root states for a verification |
Module Type ROOT_STATES.
Parameter roots : {rs : list (list (stateDescription (stackTy (option int32)) (stackState (option int32) unit))
* stateDescription (stackTy (option int32)) (stackState (option int32) unit))
| AllS (fun sd => match sdPc (snd sd) with
| ApcUnknown => False
| ApcConst pc => validPc pc
end) rs}.
Parameters functions : list (function_info (stackTy (option int32))).
End ROOT_STATES.
Module Make (Roots : ROOT_STATES).
Import Roots.
Module MyTypeSystemPlus <: TYPE_SYSTEM_WITH_FUNCTIONS.
Module Sys := MyTypeSystem.
Definition functions := functions.
End MyTypeSystemPlus.
Module TypeSystem := Stack.AddStackTypes(MyTypeSystemPlus).
| Produce the first input to the chain of functors to come |
Module User <: USE_TYPE_SYSTEM.
Module Sys := TypeSystem.
Definition minit : {init : list (list (stateDescription Sys.ty Sys.mastate)
* stateDescription Sys.ty Sys.mastate)
| (AllS (fun sd => match sdPc (snd sd) with
| ApcUnknown => False
| ApcConst pc => validPc pc
end) init)
/\ forall st, M.minitState st -> exists ctx, exists sd,
In (nil, sd) init
/\ ApcConst (SstPc st) = sdPc sd
/\ (forall r, Sys.hasTy ctx (get_reg st r) (SalRegMap.get r (sdRegs sd)))
/\ Sys.mconc ctx st (sdCust sd)}.
End User.
Module Abs1 := Abstraction(User).
Module Abs2 := Fix(Abs1).
Module Ch := MySal.Checker(Abs2).
Module Mac := MC.
Definition verify := Ch.verify.
End Make.
Definition fold_right := fold_right.
End Verifier.