source: src/Clight/abstract.ma @ 2326

include "Clight/Csem.ma".

(* Definitions about Clight syntax and semantics for use in overall results. *)

let rec any_expr (P:expr → bool) (e:expr) on e : bool ≝
P e ∨
match e with [ Expr e _ ⇒ 
match e with
[ Ederef e' ⇒ any_expr P e'
| Eunop _ e' ⇒ any_expr P e'
| Ebinop _ e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
| Ecast _ e' ⇒ any_expr P e'
| Econdition e1 e2 e3 ⇒ any_expr P e1 ∨ any_expr P e2 ∨ any_expr P e3
| Eandbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
| Eorbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
| Efield e' _ ⇒ any_expr P e'
| Ecost _ e' ⇒ any_expr P e'
| _ ⇒ false
] ].

definition any_expr_statement : (expr → bool) → statement → bool ≝
λP,s.
match s with
[ Sassign e1 e2 ⇒ P e1 ∨ P e2
| Scall oe e es ⇒ (option_map_def … P false oe) ∨ P e ∨ all ? P es
| Sifthenelse e _ _ ⇒ P e
| Swhile e _ ⇒ P e
| Sdowhile e _ ⇒ P e
| Sfor _ e _ _ ⇒ P e
| Sreturn oe ⇒ option_map_def … P false oe
| _ ⇒ false
].

let rec any_statement (P:statement → bool) (s:statement) on s : bool ≝
P s ∨
match s with
[ Ssequence s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2
| Sifthenelse _ s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2
| Swhile _ s1 ⇒ any_statement P s1
| Sdowhile _ s1 ⇒ any_statement P s1
| Sfor s1 _ s2 s3 ⇒ any_statement P s1 ∨ any_statement P s2 ∨ any_statement P s3
| Sswitch _ ls ⇒ any_labeled_statement P ls
| Slabel _ s1 ⇒ any_statement P s1
| Scost _ s1 ⇒ any_statement P s1
| _ ⇒ false
] and any_labeled_statement (P:statement → bool) (ls:labeled_statements) on ls : bool ≝
match ls with
[ LSdefault s ⇒ any_statement P s
| LScase _ _ s ls' ⇒ any_statement P s ∨ any_labeled_statement P ls'
].

(* Labelled states in Clight are a little tricky because there are cost labels
   in the expressions in addition to the cost statement.  Note that a labelled
   state may produce several cost labels due to expressions, and that we should
   only check the root of the statement because sub-statements will not be
   executed until later.
   
   Also, a labelled state will only be guaranteed to generate a cost label in
   the trace if the program is properly cost labelled - if it isn't then an
   Econd might be used to with a cost label in only one branch.
    *)

definition expr_labelled : expr → bool ≝
any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true | _ ⇒ false ] ]).

definition statement_cont_labelled : statement → cont → bool ≝
λs,k.
match s with
[ Sskip ⇒
  match k with
  [ Kdowhile e _ _ ⇒ expr_labelled e
  | _ ⇒ false
  ]
| Sassign e1 e2 ⇒ expr_labelled e1 ∨ expr_labelled e2
| Scall oe e es ⇒ (option_map_def … expr_labelled false oe) ∨ expr_labelled e ∨ all ? expr_labelled es
| Ssequence _ _ ⇒ false
| Sifthenelse e _ _ ⇒ expr_labelled e
| Swhile e _ ⇒ expr_labelled e
| Sdowhile e _ ⇒ false
| Sfor s e _ _ ⇒ match s with [ Sskip ⇒ expr_labelled e | _ ⇒ false ]
| Sbreak ⇒ false
| Scontinue ⇒
  match k with
  [ Kdowhile e _ _ ⇒ expr_labelled e
  | _ ⇒ false
  ]
| Sreturn oe ⇒ option_map_def … expr_labelled false oe
| Sswitch e _ ⇒ expr_labelled e (* should not occur due to early switch removal *)
| Slabel _ _ ⇒ false
| Sgoto _ ⇒ false
| Scost _ _ ⇒ true
].

definition Clight_labelled : state → bool ≝
λs. match s with
[ State f s k e m ⇒ statement_cont_labelled s k
| _ ⇒ false
].


(* At the moment this doesn't say anything about "jumps", just calls, returns
   and everything else. *)
include "common/StructuredTraces.ma".

definition Clight_classify : state → status_class ≝
λs. match s with
[ State _ _ _ _ _ ⇒ cl_other
| Callstate _ _ _ _ ⇒ cl_call
| Returnstate _ _ _ ⇒ cl_return
| Finalstate _ ⇒ cl_other
].

(* Help avoid ambiguous input fun *)
definition Clight_state ≝ state.