1 | |
---|

2 | include "Cexec.ma". |
---|

3 | |
---|

4 | (* Functions to allow programs to be executed up to some number of steps, given |
---|

5 | a predetermined set of input values. Note that we throw away the state if |
---|

6 | we stop at a continuation - it can be too large to work with. *) |
---|

7 | |
---|

8 | definition get_input : ∀o:io_out. eventval → res (io_in o) ≝ |
---|

9 | λo,ev. |
---|

10 | match io_in_typ o return λt. res (eventval_type t) with |
---|

11 | [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ] |
---|

12 | | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ] |
---|

13 | ]. |
---|

14 | |
---|

15 | let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝ |
---|

16 | match n with |
---|

17 | [ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉 |
---|

18 | | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉 |
---|

19 | | _ ⇒ Error ? ] |
---|

20 | | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m input e' (t⧺tr) |
---|

21 | | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉 |
---|

22 | | e_interact o k ⇒ |
---|

23 | match input with |
---|

24 | [ nil ⇒ Error ? |
---|

25 | | cons h tl ⇒ do i ← get_input o h; |
---|

26 | up_to_nth_step m tl (k i) t |
---|

27 | ] |
---|

28 | | e_wrong ⇒ Error ? |
---|

29 | ] |
---|

30 | ]. |
---|

31 | |
---|

32 | definition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝ |
---|

33 | λp,n,i. up_to_nth_step n i (exec_inf p) E0. |
---|

34 | |
---|

35 | (* Provide an easy way to get a term in proof mode for reduction. |
---|

36 | For example, |
---|

37 | |
---|

38 | example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]). |
---|

39 | normalize (* you can examine the result here *) |
---|

40 | % qed. |
---|

41 | |
---|

42 | *) |
---|

43 | |
---|

44 | inductive result (A:Type[0]) : A → Type[0] ≝ |
---|

45 | | witness : ∀a:A. result A a. |
---|

46 | |
---|

47 | (* Hide the representation of memory to make displaying the results easier. *) |
---|

48 | |
---|

49 | notation < "'MEM'" with precedence 1 for @{ 'mem }. |
---|

50 | interpretation "hide memory" 'mem = (mk_mem ???). |
---|