@ -152,10 +152,12 @@ Datatype `
(* T h e s e t o f a l l o c a t e d r a n g e s . T h e b o o l i n d i c a t e s w h e t h e r t h e r a n g e i s
* free - able or not * )
allocations : ( bool # num # num ) set ;
(* A b y t e a d d r e s s e d h e a p , w i t h a p o i s o n t a g *)
heap : addr |-> bool # word8 |>` ;
(* - - - - - T h i n g s a b o u t t y p e s - - - - - *)
(* H o w m a n y b y t e s a v a l u e o f t h e g i v e n t y p e o c c u p i e s *)
Definition sizeof_def :
( sizeof ( IntT W1 ) = 1 ) ∧
( sizeof ( IntT W8 ) = 1 ) ∧
@ -232,6 +234,7 @@ Definition bool_to_v_def:
bool_to_v b = if b then W1V 1 w else W1V 0 w
End
(* C a l c u l a t e t h e o f f s e t g i v e n b y a l i s t o f i n d i c e s *)
Definition get_offset_def :
( get_offset _ [ ] = Some 0 ) ∧
( get_offset ( ArrT _ t ) ( i :: is ) =
@ -294,14 +297,6 @@ Definition v2n_def:
( v2n _ = None )
End
Definition update_result_def :
update_result x v s = s with locals := s. locals |+ ( x , v )
End
Definition inc_pc_def :
inc_pc s = s with ip := ( s. ip with i := s. ip. i + 1 )
End
Definition interval_to_set_def :
interval_to_set ( _ , start , stop ) =
{ n | start ≤ n ∧ n < stop }
@ -324,6 +319,16 @@ Definition is_free_def:
∀b2. b2 ∈ allocs ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
End
Definition get_bytes_def :
get_bytes h ( _ , start , stop ) =
map
( λoff.
case flookup h ( A ( start + off ) ) of
| None => ( F , 0 w )
| Some w => w )
( count_list ( stop - start ) )
End
Definition set_bytes_def :
( set_bytes p [ ] n h = h ) ∧
( set_bytes p ( b :: bs ) n h =
@ -349,16 +354,8 @@ Definition deallocate_def:
( allocs DIFF to_remove , fdiff h ( image A ( bigunion ( image interval_to_set to_remove ) ) ) )
End
Definition get_bytes_def :
get_bytes h ( _ , start , stop ) =
map
( λoff.
case flookup h ( A ( start + off ) ) of
| None => ( F , 0 w )
| Some w => w )
( count_list ( stop - start ) )
End
(* R e a d l e n b y t e s f r o m t h e l i s t o f b y t e s , a n d c o n v e r t i t i n t o a w o r d v a l u e ,
* little - endian encoding * )
Definition le_read_w_def :
le_read_w len ( bs : word8 list ) =
if length bs < len then
@ -367,6 +364,7 @@ Definition le_read_w_def:
( l2w 256 ( map w2n ( take len bs ) ) , drop len bs )
End
(* R e t u r n l e n b y t e s t h a t a r e t h e l i t t l e - e n d i a n e n c o d i n g o f t h e a r g u m e n t w o r d *)
Definition le_write_w_def :
le_write_w len w =
let ( l : word8 list ) = map n2w ( w2l 256 w ) in
@ -470,6 +468,14 @@ Definition insert_value_def:
( insert_value _ _ _ = None )
End
Definition update_result_def :
update_result x v s = s with locals := s. locals |+ ( x , v )
End
Definition inc_pc_def :
inc_pc s = s with ip := ( s. ip with i := s. ip. i + 1 )
End
(* N B , t h e s e m a n t i c s t r a c k s t h e p o i s o n v a l u e s , b u t n o t m u c h t h o u g h t h a s b e e n p u t
* into getting it exactly right , so we don't have much confidence that it is
* exactly right. We also are currently ignoring the undefined value. * )
@ -601,12 +607,14 @@ Inductive step_instr:
( Call r t fname targs )
<| ip := <| f := fname ; b := None ; i := 0 |> ;
locals := alist_to_fmap ( zip ( d. params , map ( eval s o snd ) targs ) ) ;
globals := s. globals ;
allocations := s. allocations ;
stack :=
<| ret := s. ip with i := s. ip. i + 1 ;
saved_locals := s. locals ;
result_var := r ;
stack_allocs := [ ] |> :: s. stack ;
heap := heap |> ) ∧
heap := s. heap |> ) ∧
(* T O D O *)
( step_instr prog s ( Cxa_allocate_exn r a ) s ) ∧
@ -635,8 +643,9 @@ Inductive step:
step p s s'
End
(* - - - - - I n it i a l s t a t e - - - - - *)
(* - - - - - I n va r i a n t s o n s t a t e - - - - - *)
(* T h e a l l o c a t i o n s a r e o f i n t e r v a l s t h a t d o n ' t o v e r l a p *)
Definition allocations_ok_def :
allocations_ok s ⇔
∀i1 i2.
@ -646,11 +655,13 @@ Definition allocations_ok_def:
( interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2 )
End
(* T h e h e a p m a p s e x a c t l y t h e a d d r e s s i n t h e a l l o c a t i o n s *)
Definition heap_ok_def :
heap_ok s ⇔
∀n. flookup s. heap ( A n ) ≠ None ⇔ ∃i. i ∈ s. allocations ∧ n ∈ interval_to_set i
End
(* A l l g l o b a l v a r i a b l e s a r e a l l o c a t e d i n n o n - f r e e a b l e m e m o r y *)
Definition globals_ok_def :
globals_ok s ⇔
∀g n w.
@ -659,47 +670,36 @@ Definition globals_ok_def:
is_allocated ( F , w2n w , w2n w + n ) s. allocations
End
(* T h e i n i t i a l s t a t e c o n t a i n s a l l o c a t i o n s f o r t h e i n i t i a l i s e d g l o b a l v a r i a b l e s *)
Definition is_init_state_def :
is_init_state s ( global_init : glob_var |-> ty # v ) ⇔
s. ip. f = Fn " m a i n " ∧
s. ip. b = None ∧
s. ip. i = 0 ∧
s. locals = fempty ∧
s. stack = [ ] ∧
allocations_ok s ∧
globals_ok s ∧
fdom s. globals = fdom global_init ∧
s. allocations ⊆ { F , start , stop | T } ∧
∀g w t v n.
flookup s. globals g = Some ( n , w ) ∧ flookup global_init g = Some ( t , v ) ⇒
∃bytes.
get_bytes s. heap ( F , w2n w , w2n w + sizeof t ) = map ( λb. ( F , b ) ) bytes ∧
bytes_to_value t bytes = ( v , [ ] )
End
(* - - - - - I n v a r i a n t s o n s t a t e - - - - - *)
Definition prog_ok_def :
prog_ok p ⇔
∀fname dec bname block.
flookup p fname = Some dec ∧
flookup dec. blocks bname = Some block
⇒
block. body ≠ [ ] ∧ terminator ( last block. body )
End
(* I n s t r u c t i o n p o i n t e r p o i n t s t o a n i n s t r u c t i o n *)
Definition ip_ok_def :
ip_ok p ip ⇔
∃dec block. flookup p ip. f = Some dec ∧ flookup dec. blocks ip. b = Some block ∧ ip. i < length block. body
End
Definition prog_ok_def :
prog_ok p ⇔
( (* A l l b l o c k s e n d w i t h t e r m i n a t o r s *)
∀fname dec bname block.
flookup p fname = Some dec ∧
flookup dec. blocks bname = Some block
⇒
block. body ≠ [ ] ∧ terminator ( last block. body ) ) ∧
( (* A l l f u n c t i o n s h a v e a n e n t r y b l o c k *)
∀fname dec.
flookup p fname = Some dec ⇒ ∃block. flookup dec. blocks None = Some block ) ∧
(* T h e r e i s a m a i n f u n c t i o n *)
∃dec. flookup p ( Fn " m a i n " ) = Some dec
End
(* A l l c a l l f r a m e s h a v e a g o o d r e t u r n a d d r e s s , a n d t h e s t a c k a l l o c a t i o n s o f t h e
* frame are all in freeable memory * )
Definition frame_ok_def :
frame_ok p s f ⇔
ip_ok p f. ret ∧
every ( λn. ∃start stop. n = A start ∧ ( T , start , stop ) ∈ s. allocations ) f. stack_allocs
End
(* T h e f r a m e s a r e a l l o f , a n d n o t w o s t a c k a l l o c a t i o n s h a v e t h e s a m e a d d r e s s *)
Definition stack_ok_def :
stack_ok p s ⇔
every ( frame_ok p s ) s. stack ∧
@ -711,4 +711,29 @@ Definition state_invariant_def:
ip_ok p s. ip ∧ allocations_ok s ∧ heap_ok s ∧ globals_ok s ∧ stack_ok p s
End
(* - - - - - I n i t i a l s t a t e - - - - - *)
(* T h e i n i t i a l s t a t e c o n t a i n s a l l o c a t i o n s f o r t h e i n i t i a l i s e d g l o b a l v a r i a b l e s *)
Definition is_init_state_def :
is_init_state s ( global_init : glob_var |-> ty # v ) ⇔
s. ip. f = Fn " m a i n " ∧
s. ip. b = None ∧
s. ip. i = 0 ∧
s. locals = fempty ∧
s. stack = [ ] ∧
allocations_ok s ∧
globals_ok s ∧
heap_ok s ∧
fdom s. globals = fdom global_init ∧
(* T h e i n i t i a l a l l o c a t i o n s f o r g l o b a l s a r e n o t f r e e a b l e *)
s. allocations ⊆ { ( F , start , stop ) | T } ∧
(* T h e h e a p s t a r t s w i t h t h e i n i t i a l v a l u e s o f t h e g l o b a l s w r i t t e n t o t h e i r
* addresses * )
∀g w t v n.
flookup s. globals g = Some ( n , w ) ∧ flookup global_init g = Some ( t , v ) ⇒
∃bytes.
get_bytes s. heap ( F , w2n w , w2n w + sizeof t ) = map ( λb. ( F , b ) ) bytes ∧
bytes_to_value t bytes = ( v , [ ] )
End
export_theory ( ) ;
Scott Owens
5 years ago
committed by
Facebook Github Bot