Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

C heap tactic #507

Draft
wants to merge 6 commits into
base: master
Choose a base branch
from
Draft

C heap tactic #507

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
66b863c
First port of the umm_strg tactic
simonjwinwood Jul 26, 2022
99d5873
Bugfixes and whitespace
simonjwinwood Jul 26, 2022
7cbb942
Added Thm.solve_constraints to the cached theorems
simonjwinwood Jul 28, 2022
717cf08
Merge branch 'master' into wip/heap-tactic
lsf37 Oct 23, 2022
91278ee
Merge branch 'seL4:master' into wip/heap-tactic
simonjwinwood Jun 25, 2024
ab40b94
Syntax changes
Jun 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions tools/c-parser/calculate_state.ML
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ sig
val mk_thy_types :
csenv -> bool -> theory ->
theory *
(string * (string * typ * int ctype) list) list
(string * typ * (string * typ * int ctype) list) list

val mk_thy_decls :
staterep -> {mstate_ty : typ,gstate_ty : typ, owners : string list} ->
Expand Down Expand Up @@ -432,7 +432,7 @@ fun mk_thy_types cse install thy = let
fun new_rcdinfo (recname,flds) thy = let
fun fldtys (fldname, cty) = (fldname, ctype_to_typ (thy,cty), cty)
in
(recname, map fldtys flds)
(recname, ctype_to_typ (thy, StructTy recname), map fldtys flds)
end

fun rcddecls_phase0 (recflds, thy) = let
Expand Down Expand Up @@ -535,11 +535,11 @@ fun mk_thy_types cse install thy = let
end

fun rcddecl_phase1 (p as (recname, _ (* flds *)), (thy, st, rcdacc)) = let
val rcdinfo = new_rcdinfo p thy
val rcdinfo as (recname, _, flds) = new_rcdinfo p thy
val (st, thy1) =
if install then
(informStr (2, "Proving UMM properties for struct "^recname);
struct_type cse {struct_type = rcdinfo, state = st}
struct_type cse {struct_type = (recname, flds), state = st}
thy)
else (st, thy)
in
Expand Down
12 changes: 8 additions & 4 deletions tools/c-parser/isar_install.ML
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,8 @@ sig
val installed_C_files : theory
-> {c_filename : string, locale_names : string list,
options: (bool * bool * bool),
additional_options: additional_options list} list
additional_options: additional_options list,
struct_information: (string * typ * (string * typ * int CalculateState.ctype) list) list} list
end

structure IsarInstall : ISAR_INSTALL =
Expand Down Expand Up @@ -73,7 +74,8 @@ datatype additional_options = MachineState of string | GhostState of string | CR

type install_data = {c_filename : string, locale_names : string list,
options: (bool * bool * bool),
additional_options: additional_options list}
additional_options: additional_options list,
struct_information: (string * typ * (string * typ * int CalculateState.ctype) list) list }
structure C_Installs = Theory_Data
(struct
type T = install_data list
Expand Down Expand Up @@ -454,13 +456,15 @@ in
C_Installs.map (fn ss =>
{c_filename = s, locale_names = [globloc, loc2],
options = (ms, install_typs, install_defs),
additional_options = statetylist} :: ss) thy
additional_options = statetylist,
struct_information = rcdinfo} :: ss) thy
end
else
C_Installs.map (fn ss =>
{c_filename = s, locale_names = [],
options = (ms, install_typs, install_defs),
additional_options = statetylist} :: ss) thy
additional_options = statetylist,
struct_information = rcdinfo} :: ss) thy
end handle e as TYPE (s,tys,tms) =>
(Feedback.informStr (0, s ^ "\n" ^
Int.toString (length tms) ^ " term(s): " ^
Expand Down
4 changes: 2 additions & 2 deletions tools/c-parser/stmt_translation.ML
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -683,9 +683,9 @@ in
end

fun lookup_fld alist (s, f) =
case assoc(alist, s) of
case List.find (fn (recname, _, _) => recname = s) alist of
NONE => error ("No struct information for type "^s)
| SOME flds => let
| SOME (_, _, flds) => let
in
case List.find (fn (fldname, ty, cty) => fldname = f) flds of
NONE => error ("No type information for fld "^f^" in struct "^s)
Expand Down
Loading
Loading