From 1c50485c9a1b3c0595c143432664ab55e59e7991 Mon Sep 17 00:00:00 2001 From: julia Date: Mon, 4 Aug 2025 16:43:01 +1000 Subject: [PATCH] bitfield_gen: apply style fixes Signed-off-by: julia --- tools/bitfield_gen.py | 74 +++++++++++++++++++++---------------------- 1 file changed, 37 insertions(+), 37 deletions(-) diff --git a/tools/bitfield_gen.py b/tools/bitfield_gen.py index 11f0bf3dd..82fe2e0b9 100755 --- a/tools/bitfield_gen.py +++ b/tools/bitfield_gen.py @@ -945,10 +945,10 @@ proof_templates = { 'get_tag_spec': [ '''lemma (in ''' + loc_name + ''') %(name)s_get_%(tagname)s_spec: "\\s. \\ \\ {s} - \\%(ret_name)s :== ''' \ - '''PROC %(name)s_get_%(tagname)s(\\%(name)s) - \\\\%(ret_name)s = ''' \ - '''%(name)s_get_tag \\<^bsup>s\\<^esup>%(name)s\\"''', + \\%(ret_name)s :== ''' + '''PROC %(name)s_get_%(tagname)s(\\%(name)s) + \\\\%(ret_name)s = ''' + '''%(name)s_get_tag \\<^bsup>s\\<^esup>%(name)s\\"''', ''' apply(rule allI, rule conseqPre, vcg) apply (clarsimp) apply (simp add:%(name)s_get_tag_def mask_shift_simps guard_simps) @@ -990,13 +990,13 @@ proof_templates = { 'empty_union_new_spec': [ - '''lemma (in ''' + loc_name + ''') ''' \ + '''lemma (in ''' + loc_name + ''') ''' '''%(name)s_%(block)s_new_spec: "\\s. \\ \\ {s} - \\ret__struct_%(name)s_C :== ''' \ - '''PROC %(name)s_%(block)s_new() - \\%(name)s_get_tag \\ret__struct_%(name)s_C = ''' \ - '''scast %(name)s_%(block)s\\"''', + \\ret__struct_%(name)s_C :== ''' + '''PROC %(name)s_%(block)s_new() + \\%(name)s_get_tag \\ret__struct_%(name)s_C = ''' + '''scast %(name)s_%(block)s\\"''', ''' apply(rule allI, rule conseqPre, vcg) by (clarsimp simp: guard_simps %(name)s_lift_def @@ -1007,16 +1007,16 @@ proof_templates = { word_of_int_hom_syms)'''], 'union_new_spec': [ - '''lemma (in ''' + loc_name + ''') ''' \ + '''lemma (in ''' + loc_name + ''') ''' '''%(name)s_%(block)s_new_spec: "\\s. \\ \\ {s} - \\ret__struct_%(name)s_C :== ''' \ - '''PROC %(name)s_%(block)s_new(%(args)s) - \\%(name)s_%(block)s_lift ''' \ - '''\\ret__struct_%(name)s_C = \\ + \\ret__struct_%(name)s_C :== ''' + '''PROC %(name)s_%(block)s_new(%(args)s) + \\%(name)s_%(block)s_lift ''' + '''\\ret__struct_%(name)s_C = \\ %(field_eqs)s \\ \\ - %(name)s_get_tag \\ret__struct_%(name)s_C = ''' \ - '''scast %(name)s_%(block)s\\"''', + %(name)s_get_tag \\ret__struct_%(name)s_C = ''' + '''scast %(name)s_%(block)s\\"''', ''' apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists) apply (rule context_conjI[THEN iffD1[OF conj_commute]], @@ -1078,17 +1078,17 @@ proof_templates = { done'''], 'union_get_spec': [ - '''lemma (in ''' + loc_name + ''') ''' \ + '''lemma (in ''' + loc_name + ''') ''' '''%(name)s_%(block)s_get_%(field)s_spec: - "\\s. \\ \\ ''' \ -'''\\s. %(name)s_get_tag \\%(name)s = ''' \ + "\\s. \\ \\ ''' + '''\\s. %(name)s_get_tag \\%(name)s = ''' '''scast %(name)s_%(block)s\\ - \\%(ret_name)s :== ''' \ - '''PROC %(name)s_%(block)s_get_%(field)s(\\%(name)s) - \\\\%(ret_name)s = ''' \ - '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ - '''(%(name)s_%(block)s_lift \\<^bsup>s\\<^esup>%(name)s)''' \ - '''\\"''', + \\%(ret_name)s :== ''' + '''PROC %(name)s_%(block)s_get_%(field)s(\\%(name)s) + \\\\%(ret_name)s = ''' + '''%(name)s_%(block)s_CL.%(field)s_CL ''' + '''(%(name)s_%(block)s_lift \\<^bsup>s\\<^esup>%(name)s)''' + '''\\"''', ''' apply(rule allI, rule conseqPre, vcg) apply (clarsimp simp:guard_simps) apply (simp add:%(name)s_%(block)s_lift_def) @@ -1107,19 +1107,19 @@ proof_templates = { done'''], 'union_set_spec': [ - '''lemma (in ''' + loc_name + ''') ''' \ + '''lemma (in ''' + loc_name + ''') ''' '''%(name)s_%(block)s_set_%(field)s_spec: - "\\s. \\ \\ ''' \ -'''\\s. %(name)s_get_tag \\%(name)s = ''' \ + "\\s. \\ \\ ''' + '''\\s. %(name)s_get_tag \\%(name)s = ''' '''scast %(name)s_%(block)s\\ - \\ret__struct_%(name)s_C :== ''' \ - '''PROC %(name)s_%(block)s_set_%(field)s(\\%(name)s, \\v%(base)d) - \\%(name)s_%(block)s_lift \\ret__struct_%(name)s_C = ''' \ - '''%(name)s_%(block)s_lift \\<^bsup>s\\<^esup>%(name)s \\ ''' \ - '''%(name)s_%(block)s_CL.%(field)s_CL ''' \ + \\ret__struct_%(name)s_C :== ''' + '''PROC %(name)s_%(block)s_set_%(field)s(\\%(name)s, \\v%(base)d) + \\%(name)s_%(block)s_lift \\ret__struct_%(name)s_C = ''' + '''%(name)s_%(block)s_lift \\<^bsup>s\\<^esup>%(name)s \\ ''' + '''%(name)s_%(block)s_CL.%(field)s_CL ''' ''':= %(sign_extend)s (\\<^bsup>s\\<^esup>v%(base)d AND %(mask)s)\\ \\ - %(name)s_get_tag \\ret__struct_%(name)s_C = ''' \ - '''scast %(name)s_%(block)s\\"''', + %(name)s_get_tag \\ret__struct_%(name)s_C = ''' + '''scast %(name)s_%(block)s\\"''', ''' apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule context_conjI[THEN iffD1[OF conj_commute]], @@ -1207,7 +1207,7 @@ def emit_named(name, params, string): # Emit a named definition/proof, only when the given name is in # params.names - if(name in params.names): + if name in params.names: print(string, file=params.output) print(file=params.output) @@ -2281,7 +2281,7 @@ class TaggedUnion: self.classes[w] <<= self.tag_offset[w] - self.class_offset used_widths = sorted(list(used)) - assert(len(used_widths) > 0) + assert len(used_widths) > 0 if not self.classes: self.classes = {used_widths[0]: 0}