From 2b922cb0328c687090bbb64d756594f073c16386 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Thu, 20 May 2021 15:25:24 +0200 Subject: [PATCH] Preserve different C types in the frontend. --- examples/proofs/intptr/generated_code.v | 122 +++++++++--------- frontend/ail_to_coq.ml | 4 +- frontend/coq_ast.ml | 12 +- frontend/coq_pp.ml | 3 + .../proofs/page_alloc/generated_code.v | 2 +- .../pkvm/proofs/early_alloc/generated_code.v | 40 +++--- theories/lang/int_type.v | 1 + 7 files changed, 95 insertions(+), 89 deletions(-) diff --git a/examples/proofs/intptr/generated_code.v b/examples/proofs/intptr/generated_code.v index c5912afb..8bcc9d42 100644 --- a/examples/proofs/intptr/generated_code.v +++ b/examples/proofs/intptr/generated_code.v @@ -207,15 +207,15 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t) + ("i", it_layout uintptr_t) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_6 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_7 (use{void*} (LocInfoE loc_8 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_6 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_7 (use{void*} (LocInfoE loc_8 ("p"))))) ; locinfo: loc_3 ; - Return (LocInfoE loc_4 (use{it_layout size_t} (LocInfoE loc_5 ("i")))) + Return (LocInfoE loc_4 (use{it_layout uintptr_t} (LocInfoE loc_5 ("i")))) ]> $∅ )%E |}. @@ -226,15 +226,15 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t) + ("i", it_layout uintptr_t) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_17 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_18 (use{void*} (LocInfoE loc_19 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_17 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_18 (use{void*} (LocInfoE loc_19 ("p"))))) ; locinfo: loc_14 ; - Return (LocInfoE loc_15 (use{it_layout size_t} (LocInfoE loc_16 ("i")))) + Return (LocInfoE loc_15 (use{it_layout uintptr_t} (LocInfoE loc_16 ("i")))) ]> $∅ )%E |}. @@ -245,15 +245,15 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t) + ("i", it_layout uintptr_t) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_30 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_31 (use{void*} (LocInfoE loc_32 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_30 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_31 (use{void*} (LocInfoE loc_32 ("p"))))) ; locinfo: loc_25 ; - Return (LocInfoE loc_26 ((LocInfoE loc_27 (use{it_layout size_t} (LocInfoE loc_28 ("i")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_29 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_29 (i2v 0 i32)))))) + Return (LocInfoE loc_26 ((LocInfoE loc_27 (use{it_layout uintptr_t} (LocInfoE loc_28 ("i")))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_29 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_29 (i2v 0 i32)))))) ]> $∅ )%E |}. @@ -265,18 +265,18 @@ Section code. ("p2", void*) ]; f_local_vars := [ - ("i2", it_layout size_t); - ("i1", it_layout size_t) + ("i2", it_layout uintptr_t); + ("i1", it_layout uintptr_t) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i1" <-{ it_layout size_t } - LocInfoE loc_58 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_59 (use{void*} (LocInfoE loc_60 ("p1"))))) ; - "i2" <-{ it_layout size_t } - LocInfoE loc_53 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_54 (use{void*} (LocInfoE loc_55 ("p2"))))) ; + "i1" <-{ it_layout uintptr_t } + LocInfoE loc_58 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_59 (use{void*} (LocInfoE loc_60 ("p1"))))) ; + "i2" <-{ it_layout uintptr_t } + LocInfoE loc_53 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_54 (use{void*} (LocInfoE loc_55 ("p2"))))) ; locinfo: loc_48 ; - if: LocInfoE loc_48 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_48 ((LocInfoE loc_49 (use{it_layout size_t} (LocInfoE loc_50 ("i1")))) ≤{IntOp size_t, IntOp size_t} (LocInfoE loc_51 (use{it_layout size_t} (LocInfoE loc_52 ("i2"))))))) + if: LocInfoE loc_48 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_48 ((LocInfoE loc_49 (use{it_layout uintptr_t} (LocInfoE loc_50 ("i1")))) ≤{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_51 (use{it_layout uintptr_t} (LocInfoE loc_52 ("i2"))))))) then locinfo: loc_44 ; Goto "#2" @@ -286,11 +286,11 @@ Section code. ]> $ <[ "#1" := locinfo: loc_40 ; - Return (LocInfoE loc_41 (use{it_layout size_t} (LocInfoE loc_42 ("i2")))) + Return (LocInfoE loc_41 (use{it_layout uintptr_t} (LocInfoE loc_42 ("i2")))) ]> $ <[ "#2" := locinfo: loc_44 ; - Return (LocInfoE loc_45 (use{it_layout size_t} (LocInfoE loc_46 ("i1")))) + Return (LocInfoE loc_45 (use{it_layout uintptr_t} (LocInfoE loc_46 ("i1")))) ]> $ <[ "#3" := locinfo: loc_40 ; @@ -306,18 +306,18 @@ Section code. ("p2", void*) ]; f_local_vars := [ - ("i2", it_layout size_t); - ("i1", it_layout size_t) + ("i2", it_layout uintptr_t); + ("i1", it_layout uintptr_t) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i1" <-{ it_layout size_t } - LocInfoE loc_86 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_87 (use{void*} (LocInfoE loc_88 ("p1"))))) ; - "i2" <-{ it_layout size_t } - LocInfoE loc_81 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_82 (use{void*} (LocInfoE loc_83 ("p2"))))) ; + "i1" <-{ it_layout uintptr_t } + LocInfoE loc_86 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_87 (use{void*} (LocInfoE loc_88 ("p1"))))) ; + "i2" <-{ it_layout uintptr_t } + LocInfoE loc_81 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_82 (use{void*} (LocInfoE loc_83 ("p2"))))) ; locinfo: loc_76 ; - if: LocInfoE loc_76 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_76 ((LocInfoE loc_77 (use{it_layout size_t} (LocInfoE loc_78 ("i1")))) ≤{IntOp size_t, IntOp size_t} (LocInfoE loc_79 (use{it_layout size_t} (LocInfoE loc_80 ("i2"))))))) + if: LocInfoE loc_76 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_76 ((LocInfoE loc_77 (use{it_layout uintptr_t} (LocInfoE loc_78 ("i1")))) ≤{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_79 (use{it_layout uintptr_t} (LocInfoE loc_80 ("i2"))))))) then locinfo: loc_72 ; Goto "#2" @@ -327,11 +327,11 @@ Section code. ]> $ <[ "#1" := locinfo: loc_68 ; - Return (LocInfoE loc_69 (use{it_layout size_t} (LocInfoE loc_70 ("i2")))) + Return (LocInfoE loc_69 (use{it_layout uintptr_t} (LocInfoE loc_70 ("i2")))) ]> $ <[ "#2" := locinfo: loc_72 ; - Return (LocInfoE loc_73 (use{it_layout size_t} (LocInfoE loc_74 ("i1")))) + Return (LocInfoE loc_73 (use{it_layout uintptr_t} (LocInfoE loc_74 ("i1")))) ]> $ <[ "#3" := locinfo: loc_68 ; @@ -346,16 +346,16 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_103 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_104 (use{void*} (LocInfoE loc_105 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_103 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_104 (use{void*} (LocInfoE loc_105 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_98 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_99 (use{it_layout size_t} (LocInfoE loc_100 ("i"))))) ; + LocInfoE loc_98 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_99 (use{it_layout uintptr_t} (LocInfoE loc_100 ("i"))))) ; locinfo: loc_95 ; Return (LocInfoE loc_96 (use{void*} (LocInfoE loc_97 ("q")))) ]> $∅ @@ -368,16 +368,16 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_122 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_123 (use{void*} (LocInfoE loc_124 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_122 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_123 (use{void*} (LocInfoE loc_124 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_115 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_116 ((LocInfoE loc_117 (use{it_layout size_t} (LocInfoE loc_118 ("i")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_119 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_119 (i2v 0 i32))))))) ; + LocInfoE loc_115 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_116 ((LocInfoE loc_117 (use{it_layout uintptr_t} (LocInfoE loc_118 ("i")))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_119 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_119 (i2v 0 i32))))))) ; locinfo: loc_112 ; Return (LocInfoE loc_113 (use{void*} (LocInfoE loc_114 ("q")))) ]> $∅ @@ -390,16 +390,16 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_144 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_145 (use{void*} (LocInfoE loc_146 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_144 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_145 (use{void*} (LocInfoE loc_146 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_137 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_137 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_138 ((LocInfoE loc_139 (use{it_layout size_t} (LocInfoE loc_140 ("i")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_141 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_141 (i2v 0 i32))))))))) ; + LocInfoE loc_137 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_137 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_138 ((LocInfoE loc_139 (use{it_layout uintptr_t} (LocInfoE loc_140 ("i")))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_141 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_141 (i2v 0 i32))))))))) ; locinfo: loc_131 ; Return (LocInfoE loc_132 (CopyAllocId (PtrOp) (LocInfoE loc_135 (use{void*} (LocInfoE loc_136 ("q")))) (LocInfoE loc_133 (use{void*} (LocInfoE loc_134 ("p")))))) ]> $∅ @@ -412,17 +412,17 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("r", it_layout i32); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_168 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_169 (use{void*} (LocInfoE loc_170 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_168 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_169 (use{void*} (LocInfoE loc_170 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_163 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_164 (use{it_layout size_t} (LocInfoE loc_165 ("i"))))) ; + LocInfoE loc_163 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_164 (use{it_layout uintptr_t} (LocInfoE loc_165 ("i"))))) ; "r" <-{ it_layout i32 } LocInfoE loc_157 (use{it_layout i32} (LocInfoE loc_159 (!{void*} (LocInfoE loc_160 ("q"))))) ; locinfo: loc_154 ; @@ -437,17 +437,17 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("r", it_layout i32); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_201 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_202 (use{void*} (LocInfoE loc_203 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_201 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_202 (use{void*} (LocInfoE loc_203 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_194 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_195 ((LocInfoE loc_196 (use{it_layout size_t} (LocInfoE loc_197 ("i")))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_198 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_198 (i2v 1 i32))))))) ; + LocInfoE loc_194 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_195 ((LocInfoE loc_196 (use{it_layout uintptr_t} (LocInfoE loc_197 ("i")))) ×{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_198 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_198 (i2v 1 i32))))))) ; locinfo: loc_177 ; LocInfoE loc_188 ("q") <-{ void* } LocInfoE loc_189 (CopyAllocId (PtrOp) (LocInfoE loc_192 (use{void*} (LocInfoE loc_193 ("q")))) (LocInfoE loc_190 (use{void*} (LocInfoE loc_191 ("p"))))) ; @@ -465,16 +465,16 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_225 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_226 (use{void*} (LocInfoE loc_227 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_225 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_226 (use{void*} (LocInfoE loc_227 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_215 (CopyAllocId (PtrOp) (LocInfoE loc_218 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_219 ((LocInfoE loc_220 (use{it_layout size_t} (LocInfoE loc_221 ("i")))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_222 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_222 (i2v 1 i32)))))))) (LocInfoE loc_216 (use{void*} (LocInfoE loc_217 ("p"))))) ; + LocInfoE loc_215 (CopyAllocId (PtrOp) (LocInfoE loc_218 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_219 ((LocInfoE loc_220 (use{it_layout uintptr_t} (LocInfoE loc_221 ("i")))) ×{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_222 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_222 (i2v 1 i32)))))))) (LocInfoE loc_216 (use{void*} (LocInfoE loc_217 ("p"))))) ; locinfo: loc_210 ; Return (LocInfoE loc_211 (use{it_layout i32} (LocInfoE loc_213 (!{void*} (LocInfoE loc_214 ("q")))))) ]> $∅ @@ -487,16 +487,16 @@ Section code. ("p", void*) ]; f_local_vars := [ - ("i", it_layout size_t); + ("i", it_layout uintptr_t); ("q", void*) ]; f_init := "#0"; f_code := ( <[ "#0" := - "i" <-{ it_layout size_t } - LocInfoE loc_249 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_250 (use{void*} (LocInfoE loc_251 ("p"))))) ; + "i" <-{ it_layout uintptr_t } + LocInfoE loc_249 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_250 (use{void*} (LocInfoE loc_251 ("p"))))) ; "q" <-{ void* } - LocInfoE loc_242 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_243 ((LocInfoE loc_244 (use{it_layout size_t} (LocInfoE loc_245 ("i")))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_246 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_246 (i2v 1 i32))))))) ; + LocInfoE loc_242 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_243 ((LocInfoE loc_244 (use{it_layout uintptr_t} (LocInfoE loc_245 ("i")))) ×{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_246 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_246 (i2v 1 i32))))))) ; locinfo: loc_234 ; Return (LocInfoE loc_235 (use{it_layout i32} (LocInfoE loc_237 (LValue (LocInfoE loc_237 (CopyAllocId (PtrOp) (LocInfoE loc_240 (use{void*} (LocInfoE loc_241 ("q")))) (LocInfoE loc_238 (use{void*} (LocInfoE loc_239 ("p")))))))))) ]> $∅ @@ -506,7 +506,7 @@ Section code. (* Definition of function [int_to_ptr]. *) Definition impl_int_to_ptr : function := {| f_args := [ - ("p", it_layout size_t) + ("p", it_layout uintptr_t) ]; f_local_vars := [ ("q", void*) @@ -515,9 +515,9 @@ Section code. f_code := ( <[ "#0" := "q" <-{ void* } - LocInfoE loc_263 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_264 ((LocInfoE loc_265 (use{it_layout size_t} (LocInfoE loc_266 ("p")))) ×{IntOp size_t, IntOp size_t} (LocInfoE loc_267 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_267 (i2v 1 i32))))))) ; + LocInfoE loc_263 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_264 ((LocInfoE loc_265 (use{it_layout uintptr_t} (LocInfoE loc_266 ("p")))) ×{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_267 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_267 (i2v 1 i32))))))) ; locinfo: loc_257 ; - Return (LocInfoE loc_258 (CopyAllocId (IntOp size_t) (LocInfoE loc_261 (use{void*} (LocInfoE loc_262 ("q")))) (LocInfoE loc_259 (use{it_layout size_t} (LocInfoE loc_260 ("p")))))) + Return (LocInfoE loc_258 (CopyAllocId (IntOp uintptr_t) (LocInfoE loc_261 (use{void*} (LocInfoE loc_262 ("q")))) (LocInfoE loc_259 (use{it_layout uintptr_t} (LocInfoE loc_260 ("p")))))) ]> $∅ )%E |}. diff --git a/frontend/ail_to_coq.ml b/frontend/ail_to_coq.ml index ebdd5726..ac62c864 100644 --- a/frontend/ail_to_coq.ml +++ b/frontend/ail_to_coq.ml @@ -101,7 +101,7 @@ let rec translate_int_type : loc -> i_type -> Coq_ast.int_type = fun loc i -> | Int_leastN_t(_) -> not_impl loc "size_of_base_type (Int_leastN_t)" | Int_fastN_t(_) -> not_impl loc "size_of_base_type (Int_fastN_t)" | Intmax_t -> not_impl loc "size_of_base_type (Intmax_t)" - | Intptr_t -> ItSize_t(signed) + | Intptr_t -> ItIntptr_t(signed) (* Normal integer types *) | Ichar | Short | Int_ | Long | LongLong -> let ity = if signed then Signed(i) else Unsigned i in @@ -123,7 +123,7 @@ let rec translate_int_type : loc -> i_type -> Coq_ast.int_type = fun loc i -> | Wchar_t -> not_impl loc "layout_of (Wchar_t)" | Wint_t -> not_impl loc "layout_of (Win_t)" | Size_t -> ItSize_t(false) - | Ptrdiff_t -> ItSize_t(true) + | Ptrdiff_t -> ItPtrdiff_t (** [layout_of fa c_ty] translates the C type [c_ty] into a layout. Note that argument [fa] must be set to [true] when in function arguments, since this diff --git a/frontend/coq_ast.ml b/frontend/coq_ast.ml index d1ebef69..b4d51b3c 100644 --- a/frontend/coq_ast.ml +++ b/frontend/coq_ast.ml @@ -2,11 +2,13 @@ open Extra open Rc_annot type int_type = - | ItSize_t of bool (* signed *) - | ItI8 of bool (* signed *) - | ItI16 of bool (* signed *) - | ItI32 of bool (* signed *) - | ItI64 of bool (* signed *) + | ItSize_t of bool (* signed *) + | ItIntptr_t of bool (* signed *) + | ItPtrdiff_t + | ItI8 of bool (* signed *) + | ItI16 of bool (* signed *) + | ItI32 of bool (* signed *) + | ItI64 of bool (* signed *) | ItBool type layout = diff --git a/frontend/coq_pp.ml b/frontend/coq_pp.ml index 3b5e912d..87c0c03a 100644 --- a/frontend/coq_pp.ml +++ b/frontend/coq_pp.ml @@ -67,6 +67,9 @@ let pp_int_type : Coq_ast.int_type pp = fun ff it -> match it with | ItSize_t(true) -> pp "ssize_t" | ItSize_t(false) -> pp "size_t" + | ItIntptr_t(true) -> pp "intptr_t" + | ItIntptr_t(false) -> pp "uintptr_t" + | ItPtrdiff_t -> pp "ptrdiff_t" | ItI8(true) -> pp "i8" | ItI8(false) -> pp "u8" | ItI16(true) -> pp "i16" diff --git a/linux/casestudies/proofs/page_alloc/generated_code.v b/linux/casestudies/proofs/page_alloc/generated_code.v index 07320d1c..9363826a 100644 --- a/linux/casestudies/proofs/page_alloc/generated_code.v +++ b/linux/casestudies/proofs/page_alloc/generated_code.v @@ -1175,7 +1175,7 @@ Section code. f_code := ( <[ "#0" := locinfo: loc_185 ; - Return (LocInfoE loc_186 ((LocInfoE loc_187 (UnOp (CastOp $ IntOp u64) (IntOp ssize_t) (LocInfoE loc_188 ((LocInfoE loc_189 (use{void*} (LocInfoE loc_190 ("page")))) -{PtrOp, PtrOp} (LocInfoE loc_191 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_192 (use{void*} (LocInfoE loc_193 (global___hyp_vmemmap)))))))))) <<{IntOp u64, IntOp u64} (LocInfoE loc_194 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_194 (i2v 12 i32)))))) + Return (LocInfoE loc_186 ((LocInfoE loc_187 (UnOp (CastOp $ IntOp u64) (IntOp ptrdiff_t) (LocInfoE loc_188 ((LocInfoE loc_189 (use{void*} (LocInfoE loc_190 ("page")))) -{PtrOp, PtrOp} (LocInfoE loc_191 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_192 (use{void*} (LocInfoE loc_193 (global___hyp_vmemmap)))))))))) <<{IntOp u64, IntOp u64} (LocInfoE loc_194 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_194 (i2v 12 i32)))))) ]> $∅ )%E |}. diff --git a/linux/pkvm/proofs/early_alloc/generated_code.v b/linux/pkvm/proofs/early_alloc/generated_code.v index cd88c587..0e5e52d1 100644 --- a/linux/pkvm/proofs/early_alloc/generated_code.v +++ b/linux/pkvm/proofs/early_alloc/generated_code.v @@ -140,8 +140,8 @@ Section code. (* Definition of struct [region]. *) Program Definition struct_region := {| sl_members := [ - (Some "end", it_layout size_t); - (Some "cur", it_layout size_t); + (Some "end", it_layout uintptr_t); + (Some "cur", it_layout uintptr_t); (Some "base", void*) ]; |}. @@ -157,7 +157,7 @@ Section code. f_code := ( <[ "#0" := locinfo: loc_2 ; - Return (LocInfoE loc_3 ((LocInfoE loc_4 ((LocInfoE loc_5 (use{it_layout size_t} (LocInfoE loc_6 ((LocInfoE loc_7 (global_mem)) at{struct_region} "cur")))) -{IntOp size_t, IntOp size_t} (LocInfoE loc_8 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_9 (use{void*} (LocInfoE loc_10 ((LocInfoE loc_11 (global_mem)) at{struct_region} "base")))))))) >>{IntOp size_t, IntOp size_t} (LocInfoE loc_12 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_12 (i2v 12 i32)))))) + Return (LocInfoE loc_3 (UnOp (CastOp $ IntOp size_t) (IntOp uintptr_t) (LocInfoE loc_3 ((LocInfoE loc_4 ((LocInfoE loc_5 (use{it_layout uintptr_t} (LocInfoE loc_6 ((LocInfoE loc_7 (global_mem)) at{struct_region} "cur")))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_8 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_9 (use{void*} (LocInfoE loc_10 ((LocInfoE loc_11 (global_mem)) at{struct_region} "base")))))))) >>{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_12 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_12 (i2v 12 i32)))))))) ]> $∅ )%E |}. @@ -169,14 +169,14 @@ Section code. ]; f_local_vars := [ ("i", it_layout u32); - ("ret", it_layout size_t); - ("p", it_layout size_t) + ("ret", it_layout uintptr_t); + ("p", it_layout uintptr_t) ]; f_init := "#0"; f_code := ( <[ "#0" := - "ret" <-{ it_layout size_t } - LocInfoE loc_103 (use{it_layout size_t} (LocInfoE loc_104 ((LocInfoE loc_105 (global_mem)) at{struct_region} "cur"))) ; + "ret" <-{ it_layout uintptr_t } + LocInfoE loc_103 (use{it_layout uintptr_t} (LocInfoE loc_104 ((LocInfoE loc_105 (global_mem)) at{struct_region} "cur"))) ; locinfo: loc_99 ; if: LocInfoE loc_99 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_99 ((UnOp (CastOp $ IntOp u32) (IntOp i32) (i2v 0 i32)) ={IntOp u32, IntOp u32} (LocInfoE loc_101 (use{it_layout u32} (LocInfoE loc_102 ("nr_pages"))))))) then @@ -190,10 +190,10 @@ Section code. locinfo: loc_17 ; expr: (LocInfoE loc_93 (&(LocInfoE loc_94 ((LocInfoE loc_95 (global_mem)) at{struct_region} "base")))) ; locinfo: loc_19 ; - LocInfoE loc_83 ((LocInfoE loc_84 (global_mem)) at{struct_region} "cur") <-{ it_layout size_t } - LocInfoE loc_85 ((LocInfoE loc_86 (use{it_layout size_t} (LocInfoE loc_87 ((LocInfoE loc_88 (global_mem)) at{struct_region} "cur")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_89 (UnOp (CastOp $ IntOp size_t) (IntOp u32) (LocInfoE loc_89 ((LocInfoE loc_90 (use{it_layout u32} (LocInfoE loc_91 ("nr_pages")))) <<{IntOp u32, IntOp u32} (LocInfoE loc_92 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_92 (i2v 12 i32))))))))) ; + LocInfoE loc_83 ((LocInfoE loc_84 (global_mem)) at{struct_region} "cur") <-{ it_layout uintptr_t } + LocInfoE loc_85 ((LocInfoE loc_86 (use{it_layout uintptr_t} (LocInfoE loc_87 ((LocInfoE loc_88 (global_mem)) at{struct_region} "cur")))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_89 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u32) (LocInfoE loc_89 ((LocInfoE loc_90 (use{it_layout u32} (LocInfoE loc_91 ("nr_pages")))) <<{IntOp u32, IntOp u32} (LocInfoE loc_92 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_92 (i2v 12 i32))))))))) ; locinfo: loc_76 ; - if: LocInfoE loc_76 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_76 ((LocInfoE loc_77 (use{it_layout size_t} (LocInfoE loc_78 ((LocInfoE loc_79 (global_mem)) at{struct_region} "cur")))) >{IntOp size_t, IntOp size_t} (LocInfoE loc_80 (use{it_layout size_t} (LocInfoE loc_81 ((LocInfoE loc_82 (global_mem)) at{struct_region} "end"))))))) + if: LocInfoE loc_76 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_76 ((LocInfoE loc_77 (use{it_layout uintptr_t} (LocInfoE loc_78 ((LocInfoE loc_79 (global_mem)) at{struct_region} "cur")))) >{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_80 (use{it_layout uintptr_t} (LocInfoE loc_81 ((LocInfoE loc_82 (global_mem)) at{struct_region} "end"))))))) then locinfo: loc_68 ; Goto "#6" @@ -222,21 +222,21 @@ Section code. locinfo: loc_33 ; expr: (LocInfoE loc_57 (&(LocInfoE loc_58 ((LocInfoE loc_59 (global_mem)) at{struct_region} "base")))) ; locinfo: loc_35 ; - LocInfoE loc_49 ("p") <-{ it_layout size_t } - LocInfoE loc_50 ((LocInfoE loc_51 (use{it_layout size_t} (LocInfoE loc_52 ("ret")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_53 (UnOp (CastOp $ IntOp size_t) (IntOp u32) (LocInfoE loc_53 ((LocInfoE loc_54 (use{it_layout u32} (LocInfoE loc_55 ("i")))) <<{IntOp u32, IntOp u32} (LocInfoE loc_56 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_56 (i2v 12 i32))))))))) ; + LocInfoE loc_49 ("p") <-{ it_layout uintptr_t } + LocInfoE loc_50 ((LocInfoE loc_51 (use{it_layout uintptr_t} (LocInfoE loc_52 ("ret")))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_53 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u32) (LocInfoE loc_53 ((LocInfoE loc_54 (use{it_layout u32} (LocInfoE loc_55 ("i")))) <<{IntOp u32, IntOp u32} (LocInfoE loc_56 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_56 (i2v 12 i32))))))))) ; locinfo: loc_36 ; - expr: (LocInfoE loc_36 (Call (LocInfoE loc_41 (global_clear_page)) [@{expr} LocInfoE loc_42 (CopyAllocId (PtrOp) (LocInfoE loc_46 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_47 (use{it_layout size_t} (LocInfoE loc_48 ("p")))))) (LocInfoE loc_43 (use{void*} (LocInfoE loc_44 ((LocInfoE loc_45 (global_mem)) at{struct_region} "base"))))) ])) ; + expr: (LocInfoE loc_36 (Call (LocInfoE loc_41 (global_clear_page)) [@{expr} LocInfoE loc_42 (CopyAllocId (PtrOp) (LocInfoE loc_46 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_47 (use{it_layout uintptr_t} (LocInfoE loc_48 ("p")))))) (LocInfoE loc_43 (use{void*} (LocInfoE loc_44 ((LocInfoE loc_45 (global_mem)) at{struct_region} "base"))))) ])) ; locinfo: loc_37 ; Goto "continue5" ]> $ <[ "#5" := locinfo: loc_24 ; - Return (LocInfoE loc_25 (CopyAllocId (PtrOp) (LocInfoE loc_29 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_30 (use{it_layout size_t} (LocInfoE loc_31 ("ret")))))) (LocInfoE loc_26 (use{void*} (LocInfoE loc_27 ((LocInfoE loc_28 (global_mem)) at{struct_region} "base")))))) + Return (LocInfoE loc_25 (CopyAllocId (PtrOp) (LocInfoE loc_29 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_30 (use{it_layout uintptr_t} (LocInfoE loc_31 ("ret")))))) (LocInfoE loc_26 (use{void*} (LocInfoE loc_27 ((LocInfoE loc_28 (global_mem)) at{struct_region} "base")))))) ]> $ <[ "#6" := locinfo: loc_68 ; - LocInfoE loc_71 ((LocInfoE loc_72 (global_mem)) at{struct_region} "cur") <-{ it_layout size_t } - LocInfoE loc_73 (use{it_layout size_t} (LocInfoE loc_74 ("ret"))) ; + LocInfoE loc_71 ((LocInfoE loc_72 (global_mem)) at{struct_region} "cur") <-{ it_layout uintptr_t } + LocInfoE loc_73 (use{it_layout uintptr_t} (LocInfoE loc_74 ("ret"))) ; locinfo: loc_69 ; Return (LocInfoE loc_70 (NULL)) ]> $ @@ -295,11 +295,11 @@ Section code. LocInfoE loc_139 ((LocInfoE loc_140 (global_mem)) at{struct_region} "base") <-{ void* } LocInfoE loc_141 (use{void*} (LocInfoE loc_142 ("virt"))) ; locinfo: loc_123 ; - LocInfoE loc_130 ((LocInfoE loc_131 (global_mem)) at{struct_region} "end") <-{ it_layout size_t } - LocInfoE loc_132 (UnOp (CastOp $ IntOp size_t) (IntOp size_t) (LocInfoE loc_133 ((LocInfoE loc_134 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_135 (use{void*} (LocInfoE loc_136 ("virt")))))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_137 (UnOp (CastOp $ IntOp size_t) (IntOp u32) (LocInfoE loc_137 (use{it_layout u32} (LocInfoE loc_138 ("size"))))))))) ; + LocInfoE loc_130 ((LocInfoE loc_131 (global_mem)) at{struct_region} "end") <-{ it_layout uintptr_t } + LocInfoE loc_132 (UnOp (CastOp $ IntOp uintptr_t) (IntOp uintptr_t) (LocInfoE loc_133 ((LocInfoE loc_134 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_135 (use{void*} (LocInfoE loc_136 ("virt")))))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_137 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u32) (LocInfoE loc_137 (use{it_layout u32} (LocInfoE loc_138 ("size"))))))))) ; locinfo: loc_124 ; - LocInfoE loc_125 ((LocInfoE loc_126 (global_mem)) at{struct_region} "cur") <-{ it_layout size_t } - LocInfoE loc_127 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_128 (use{void*} (LocInfoE loc_129 ("virt"))))) ; + LocInfoE loc_125 ((LocInfoE loc_126 (global_mem)) at{struct_region} "cur") <-{ it_layout uintptr_t } + LocInfoE loc_127 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_128 (use{void*} (LocInfoE loc_129 ("virt"))))) ; Return (VOID) ]> $∅ )%E diff --git a/theories/lang/int_type.v b/theories/lang/int_type.v index 2888f4dd..977adcf9 100644 --- a/theories/lang/int_type.v +++ b/theories/lang/int_type.v @@ -55,6 +55,7 @@ Definition uintptr_t := IntType bytes_per_addr_log false. Definition size_t := uintptr_t. Definition ssize_t := intptr_t. +Definition ptrdiff_t := intptr_t. Definition bool_it := u8. (*** Lemmas about [int_type] *) -- GitLab