Skip to content

GitLab

Commit 2b922cb0 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Preserve different C types in the frontend.

parent 2c7772a9
Pipeline #47036 passed with stage
in 31 minutes and 14 seconds
Hide whitespace changes
Inline Side-by-side
examples/proofs/intptr/generated_code.v
View file @ 2b922cb0
......@@ -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
|}.
......
frontend/ail_to_coq.ml
View file @ 2b922cb0
......@@ -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
......
frontend/coq_ast.ml
View file @ 2b922cb0
......@@ -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 =
......
frontend/coq_pp.ml
View file @ 2b922cb0
......@@ -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"
......
linux/casestudies/proofs/page_alloc/generated_code.v
View file @ 2b922cb0
......@@ -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
|}.
......
linux/pkvm/proofs/early_alloc/generated_code.v
View file @ 2b922cb0
......@@ -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
......
theories/lang/int_type.v
View file @ 2b922cb0
......@@ -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] *)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment