-
Notifications
You must be signed in to change notification settings - Fork 105
/
SimplExport.thy
1174 lines (1054 loc) · 53.8 KB
/
SimplExport.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*)
theory SimplExport
imports GraphLang CommonOpsLemmas GlobalsSwap ExtraSpecs
begin
lemma field_lvalue_offset_eq:
"field_lookup (typ_info_t TYPE('a :: c_type)) f 0 = Some v
\<Longrightarrow> field_lvalue (ptr :: 'a ptr) f = ptr_val ptr + of_nat (snd v)"
apply (cases v, simp, drule field_lookup_offset_eq)
apply (simp add: field_lvalue_def)
done
ML \<open>
fun dest_binT (Type (@{type_name signed}, [t])) = Word_Lib.dest_binT t
| dest_binT t = Word_Lib.dest_binT t
fun dest_array_type (Type (@{type_name array}, [T, n])) = let
val (s, _) = dest_Type n
val s = Long_Name.base_name s
in if String.isPrefix "tyCopy" s
then (T, fst (read_int (raw_explode (unprefix "tyCopy" s))))
else (T, dest_binT n)
end
| dest_array_type typ = raise TYPE ("dest_array_type", [typ], [])
fun dest_array_init (Const (@{const_name fupdate}, _) $ n $ f $ arr) = let
val xs = dest_array_init arr
val n = HOLogic.dest_number n |> snd
in nth_map n (curry betapply f) xs end
| dest_array_init (Const (@{const_name FCP}, T) $ f) = let
val (_, width) = dest_array_type (range_type T)
in map (curry betapply f) (map (HOLogic.mk_number @{typ nat})
(0 upto width - 1))
end
| dest_array_init t = raise TERM ("dest_array_init", [t])
val ops = Symtab.make [
(@{const_name "plus"}, ("Plus", true)),
(@{const_name "minus"}, ("Minus", true)),
(@{const_name "times"}, ("Times", true)),
(@{const_name "modulo_class.modulo"}, ("Modulus", true)),
(@{const_name "divide_class.divide"}, ("DividedBy", true)),
(@{const_name "and"}, ("BWAnd", true)),
(@{const_name "or"}, ("BWOr", true)),
(@{const_name "xor"}, ("BWXOR", true)),
(@{const_name "conj"}, ("And", true)),
(@{const_name "disj"}, ("Or", true)),
(@{const_name "implies"}, ("Implies", true)),
(@{const_name "HOL.eq"}, ("Equals", false)),
(@{const_name "less"}, ("Less", false)),
(@{const_name "less_eq"}, ("LessEquals", false)),
(@{const_name "ptr_less"}, ("Less", false)),
(@{const_name "ptr_le"}, ("LessEquals", false)),
(@{const_name "word_sless"}, ("SignedLess", false)),
(@{const_name "word_sle"}, ("SignedLessEquals", false)),
(@{const_name "Not"}, ("Not", true)),
(@{const_name "not"}, ("BWNot", true)),
(@{const_name "unsigned"}, ("WordCast", false)),
(@{const_name "signed"}, ("WordCastSigned", false)),
(@{const_name "True"}, ("True", true)),
(@{const_name "False"}, ("False", true)),
(@{const_name "If"}, ("IfThenElse", false)),
(@{const_name "Set.member"}, ("MemDom", false)),
(@{const_name "shiftl"}, ("ShiftLeft", false)),
(@{const_name "shiftr"}, ("ShiftRight", false)),
(@{const_name "sshiftr"}, ("SignedShiftRight", false)),
(@{const_name "bv_clz"}, ("CountLeadingZeroes", true)),
(@{const_name "bv_ctz"}, ("CountTrailingZeroes", true)),
(@{const_name "all_htd_updates"}, ("HTDUpdate", false))
] |> Symtab.lookup
fun locals ctxt = Syntax.read_typ ctxt "'a myvars"
|> Record.get_recT_fields (Proof_Context.theory_of ctxt)
|> fst
|> filter_out (fn (s, _) => s = @{const_name "globals"})
|> Symtab.make |> Symtab.defined
fun local_upds ctxt = Syntax.read_typ ctxt "'a myvars"
|> Record.get_recT_fields (Proof_Context.theory_of ctxt)
|> fst
|> filter_out (fn (s, _) => s = @{const_name "globals"})
|> map (apfst (suffix Record.updateN))
|> Symtab.make |> Symtab.defined
fun get_field ctxt s = let
val xs = space_explode "." s
val fld = List.last xs
val tp = rev xs |> tl |> rev |> space_implode "."
val is_upd = String.isSuffix "_update" fld
val fld = if is_upd then unsuffix "_update" fld else fld
val _ = Proof_Context.get_thm ctxt
(tp ^ "_" ^ fld ^ "_fl_Some")
in SOME (tp, fld, is_upd) end
handle ERROR _ => NONE
| Bind => NONE
fun read_const ctxt (pfx : string) (name : string) = let
val nm = if pfx = "" then name else (pfx ^ "." ^ name)
in Proof_Context.read_const {proper = true, strict = true} ctxt nm end
fun process_struct ctxt csenv pfx (nm, flds) = let
val offs = map (ProgramAnalysis.offset csenv (map snd flds))
(0 upto (length flds - 1))
val cons = read_const ctxt pfx (nm ^ "." ^ nm)
val typ = dest_Const cons |> snd |> strip_type |> snd
val sz = ProgramAnalysis.sizeof csenv (Absyn.StructTy nm)
val algn = ProgramAnalysis.alignof csenv (Absyn.StructTy nm)
val accs = map (fst #> prefix (nm ^ ".")
#> read_const ctxt pfx) flds
in (nm, (cons, typ, sz, algn, map fst flds ~~ (accs ~~ offs))) end
fun structs ctxt csenv pfx = ProgramAnalysis.get_senv csenv
|> map (process_struct ctxt csenv pfx)
|> Symtab.make
fun structs_by_typ ctxt csenv pfx = Symtab.dest (structs ctxt csenv pfx)
|> map (fn (nm, (cons, typ, sz, algn, flds)) => (fst (dest_Type typ), (nm, cons, sz, algn, flds)))
|> Symtab.make |> Symtab.lookup
fun cons_fields ctxt csenv pfx = structs ctxt csenv pfx |> Symtab.dest
|> map (fn (_, (cons, typ, _, _, flds))
=> (fst (dest_Const cons), (fst (dest_Type typ),
map (snd #> fst #> dest_Const #> fst) flds)))
|> Symtab.make |> Symtab.lookup
fun enums ctxt csenv pfx = let
val Absyn.CE ecenv = ProgramAnalysis.cse2ecenv csenv
in
#enumenv ecenv |> Symtab.dest
|> map (fn (s, (n, _)) =>
(read_const ctxt pfx s
|> dest_Const |> fst, n))
|> Symtab.make |> Symtab.lookup
end
fun thm_to_rew thm
= ((Thm.concl_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_eq)
handle TERM _ => (Thm.concl_of thm |> Logic.dest_equals))
handle TERM _ => (Thm.concl_of thm |> HOLogic.dest_Trueprop |> HOLogic.dest_imp)
fun cons_field_upds ctxt csenv = let
val simps = ProgramAnalysis.get_senv csenv
|> maps (fn (tp, vs) => map (pair tp o fst) vs)
|> maps (fn (tp, fld) => [Proof_Context.get_thm ctxt
(tp ^ "." ^ fld ^ ".simps"),
Proof_Context.get_thm ctxt
(tp ^ "." ^ fld ^ Record.updateN ^ ".simps")])
val accups = ProgramAnalysis.get_senv csenv
|> map (fn (tp, _) => (tp, Proof_Context.get_thms ctxt
(tp ^ "_accupd_same")))
|> maps (fn (_, [t]) => [t]
| (tp, ts) => ts @ Proof_Context.get_thms ctxt
(tp ^ "_accupd_diff"))
val rews = map thm_to_rew (simps @ accups)
in Pattern.rewrite_term (Proof_Context.theory_of ctxt) rews [] end
type export_params = {cons_field_upds: term -> term,
cons_fields: string -> (string * string list) option,
const_globals: Termtab.key -> string option,
enums: string -> int option,
local_upds: string -> bool,
locals: string -> bool,
rw_global_accs: string -> string option,
rw_global_upds: string -> string option,
rw_globals_tab: (term * term) Symtab.table,
structs_by_typ:
string -> (string * term * int * int * (string * (term * int)) list) option,
pfx: string (* prefix for looking up full names of constants *)}
fun get_all_export_params ctxt csenv pfx : export_params = let
(* assuming DefineGlobalsList has already run *)
val defs = if (can (Proof_Context.get_thms ctxt) "no_global_data_defs")
then [] else Proof_Context.get_thms ctxt "global_data_defs"
val rhss = map (Thm.concl_of #> Logic.dest_equals #> snd) defs
val const_globals = map_filter
(fn (Const (@{const_name const_global_data}, _) $ nm $ v)
=> SOME (HOLogic.dest_string nm, v)
| _ => NONE) rhss |> map swap |> Termtab.make |> Termtab.lookup
val rw_globals = map_filter (fn (Const (@{const_name global_data}, _) $ nm $ get $ set)
=> SOME (HOLogic.dest_string nm, get, set) | _ => NONE) rhss
val rw_globals_tab = Symtab.make (map (fn x => (#1 x, (#2 x, #3 x))) rw_globals)
val rw_global_accs = map (fn (nm, c, _) => (fst (dest_Const c), nm)) rw_globals
|> Symtab.make |> Symtab.lookup
val rw_global_upds = map (fn (nm, _, c) => (fst (dest_Const c), nm)) rw_globals
|> Symtab.make |> Symtab.lookup
in {const_globals = const_globals, rw_globals_tab = rw_globals_tab,
rw_global_accs = rw_global_accs,
rw_global_upds = rw_global_upds,
cons_field_upds = cons_field_upds ctxt csenv,
enums = enums ctxt csenv pfx,
cons_fields = cons_fields ctxt csenv pfx,
structs_by_typ = structs_by_typ ctxt csenv pfx,
locals = locals ctxt,
local_upds = local_upds ctxt,
pfx = pfx} end
\<close>
ML \<open>
val machine_word = case @{typ machine_word} of
@{typ word32} => "Word 32"
| @{typ word64} => "Word 64"
fun convert_type _ _ @{typ bool} = "Bool"
| convert_type _ _ (Type (@{type_name word}, [n]))
= "Word " ^ signed_string_of_int (dest_binT n)
| convert_type abs ctxt (Type (@{type_name array}, [t, n]))
= "Array " ^ convert_type abs ctxt t ^ " " ^ (string_of_int (dest_binT n)
handle TYPE _ => (case n of Type (s, []) => (unprefix "tyCopy" (Long_Name.base_name s)
handle Fail _ => raise TYPE ("convert_type", [t, n], []))
| _ => raise TYPE ("convert_type", [t, n], [])))
| convert_type true ctxt (Type (@{type_name ptr}, [T])) = "Ptr " ^ convert_type true ctxt T
| convert_type false _ (Type (@{type_name ptr}, _)) = machine_word
| convert_type _ _ @{typ "machine_word \<Rightarrow> word8"} = "Mem"
| convert_type _ _ @{typ "machine_word \<Rightarrow> bool"} = "Dom"
| convert_type _ _ @{typ "machine_word set"} = "Dom"
| convert_type _ _ @{typ heap_typ_desc} = "HTD"
| convert_type _ _ @{typ nat} = raise TYPE ("convert_type: nat", [], [])
| convert_type _ _ @{typ unit} = "UNIT"
| convert_type _ _ (Type ("fun", [Type (@{type_name word}, [i]), Type (@{type_name word}, [j])]))
= "WordArray " ^ signed_string_of_int (dest_binT i) ^ " " ^ signed_string_of_int (dest_binT j)
| convert_type _ _ (Type (@{type_name itself}, _)) = "Type"
| convert_type _ _ @{typ int} = raise TYPE ("convert_type: int", [], [])
| convert_type _ ctxt (Type (s, [])) = if Long_Name.base_name s = "machine_state" then "PMS"
else (Proof_Context.get_thm ctxt
(Long_Name.base_name s ^ "_td_names"); "Struct " ^ s)
| convert_type _ _ T = raise TYPE ("convert_type", [T], [])
\<close>
consts
pseudo_acc :: "'a \<Rightarrow> 'a"
text \<open>
Phase 1 of the conversion, converts accs and upds on SIMPL
state (a record) to accs of named vars, using the pseudo_acc
constant above to guard the accesses and lists of upds with strings.
\<close>
ML \<open>
fun naming localname = Long_Name.base_name localname
|> unsuffix "_'" |> suffix "#v"
fun mk_pseudo_acc s T = Const (@{const_name pseudo_acc}, T --> T)
$ Free (s, T)
fun dest_global_mem_acc_addr (params : export_params) t = let
val acc = case head_of t of Const (c, _) => #rw_global_accs params c
| _ => NONE
val const = #const_globals params t
val T = fastype_of t
in case (const, acc) of
(SOME _, _) => NONE
| (NONE, SOME nm) => SOME (TermsTypes.mk_global_addr_ptr (nm, T))
| (NONE, NONE) => NONE
end
fun dest_ptr_type (Type (@{type_name ptr}, [a])) = a
| dest_ptr_type T = raise TYPE ("dest_ptr_type", [T], [])
fun mk_memacc p = let
val T = fastype_of p
in Const (@{const_name h_val}, @{typ heap_mem} --> T --> dest_ptr_type T)
$ mk_pseudo_acc "Mem" @{typ heap_mem} $ p end
fun mk_fun_app f x = let
val fT = fastype_of f
in Const (@{const_name "fun_app"}, fT --> fastype_of x --> range_type fT) $ f $ x end
val ghost_assns = mk_pseudo_acc "GhostAssertions" @{typ "ghost_assertions"}
val int_to_ghost_key = @{term "word_of_int :: int \<Rightarrow> 50 word"}
fun convert_fetch_phase1 _ (@{term hrs_mem} $ _) = mk_pseudo_acc "Mem" @{typ heap_mem}
| convert_fetch_phase1 _ (@{term hrs_htd} $ _) = mk_pseudo_acc "HTD" @{typ heap_typ_desc}
| convert_fetch_phase1 _ (Const (@{const_name ghost_assertion_data_get}, _) $ k $ _ $ _)
= mk_fun_app ghost_assns (int_to_ghost_key $ k)
| convert_fetch_phase1 params (Abs (s, T, t))
= Abs (s, T, convert_fetch_phase1 params t)
| convert_fetch_phase1 params t = if not (is_Const (head_of t)) then t
else let
val (f, xs) = strip_comb t
val (c, _) = dest_Const f
val T = fastype_of t
in case (#locals params c, dest_global_mem_acc_addr params t, #enums params c) of
(true, _, _) => (case xs of [Free ("s", _)] => mk_pseudo_acc (naming c) T
| [Free ("rv", _)] => mk_pseudo_acc ("rv#space#" ^ naming c) T
| _ => raise TERM ("convert_fetch_phase1: acc?", [t])
)
| (_, SOME p, _) => mk_memacc p
| (_, _, SOME n) => HOLogic.mk_number T n
| _ => list_comb (f, map (convert_fetch_phase1 params) xs)
end
fun mk_memupd1 ptr v m = if dest_ptr_type (fastype_of ptr) = fastype_of v
then Const (@{const_name heap_update}, fastype_of ptr --> fastype_of v
--> @{typ "heap_mem \<Rightarrow> heap_mem"})
$ ptr $ v $ m
else raise TERM ("mk_memupd1: types disagree", [ptr, v])
fun mk_memupd2 ptr v = mk_memupd1 ptr v (mk_pseudo_acc "Mem" @{typ heap_mem})
fun mk_fun_upd f x v = Const (@{const_name fun_upd},
fastype_of f --> fastype_of x --> fastype_of v --> fastype_of f) $ f $ x $ v
fun convert_upd_phase1 ctxt params (t as (Const (@{const_name globals_update}, _)
$ (Const (c, _) $ f) $ s)) = (case (Envir.beta_eta_contract f,
String.isPrefix NameGeneration.ghost_state_name
(Long_Name.base_name c), #rw_global_upds params c) of
(Const (@{const_name hrs_mem_update}, _)
$ (Const (@{const_name heap_update}, _) $ p $ v), _, _)
=> [("Mem", convert_fetch_phase1 params (mk_memupd2 p v))]
| (Const (@{const_name hrs_htd_update}, _) $ g, _, _)
=> [("HTD", (convert_fetch_phase1 params
(betapply (g, mk_pseudo_acc "HTD" @{typ heap_typ_desc}))))]
| (Const (@{const_name ghost_assertion_data_set}, _) $ k $ v $ _, _, _)
=> [("GhostAssertions", mk_fun_upd ghost_assns (int_to_ghost_key $ k)
(convert_fetch_phase1 params v))]
| (_, true, _) => ((Syntax.pretty_term ctxt f |> Pretty.writeln); [])
| (_, _, SOME nm) => let
val acc = the (Symtab.lookup (#rw_globals_tab params) nm) |> fst
val v = convert_fetch_phase1 params (betapply (f, acc $ s))
val ptr = TermsTypes.mk_global_addr_ptr (nm, fastype_of v)
in [("Mem", mk_memupd2 ptr v)] end
| _ => raise TERM ("convert_upd", [t]))
| convert_upd_phase1 _ params (t as (Const (c, _) $ f $ s)) = let
val c' = unsuffix Record.updateN c
val cT' = fastype_of s --> fastype_of (f $ s)
val _ = (#local_upds params c) orelse raise TERM ("convert_upd_phase1: nonlocal", [t])
val v = betapply (f, Const (c', cT') $ s)
in [(naming c', convert_fetch_phase1 params v)] end
| convert_upd_phase1 _ _ t = raise TERM ("convert_upd_phase1", [t])
\<close>
text \<open>Phase 2 eliminates compound types, so we access and
update only words from memory and local values.\<close>
ML \<open>
fun ptr_simp ctxt = ctxt addsimps @{thms CTypesDefs.ptr_add_def size_of_def size_td_array
field_lvalue_offset_eq align_td_array' scast_def[symmetric]
ucast_def[symmetric]
sint_sbintrunc' word_smod_numerals word_sdiv_numerals sdiv_int_def smod_int_def}
|> Simplifier.rewrite
val trace_ptr_simp = false
fun ptr_simp_term ctxt s pat t = let
val rew_thm = pat |> Thm.cterm_of ctxt |> ptr_simp ctxt
val rew = rew_thm |> Thm.concl_of |> Logic.varify_global |> Logic.dest_equals
val _ = (not (fst rew aconv snd rew))
orelse raise TERM ("ptr_simp_term: " ^ s, [fst rew])
val _ = if not trace_ptr_simp then () else
(Thm.pretty_thm ctxt rew_thm |> Pretty.writeln;
Syntax.pretty_term ctxt t |> Pretty.writeln)
in Pattern.rewrite_term (Proof_Context.theory_of ctxt) [rew] [] t end
fun convert_ghost_key ctxt k = let
val procs = Term.add_const_names k []
|> filter (String.isSuffix HoarePackage.proc_deco)
val proc_defs = map (suffix "_def" #> Proof_Context.get_thm ctxt) procs
val conv = Simplifier.rewrite (ctxt addsimps proc_defs)
(Thm.cterm_of ctxt k)
val n = Thm.rhs_of conv |> Thm.term_of
val _ = HOLogic.dest_number n
in n end
fun dest_arrayT (Type (@{type_name array}, [elT, nT])) = let
in (elT, dest_binT nT) end
| dest_arrayT T = raise TYPE ("dest_arrayT", [T], [])
fun dest_nat (@{term Suc} $ n) = dest_nat n + 1
| dest_nat (@{term "0 :: nat"}) = 0
| dest_nat n = HOLogic.dest_number n |> snd
fun get_c_type_size ctxt T = let
val TT = Logic.mk_type T
val size_of = Const (@{const_name size_of}, type_of TT --> @{typ nat}) $ TT
in (ptr_simp_term ctxt "c_type_size" size_of size_of |> dest_nat) end
val ptr_to_typ = Logic.mk_type o dest_ptr_type o fastype_of
fun mk_arr_idx arr i = let
val arrT = fastype_of arr
val elT = case arrT of Type (@{type_name "array"}, [elT, _])
=> elT | _ => raise TYPE ("mk_arr_idx", [arrT], [arr])
in Const (@{const_name "Arrays.index"}, arrT --> @{typ nat} --> elT)
$ arr $ i
end
fun get_ptr_val (Const (@{const_name "Ptr"}, _) $ x) = x
| get_ptr_val p = Const (@{const_name ptr_val},
fastype_of p --> @{typ machine_word}) $ p
fun mk_ptr_offs opt_T p offs = let
val pT = fastype_of p
val T = case opt_T of NONE => pT
| SOME T => Type (@{type_name ptr}, [T])
in Const (@{const_name Ptr}, @{typ machine_word} --> T)
$ (@{term "(+) :: machine_word \<Rightarrow> _"}
$ get_ptr_val p $ offs)
end
fun get_acc_type [] T = T
| get_acc_type accs _ = (List.last accs $ @{term x})
|> fastype_of
val normalise_ring_ops = let
fun gather_plus (Const (@{const_name "plus"}, _) $ a $ b)
= gather_plus a @ gather_plus b
| gather_plus x = [x]
fun gather_times (Const (@{const_name "times"}, _) $ a $ b)
= gather_times a @ gather_times b
| gather_times x = [x]
fun fold_op _ [x] = x
| fold_op oper (x :: xs) = oper $ x $ (fold_op oper xs)
| fold_op _ [] = error "fold_op: shouldn't get empty list"
fun inner (x as (Const (@{const_name "plus"}, _) $ _ $ _))
= gather_plus x |> map inner
|> sort Term_Ord.fast_term_ord
|> fold_op (head_of x)
| inner (x as (Const (@{const_name "times"}, _) $ _ $ _))
= gather_times x |> map inner
|> sort Term_Ord.fast_term_ord
|> fold_op (head_of x)
| inner (f $ x) = inner f $ inner x
| inner x = x
in inner end
fun dest_mem_acc_addr (Const (@{const_name h_val}, _) $ _ $ p)
= SOME p
| dest_mem_acc_addr _ = NONE
fun narrow_mem_upd ctxt (params : export_params) p v = let
val T = fastype_of v
fun mk_offs T = mk_ptr_offs (SOME T) p
fun mk_offs2 T = mk_offs T o HOLogic.mk_number @{typ machine_word}
val sterm = Syntax.pretty_term ctxt #> Pretty.string_of
val styp = Syntax.pretty_typ ctxt #> Pretty.string_of
in if (dest_mem_acc_addr v = SOME p) then []
else if #structs_by_typ params (fst (dest_Type T)) <> NONE
then let
val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T)))
val fld_writes = map (fn (_, (acc, offs))
=> (mk_offs2 (fastype_of (acc $ v)) offs,
#cons_field_upds params (acc $ v))) flds
in maps (uncurry (narrow_mem_upd ctxt params)) fld_writes end
else if fst (dest_Type T) = @{type_name array}
then let
val (elT, n) = dest_arrayT T
val elT_size = get_c_type_size ctxt elT
in case v of (Const (@{const_name Arrays.update}, _) $ arr $ i $ x)
=> narrow_mem_upd ctxt params (mk_offs elT (@{term "(*) :: machine_word => _"}
$ HOLogic.mk_number @{typ machine_word} elT_size
$ (@{term "of_nat :: nat \<Rightarrow> machine_word"} $ i)))
x @ narrow_mem_upd ctxt params p arr
| _ => let
val addrs = map (fn i => (mk_offs2 elT (i * elT_size)))
(0 upto (n - 1))
val elems = dest_array_init v
handle TERM _ => map
(fn i => mk_arr_idx v (HOLogic.mk_number @{typ nat} i))
(0 upto (n - 1))
val _ = (if n < 16 then () else
warning ("expanding " ^ string_of_int n ^ ": "
^ sterm p ^ styp (fastype_of p) ^ ": " ^ sterm v))
in maps (uncurry (narrow_mem_upd ctxt params)) (addrs ~~ elems) end
end
else if fst (dest_Type T) <> @{type_name word}
andalso fst (dest_Type T) <> @{type_name ptr}
then raise TERM ("narrow_mem_upd failed to narrow:", [p, v])
else [(p, v)]
end
fun triv_mem_upd ctxt p v = case dest_mem_acc_addr v of
NONE => false
| SOME p' => p aconv p' orelse let
val t = @{term "(-) :: machine_word \<Rightarrow> _"} $ get_ptr_val p $ get_ptr_val p'
val thm = ptr_simp ctxt (Thm.cterm_of ctxt t)
val t' = Thm.rhs_of thm |> Thm.term_of
in t' = @{term "0 :: machine_word"}
orelse (Thm.pretty_thm ctxt thm |> Pretty.writeln; false)
end
fun narrow_mem_acc _ _ [] p = p
| narrow_mem_acc ctxt params accs p = let
fun get_offs (Const (@{const_name Arrays.index}, idxT) $ i) = let
val (elT, _) = dest_arrayT (domain_type idxT)
val elT_size = get_c_type_size ctxt elT
in @{term "(*) :: machine_word \<Rightarrow> _"} $ HOLogic.mk_number @{typ machine_word} elT_size
$ (@{term "of_nat :: nat \<Rightarrow> machine_word"} $ i) end
| get_offs (Const (s, T)) = let
val struct_typ = domain_type T |> dest_Type |> fst
val (_, _, _, _, flds) = the (#structs_by_typ params struct_typ)
val matches = filter (fn (_, (c, _)) => c = Const (s, T)) flds
val _ = (length matches = 1)
orelse raise TERM ("narrow_mem_acc: get_offs: ", [Const (s, T)])
val offs = snd (snd (hd matches))
in HOLogic.mk_number @{typ machine_word} offs end
| get_offs t = raise TERM ("narrow_mem_acc: get_offs: ", [t])
val T' = get_acc_type accs (@{typ nat} (* doesn't matter *))
val offs = foldr1 (fn (x, y) => @{term "(+) :: machine_word \<Rightarrow> _"} $ x $ y)
(map get_offs accs)
in mk_ptr_offs (SOME T') p offs end
fun try_norm_index ctxt i = let
val i' = ptr_simp_term ctxt "idx_simp" i i
in dest_nat i'; i' end handle TERM _ => i
fun mk_acc_array i xs = let
val n = length xs
val _ = warning ("expanding acc array, width " ^ string_of_int n)
val i = @{term "of_nat :: nat \<Rightarrow> machine_word"} $ i
fun inner [(x, _)] = x
| inner ((x, j) :: xs) = let
val y = inner xs
val T = fastype_of x
in Const (@{const_name "If"}, HOLogic.boolT --> T --> T --> T)
$ HOLogic.mk_eq (i, HOLogic.mk_number @{typ machine_word} j) $ x $ y end
| inner [] = error "mk_acc_array: empty"
in inner (xs ~~ (0 upto (n - 1))) end
fun phase2_convert_global ctxt params accs
((idx as Const (@{const_name Arrays.index}, _)) $ i $ t)
= phase2_convert_global ctxt params ((idx $ try_norm_index ctxt i) :: accs) t
| phase2_convert_global ctxt params accs (Const acc $ t)
= phase2_convert_global ctxt params (Const acc :: accs) t
| phase2_convert_global ctxt params accs t = case #const_globals params t
of SOME nm => let
val known_offs = forall (fn Const (@{const_name Arrays.index}, _) $ i
=> (try dest_nat i) <> NONE
| _ => true) accs
val (c, _) = dest_Const t
val c_def = Proof_Context.get_thm ctxt (c ^ "_def")
val def_body = safe_mk_meta_eq c_def |> Thm.rhs_of |> Thm.term_of
|> Envir.beta_eta_contract
val p = TermsTypes.mk_global_addr_ptr (nm, fastype_of t)
val t' = if known_offs then def_body else mk_memacc p
val t_thm = if known_offs then SOME c_def else NONE
in SOME (t', t_thm) end
| _ => NONE
fun convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs)
(t as (Const (@{const_name fupdate}, _) $ _ $ _ $ _)) = let
val xs = dest_array_init (#cons_field_upds (params : export_params) t)
in case (try dest_nat i) of
SOME i => convert_fetch_ph2 ctxt params accs (nth xs i)
| NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i)
(map (convert_fetch_ph2 ctxt params accs) xs)
end
| convert_fetch_ph2 ctxt params ((Const (@{const_name Arrays.index}, _) $ i) :: accs)
(t as (Const (@{const_name FCP}, _) $ _)) = let
val xs = dest_array_init (#cons_field_upds params t)
in case (try dest_nat i) of
SOME i => convert_fetch_ph2 ctxt params accs (nth xs i)
| NONE => mk_acc_array (convert_fetch_ph2 ctxt params [] i)
(map (convert_fetch_ph2 ctxt params accs) xs)
end
| convert_fetch_ph2 ctxt params accs ((idx as Const (@{const_name Arrays.index}, _)) $ arr $ i) = let
val i' = convert_fetch_ph2 ctxt params accs i
val i'' = try_norm_index ctxt i'
in convert_fetch_ph2 ctxt params (idx $ i'' :: accs) arr end
| convert_fetch_ph2 ctxt params ((idx as Const (@{const_name Arrays.index}, _)) $ i :: accs)
(Const (@{const_name Arrays.update}, _) $ arr' $ i' $ v)
= let
val eq = HOLogic.mk_eq (i, i')
val eq = ptr_simp_term ctxt "idx_eq_simp" eq eq handle TERM _ => eq
val x = convert_fetch_ph2 ctxt params accs v
val y = convert_fetch_ph2 ctxt params (idx $ i :: accs) arr'
val T = fastype_of x
in case eq of @{term True} => x | @{term False} => y
| _ => Const (@{const_name If}, HOLogic.boolT --> T --> T --> T)
$ convert_fetch_ph2 ctxt params [] eq $ x $ y end
| convert_fetch_ph2 ctxt params accs (Const (@{const_name h_val}, _) $ _ $ p)
= let
val p = convert_fetch_ph2 ctxt params [] p
val p = narrow_mem_acc ctxt params accs p
in mk_memacc p end
| convert_fetch_ph2 ctxt params [] (Const (@{const_name heap_update}, _) $ p $ v $ m)
= let
val xs = narrow_mem_upd ctxt params p v
|> map (apply2 (convert_fetch_ph2 ctxt params []))
|> filter_out (uncurry (triv_mem_upd ctxt))
val m = convert_fetch_ph2 ctxt params [] m
in fold (uncurry mk_memupd1) xs m end
| convert_fetch_ph2 _ _ [] (t as (Const (@{const_name pseudo_acc}, _) $ _)) = t
| convert_fetch_ph2 ctxt params accs (Const (@{const_name pseudo_acc}, _) $ Free (s, T)) = let
val T = get_acc_type accs T
fun canon s [] = mk_pseudo_acc s T
| canon s (Const (@{const_name Arrays.index}, idxT) $ i :: accs) = (case
(try dest_nat i)
of SOME i => canon (s ^ "." ^ string_of_int i) accs
| NONE => let val (_, n) = dest_arrayT (domain_type idxT)
in mk_acc_array (convert_fetch_ph2 ctxt params [] i)
(map (fn j => canon (s ^ "." ^ string_of_int j) accs)
(0 upto (n - 1))) end)
| canon s (Const (acc_nm, _) :: accs)
= canon (s ^ "." ^ Long_Name.base_name acc_nm) accs
| canon _ (t :: _) = raise TERM ("convert_fetch_ph2: canon: ", [t])
in canon s accs end
| convert_fetch_ph2 _ _ [] (t as (Free ("symbol_table", _) $ _))
= t
| convert_fetch_ph2 _ _ [] (t as Free ("domain", _))
= t
| convert_fetch_ph2 ctxt params accs t = let
val (f, xs) = strip_comb t
val (c, _) = dest_Const f
val cnv = phase2_convert_global ctxt params accs f
|> Option.map (fst #> convert_fetch_phase1 params)
in if (get_field ctxt c |> Option.map #3) = SOME false
then case xs of [x] => convert_fetch_ph2 ctxt params (f :: accs) x
| _ => raise TERM ("convert_fetch_ph2: expected single", f :: xs)
else if cnv <> NONE then convert_fetch_ph2 ctxt params accs (the cnv)
else if (get_field ctxt c <> NONE orelse #cons_fields params c <> NONE)
then let
val _ = (accs <> []) orelse raise TERM ("convert_fetch_ph2: no accs", [t])
val t' = hd accs $ t
val t'' = #cons_field_upds params t'
in if t'' aconv t' then raise TERM ("convert_fetch_ph2: irreducible upd:", [t'])
else convert_fetch_ph2 ctxt params (tl accs) t'' end
else list_comb (f, map (convert_fetch_ph2 ctxt params []) xs) end
fun convert_upd_ph2_worker ctxt params s v T accs =
if #structs_by_typ params (fst (dest_Type T)) <> NONE
then let
val (_, _, _, _, flds) = the (#structs_by_typ params (fst (dest_Type T)))
in maps (fn (fld_nm, (acc, _)) => convert_upd_ph2_worker ctxt params (s ^ "." ^ fld_nm)
v (range_type (fastype_of acc)) (accs @ [acc])) flds end
else if fst (dest_Type T) = @{type_name array}
then let
val (elT, n) = dest_arrayT T
in maps (fn i => convert_upd_ph2_worker ctxt params (s ^ "." ^ string_of_int i)
v elT (accs @ [Const (@{const_name Arrays.index}, T --> @{typ nat} --> elT)
$ HOLogic.mk_number @{typ nat} i])) (0 upto (n - 1))
end
else [(s, convert_fetch_ph2 ctxt params accs v)]
fun convert_upd_ph2 ctxt params (s, v)
= convert_upd_ph2_worker ctxt params s v (fastype_of v) []
(* |> tap (map (snd #> Syntax.pretty_term ctxt #> Pretty.writeln)) *)
\<close>
text \<open>The final conversion reduces Isabelle terms to strings\<close>
ML \<open>
val space_pad = space_implode " "
fun space_pad_list xs = space_pad (string_of_int (length xs) :: xs)
fun s_st ctxt = Syntax.read_term ctxt "s :: globals myvars"
fun rv_st ctxt = Syntax.read_term ctxt "rv :: globals myvars"
fun convert_op ctxt params nm tp xs = "Op " ^ nm ^ " " ^ tp
^ " " ^ space_pad_list (map (convert_ph3 ctxt params) xs)
and convert_ph3 ctxt params (Const (@{const_name Collect}, _) $ S $ x)
= convert_ph3 ctxt params (betapply (S, x))
| convert_ph3 ctxt params (Const (@{const_name Lattices.inf}, _) $ S $ T $ x)
= convert_op ctxt params "And" "Bool" [betapply (S, x), betapply (T, x)]
| convert_ph3 ctxt params (Const (@{const_name Ptr}, _) $ p) = convert_ph3 ctxt params p
| convert_ph3 ctxt params (Const (@{const_name ptr_val}, _) $ p) = convert_ph3 ctxt params p
| convert_ph3 ctxt params (t as (Const (@{const_name CTypesDefs.ptr_add}, T) $ _ $ _))
= convert_ph3 ctxt params (ptr_simp_term ctxt "ptr_add"
(head_of t $ Free ("p", domain_type T) $ Free ("n", @{typ int})) t)
| convert_ph3 ctxt params (t as (Const (@{const_name field_lvalue}, T) $ _ $ s))
= convert_ph3 ctxt params (ptr_simp_term ctxt "field_lvalue"
(head_of t $ Free ("p", domain_type T) $ s) t)
| convert_ph3 ctxt params (Const (@{const_name store_word64}, _) $ p $ w $ m)
= convert_op ctxt params "MemUpdate" "Mem" [m, p, w]
| convert_ph3 ctxt params (Const (@{const_name store_word32}, _) $ p $ w $ m)
= convert_op ctxt params "MemUpdate" "Mem" [m, p, w]
| convert_ph3 ctxt params (Const (@{const_name store_word8}, _) $ p $ w $ m)
= convert_op ctxt params "MemUpdate" "Mem" [m, p, w]
| convert_ph3 ctxt params (Const (@{const_name heap_update}, _) $ p $ v $ m)
= convert_op ctxt params "MemUpdate" "Mem" [m, p, v]
| convert_ph3 ctxt params (t as (Const (@{const_name h_val}, _) $ m $ p))
= convert_op ctxt params "MemAcc" (convert_type false ctxt (fastype_of t)) [m, p]
| convert_ph3 ctxt params (Const (@{const_name load_word64}, _) $ p $ m)
= convert_op ctxt params "MemAcc" "Word 64" [m, p]
| convert_ph3 ctxt params (Const (@{const_name load_word32}, _) $ p $ m)
= convert_op ctxt params "MemAcc" "Word 32" [m, p]
| convert_ph3 ctxt params (Const (@{const_name load_word8}, _) $ p $ m)
= convert_op ctxt params "MemAcc" "Word 8" [m, p]
| convert_ph3 ctxt params (Const (@{const_name fun_upd}, _) $ f $ x $ v)
= convert_op ctxt params "WordArrayUpdate"
(convert_type false ctxt (fastype_of f)) [f, x, v]
| convert_ph3 ctxt params (Const (@{const_name fun_app}, _) $ f $ x)
= convert_op ctxt params "WordArrayAccess"
(convert_type false ctxt (fastype_of (f $ x))) [f, x]
| convert_ph3 ctxt params ((le as Const (@{const_name less_eq}, _))
$ (Const (@{const_name insert}, _) $ p $ S) $ D)
= convert_op ctxt params "And" "Bool" [HOLogic.mk_mem (p, D), le $ S $ D]
| convert_ph3 ctxt params (Const (@{const_name less_eq}, _)
$ Const (@{const_name bot_class.bot}, _) $ _) = convert_ph3 ctxt params @{term True}
| convert_ph3 ctxt params (Const (@{const_name htd_safe}, _) $ _ $ _)
= convert_ph3 ctxt params @{term True}
| convert_ph3 ctxt params (Const (@{const_name uminus}, T) $ v)
= let val T = domain_type T
in convert_ph3 ctxt params (Const (@{const_name minus}, T --> T --> T)
$ Const (@{const_name zero_class.zero}, T) $ v) end
| convert_ph3 ctxt params (Const (@{const_name h_t_valid}, _) $ htd
$ Const (@{const_name c_guard}, _) $ p)
= convert_op ctxt params "PValid" "Bool" [htd, ptr_to_typ p, p]
| convert_ph3 ctxt params (Const (@{const_name array_assertion}, _) $ p $ n $ htd)
= convert_op ctxt params "PArrayValid" "Bool"
[htd, ptr_to_typ p, p, @{term "of_nat :: nat => machine_word"} $ n]
| convert_ph3 ctxt params (Const (@{const_name ptr_add_assertion'}, assT)
$ p $ n $ str $ htd)
= convert_ph3 ctxt params let val T = dest_ptr_type (fastype_of p)
val ass' = (Const (@{const_name ptr_add_assertion}, assT)) $ p $ n $ str $ htd
val ass'' = Pattern.rewrite_term (Proof_Context.theory_of ctxt)
(map thm_to_rew @{thms ptr_add_assertion_uintD ptr_add_assertion_sintD
if_True if_False}) [] ass'
in if T = @{typ unit} orelse T = @{typ word8}
then @{term True} else ass'' end
| convert_ph3 ctxt params (Const (@{const_name ptr_inverse_safe}, _) $ p $ htd)
= convert_op ctxt params "PGlobalValid" "Bool" [htd, ptr_to_typ p, p]
| convert_ph3 ctxt params (Const (@{const_name ptr_safe}, _) $ p $ htd)
= convert_op ctxt params "PWeakValid" "Bool" [htd, ptr_to_typ p, p]
| convert_ph3 ctxt params (Const (@{const_name globals_list_distinct}, _) $
(Const (@{const_name image}, _) $ Const (@{const_name fst}, _)
$ (Const (@{const_name s_footprint}, _) $ _)) $ _ $ _)
= convert_ph3 ctxt params @{term True}
| convert_ph3 ctxt params (Const (@{const_name c_guard}, _) $ p)
= convert_op ctxt params "PAlignValid" "Bool" [ptr_to_typ p, p]
| convert_ph3 ctxt params (Const (@{const_name bot}, _) $ _)
= convert_ph3 ctxt params @{term False}
| convert_ph3 ctxt params (Const (@{const_name top_class.top}, _) $ _)
= convert_ph3 ctxt params @{term True}
| convert_ph3 ctxt params (Const (@{const_name insert}, _) $ v $ S $ x)
= convert_op ctxt params "Or" "Bool" [HOLogic.mk_eq (v, x), betapply (S, x)]
| convert_ph3 _ _ (Free ("symbol_table", _) $ s)
= "Symbol " ^ HOLogic.dest_string s ^ " " ^ machine_word
| convert_ph3 ctxt params (Const (@{const_name of_nat}, T) $ (Const (@{const_name unsigned}, _) $ x))
= let
val t1 = fastype_of x
val t2 = range_type T
in if t1 = t2 then convert_ph3 ctxt params x
else convert_ph3 ctxt params (Const (@{const_name unsigned}, t1 --> t2) $ x)
end
| convert_ph3 ctxt params (t as (Const (@{const_name of_nat}, _) $ _))
= convert_ph3 ctxt params (ptr_simp_term ctxt "of_nat" t t)
| convert_ph3 ctxt params (t as (Const (@{const_name power}, _) $ x $ y))
= (case try HOLogic.dest_number x of
SOME ((typ as Type (@{type_name word}, _)), 2) => convert_ph3 ctxt params
(Const (@{const_name shiftl}, typ --> @{typ nat} --> typ)
$ HOLogic.mk_number typ 1 $ y)
| _ => convert_ph3 ctxt params (ptr_simp_term ctxt "power" t t))
| convert_ph3 ctxt params (Const (@{const_name ptr_coerce}, _) $ p)
= convert_ph3 ctxt params p
| convert_ph3 ctxt params (t as (Const (@{const_name of_int}, _) $ _))
= if head_of t = int_to_ghost_key then convert_ph3 ctxt params (convert_ghost_key ctxt t)
else let
val thy = Proof_Context.theory_of ctxt
val t' = Pattern.rewrite_term thy (map (Thm.concl_of #> HOLogic.dest_Trueprop
#> HOLogic.dest_eq) @{thms word_uint.Rep_inverse word_sint.Rep_inverse}) [] t
in if t' aconv t then convert_ph3 ctxt params (ptr_simp_term ctxt "word_of_int" t t)
else convert_ph3 ctxt params t' end
| convert_ph3 ctxt params (t as (Const (@{const_name signed_divide}, _) $ _ $ _))
= convert_ph3 ctxt params (ptr_simp_term ctxt "sdiv" t t)
| convert_ph3 ctxt _ (t as (Const (@{const_name numeral}, _) $ _))
= let
val n = HOLogic.dest_number t |> snd
handle TERM _ => raise TERM ("convert_ph3", [t])
val _ = (fastype_of t <> @{typ int}) orelse raise TERM ("convert_ph3: int", [t])
in "Num " ^ signed_string_of_int n ^ " " ^ convert_type false ctxt (fastype_of t) end
| convert_ph3 ctxt _ (Const (@{const_name Pure.type}, Type (_, [T])))
= "Type " ^ convert_type true ctxt T
| convert_ph3 ctxt _ (Const (@{const_name pseudo_acc}, _) $ Free (s, T))
= "Var " ^ s ^ " " ^ convert_type false ctxt T
| convert_ph3 ctxt params t = let
val (f, xs) = strip_comb t
val (c, _) = dest_Const f
val xs = if member (op =) [@{const_name shiftl},
@{const_name shiftr}, @{const_name sshiftr}] c
then case xs of
[x, y] => [x, Const (@{const_name of_nat}, @{typ nat} --> fastype_of x) $ y]
| _ => raise TERM ("convert_ph3: shift", [t])
else xs
in case ops c of
(SOME (nm, _)) => convert_op ctxt params nm (convert_type false ctxt (fastype_of t)) xs
| NONE => ("Num " ^ signed_string_of_int (snd (HOLogic.dest_number t))
^ " " ^ convert_type false ctxt (fastype_of t)
handle TERM _ => raise TERM ("convert_ph3", [t]))
end
fun htd_simp ctxt = ctxt addsimps @{thms fold_all_htd_updates
unat_less_2p_word_bits[simplified word_bits_conv]}
|> Simplifier.add_cong @{thm if_cong} |> Simplifier.rewrite
fun simp_htd ctxt t = let
val rew_thm = Thm.cterm_of ctxt t |> htd_simp ctxt
in Thm.term_of (Thm.rhs_of rew_thm) end
fun convert_upd_ph3 ctxt params (s, v) =
let
val nm = if s = "HTD" then "HTD HTD"
else s ^ " " ^ convert_type false ctxt (fastype_of v)
val v = if s = "HTD" then simp_htd ctxt v else v
val v = convert_ph3 ctxt params v
in (nm, v) end
handle TERM (s, ts) => raise TERM ("convert_upd_ph3: " ^ s, v :: ts)
\<close>
ML \<open>
fun convert_fetch ctxt params t =
Envir.beta_eta_contract t
|> convert_fetch_phase1 params
|> convert_fetch_ph2 ctxt params []
|> convert_ph3 ctxt params
fun tracet (s, t) = ((Syntax.pretty_term @{context} t |> Pretty.writeln); (s, t))
fun convert_param_upds ctxt params (t as (Const (c, _) $ _ $ s))
= if #local_upds params c orelse c = @{const_name globals_update}
then convert_param_upds ctxt params s
@ (Envir.beta_eta_contract t
(* |> tap (Syntax.pretty_term ctxt #> Pretty.writeln) *)
|> convert_upd_phase1 ctxt params
(* |> map tracet *)
(* |> map (apsnd (Syntax.check_term ctxt)) *)
|> maps (convert_upd_ph2 ctxt params)
(* |> map (apsnd (Syntax.check_term ctxt)) *)
|> map (convert_upd_ph3 ctxt params)
)
else raise TERM ("convert_param_upds", [t])
| convert_param_upds ctxt _ t = (if t = s_st ctxt then []
else raise TERM ("convert_param_upds", [t]))
\<close>
ML \<open>
val all_c_params = ["Mem Mem", "HTD HTD", "PMS PMS",
"GhostAssertions WordArray 50 " ^ ParseGraph.ptr_size_str]
val all_c_in_params = map (prefix "Var ") all_c_params
val all_asm_params = ["Mem Mem", "PMS PMS"]
val all_asm_in_params = map (prefix "Var ") all_asm_params
fun asm_spec_name_to_fn_name _ specname = let
val name = space_implode "_" (space_explode " " specname)
in "asm_instruction'" ^ name end
fun mk_safe f ctxt params s = (
Proof_Context.get_thm ctxt (s ^ "_body_def");
Proof_Context.get_thm ctxt (s ^ "_impl");
f ctxt params s) handle ERROR _ => false
fun mk_set_int s t = let
val T = fastype_of s
in Const (@{const_name Lattices.inf}, T --> T --> T) $ s $ t end
val reduce_set_mem_eqs = @{thms mem_Collect_eq Int_iff Un_iff empty_iff iffI[OF TrueI UNIV_I]}
|> map (mk_meta_eq #> Thm.concl_of #> Logic.dest_equals)
fun reduce_set_mem ctxt x S = let
val t = HOLogic.mk_mem (x, S)
val t' = Pattern.rewrite_term (Proof_Context.theory_of ctxt)
reduce_set_mem_eqs [] t
in if t aconv t' then Pretty.writeln (Syntax.pretty_term ctxt (HOLogic.mk_prod (t, t')))
else (); t'
end
fun is_spec_body_const @{const_name Spec} = true
| is_spec_body_const @{const_name guarded_spec_body} = true
| is_spec_body_const _ = false
fun has_reads body = exists_Const (fn (s, T) =>
snd (strip_type T) = @{typ heap_raw_state}
orelse is_spec_body_const s) body
fun has_reads_globals (params : export_params) body = exists_Const (fn (s, T) =>
snd (strip_type T) = @{typ heap_raw_state}
orelse is_spec_body_const s
orelse #rw_global_accs params s <> NONE
orelse #const_globals params (Const (s, T)) <> NONE
) body
fun get_reads_calls ctxt params globals name = let
val thm = Proof_Context.get_thm ctxt (name ^ "_body_def")
|> simplify (put_simpset HOL_basic_ss ctxt addsimps @{thms call_def block_def block_exn_def})
fun calls (Const (@{const_name com.Call}, _) $ proc) = [proc]
| calls (f $ x) = calls f @ calls x
| calls (Abs (_, _, t)) = calls t
| calls _ = []
val reads = (if globals then has_reads_globals params else has_reads)
(Thm.concl_of thm)
val call_to_name = dest_Const #> fst #> Long_Name.base_name
#> unsuffix "_'proc"
in (reads, calls (Thm.concl_of thm) |> map call_to_name) end
fun is_no_read ctxt params globals s = let
fun inner stack s = if member (op =) stack s then true else let
val (reads, calls) = get_reads_calls ctxt params globals s
in not reads andalso forall I (map (inner (s :: stack)) calls) end
in inner [] s end
fun is_no_write ctxt s = let
val thm = Proof_Context.get_thm ctxt (s ^ "_modifies")
val mex = exists_Const (fn (s, _) => s = @{const_name mex}) (Thm.concl_of thm)
in not mex end
fun synthetic_updates ctxt params pref (Const (c, T)) = let
val s = s_st ctxt
val sT = fastype_of s
val xT = range_type T
val upd = Const (suffix Record.updateN c, (xT --> xT) --> sT --> sT)
$ Abs ("v", xT, Bound 0) $ s
|> Syntax.check_term ctxt
val upds = convert_param_upds ctxt params upd
in map (apfst (prefix pref)) upds end
| synthetic_updates _ _ _ t = raise TERM ("synthetic_updates", [t])
fun is_no_read_globals ctxt params = is_no_read ctxt params true
fun get_global_valid_assertion ctxt (params : export_params) t = let
val tnames = Term.add_const_names t []
val globs = map_filter (#rw_global_accs params) tnames
@ map_filter (#rw_global_upds params) tnames
fun assert nm = let
val T = Symtab.lookup (#rw_globals_tab params) nm
|> the |> fst |> fastype_of |> range_type
val p = TermsTypes.mk_global_addr_ptr (nm, T)
in convert_op ctxt params "PGlobalValid" "Bool"
[mk_pseudo_acc "HTD" @{typ heap_typ_desc}, ptr_to_typ p, p]
end
val globs = sort_distinct fast_string_ord globs
|> map assert
fun conj (x, y) = "Op And Bool 2 " ^ x ^ " " ^ y
in case globs of [] => NONE
| _ => SOME (foldr1 conj globs)
end
fun emit outfile s = TextIO.output (outfile, s ^ "\n")
fun add_global_valid_assertion outfile ctxt params t n =
case get_global_valid_assertion ctxt params t of NONE =>
(n + 1, string_of_int n)
| SOME ass => (emit outfile (string_of_int (n + 1) ^ " Cond " ^ string_of_int n ^ " Err " ^ ass);
(n + 2, string_of_int (n + 1)))
fun emit_body ctxt outfile params (Const (@{const_name Seq}, _) $ a $ b) n c e = let
val (n, nm) = emit_body ctxt outfile params b n c e
handle TERM (s, ts) => raise TERM (s, b :: ts)
| Empty => raise TERM ("emit_body: got Empty", [b])
val (n, nm) = emit_body ctxt outfile params a n nm e
handle TERM (s, ts) => raise TERM (s, a :: ts)
| Empty => raise TERM ("emit_body: got Empty", [a])
in (n, nm) end
| emit_body ctxt outfile params (Const (@{const_name Catch}, _) $ a $ b) n c e = (case b of
Const (@{const_name com.Skip}, _) => emit_body ctxt outfile params a n c (c, c)
| Const (@{const_name ccatchbrk}, _) $ _ => emit_body ctxt outfile params a n c (fst e, c)
| t => raise TERM ("emit_body ctxt params (Catch)", [t])
)
| emit_body ctxt outfile params (Const (@{const_name creturn}, _) $ _ $ upd $ f) n _ (r, b) =
emit_body ctxt outfile params (@{term com.Basic} $ Abs ("s", dummyT, betapplys (upd,
[Abs ("_", dummyT, betapply (f, Bound 1)), Bound 0]))) n r (r, b)
| emit_body _ _ _ (Const (@{const_name creturn_void}, _) $ _) n _ (r, _) = (n, r)
| emit_body _ _ _ (Const (@{const_name cbreak}, _) $ _) n _ (_, b) = (n, b)
| emit_body _ _ _ (Const (@{const_name com.Skip}, _)) n c _ = (n, c)
| emit_body ctxt outfile params (Const (@{const_name com.Cond}, _) $ S $ a $ b) n c e = let
val (n, nm_a) = emit_body ctxt outfile params a n c e
val (n, nm_b) = emit_body ctxt outfile params b n c e
val s = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) S)
in
emit outfile (string_of_int n ^ " Cond " ^ nm_a ^ " " ^ nm_b ^ " " ^ s);
add_global_valid_assertion outfile ctxt params S n
end
| emit_body ctxt outfile params (Const (@{const_name Guard}, T) $ F $ G $
(Const (@{const_name Guard}, _) $ _ $ G' $ a)) n c e
= emit_body ctxt outfile params (Const (@{const_name Guard}, T) $ F
$ (mk_set_int G G') $ a) n c e
| emit_body ctxt outfile params (Const (@{const_name Guard}, _) $ _ $ G $ a) n c e = let
val (n, nm) = emit_body ctxt outfile params a n c e
val thy = Proof_Context.theory_of ctxt
val G = Pattern.rewrite_term thy
(@{thms guard_arith_simps meta_eq_to_obj_eq[OF ptr_arr_retyps_def]}
|> map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq)) [] G
val s = convert_fetch ctxt params (reduce_set_mem ctxt (s_st ctxt) G)
in
emit outfile (string_of_int n ^ " Cond " ^ nm ^ " Err " ^ s);
add_global_valid_assertion outfile ctxt params G n
end
| emit_body _ _ _ (Const (@{const_name com.Basic}, _) $ Abs (_, _, Bound 0)) n c _
= (n, c)
| emit_body ctxt outfile params (Const (@{const_name com.Basic}, _) $ f) n c _ = let
val upds = convert_param_upds ctxt params (betapply (f, s_st ctxt))
|> filter_out (fn (s, v) => v = "Var " ^ s)
|> map (fn (s, v) => s ^ " " ^ v)