From d6e96cc1342ab4c855b5fc1b6cd718aec8b61ca3 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Wed, 12 Mar 2025 15:47:05 +0100
Subject: [PATCH] [ir2cabs] stabilize translation of function template
instantiation
---
reorder_defs.ml | 44 ++++++++++++++++-
tests/stl/oracle/stl_algorithm.res.oracle | 4 +-
tests/stl/oracle/stl_iterator.res.oracle | 8 ++--
tests/stl/oracle/stl_unique_ptr.res.oracle | 4 +-
tests/stl/oracle/stl_utility.res.oracle | 48 +++++++++----------
.../oracle/simple_template.res.oracle | 8 ++--
6 files changed, 79 insertions(+), 37 deletions(-)
diff --git a/reorder_defs.ml b/reorder_defs.ml
index 8e168745..34898872 100644
--- a/reorder_defs.ml
+++ b/reorder_defs.ml
@@ -410,6 +410,47 @@ class compute_deps =
end else DoChildren
end
+let extract_def_name =
+ function
+ | _,FUNDEF(_,(_,(n,_,_,_)),_,_,_) -> Some n
+ | _,DECDEF(_,(_,[(n,_,_,_),_]),_) -> Some n
+ | _ -> None (* we only reorder function template definitions *)
+
+let reorder_insts l =
+ let compare d1 d2 =
+ match extract_def_name d1, extract_def_name d2 with
+ | None, _ | _, None -> 0
+ | Some n1, Some n2 -> String.compare n1 n2
+ in
+ List.stable_sort compare l
+
+let same_template d1 d2 =
+ match extract_def_name d1, extract_def_name d2 with
+ | None, _ | _, None -> false
+ | Some n1, Some n2 ->
+ let n1 = Mangling.unmangle n1 in
+ let n2 = Mangling.unmangle n2 in
+ let fct_template_regex=Str.regexp {|\(.*\)<.*>$|} in
+ Str.string_match fct_template_regex n1 0 &&
+ let n1 = Str.matched_group 1 n1 in
+ Str.string_match fct_template_regex n2 0 &&
+ let n2 = Str.matched_group 1 n2 in
+ n1 = n2
+
+let order_template_insts l =
+ let rec aux res curr tl =
+ match curr,tl with
+ | _, [] -> List.rev_append res (reorder_insts curr)
+ | [], _ -> assert false
+ | cd::_, d :: tl ->
+ if same_template cd d then
+ aux res (d::curr) tl
+ else aux (List.rev_append (reorder_insts (List.rev curr)) res) [d] tl
+ in
+ match l with
+ | [] -> []
+ | hd :: tl -> aux [] [hd] tl
+
let reorder file =
ignore (Cabsvisit.visitCabsFile (new compute_deps) file);
if not (Dependencies.is_complete()) then
@@ -418,4 +459,5 @@ let reorder file =
if Dependencies.has_cycle () then
Frama_Clang_option.fatal
"cannot reorder global definitions: dependencies cycle";
- (fst file, Dependencies.emit_deps (snd file))
+ let l = order_template_insts (snd file) in
+ (fst file, Dependencies.emit_deps l)
diff --git a/tests/stl/oracle/stl_algorithm.res.oracle b/tests/stl/oracle/stl_algorithm.res.oracle
index cd0b3f34..5d910338 100644
--- a/tests/stl/oracle/stl_algorithm.res.oracle
+++ b/tests/stl/oracle/stl_algorithm.res.oracle
@@ -279,10 +279,10 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ ensures \valid(\result); */
-type declval<int*&>(void);
+type declval<int*&&>(void);
/*@ ensures \valid(\result); */
-type declval<int*&&>(void);
+type declval<int*&>(void);
/*@ ensures \valid(\result); */
type declval<int*&>(void);
diff --git a/tests/stl/oracle/stl_iterator.res.oracle b/tests/stl/oracle/stl_iterator.res.oracle
index d5c0479f..d89e946f 100644
--- a/tests/stl/oracle/stl_iterator.res.oracle
+++ b/tests/stl/oracle/stl_iterator.res.oracle
@@ -715,6 +715,10 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
+/*@ requires \valid_read(a);
+ ensures \valid_read(\result); */
+int const *get<3,int,4>(struct array<int,4> const *a);
+
/*@ requires \valid(a);
ensures \valid(\result); */
int *get<3,int,4>(struct array<int,4> *a)
@@ -724,10 +728,6 @@ int *get<3,int,4>(struct array<int,4> *a)
return tmp;
}
-/*@ requires \valid_read(a);
- ensures \valid_read(\result); */
-int const *get<3,int,4>(struct array<int,4> const *a);
-
int main(void)
{
int __retres;
diff --git a/tests/stl/oracle/stl_unique_ptr.res.oracle b/tests/stl/oracle/stl_unique_ptr.res.oracle
index 84212433..a113095c 100644
--- a/tests/stl/oracle/stl_unique_ptr.res.oracle
+++ b/tests/stl/oracle/stl_unique_ptr.res.oracle
@@ -757,11 +757,11 @@ struct unique_ptr<PlainOldStruct,std::default_delete<PlainOldStruct>> *forward<s
struct unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>> *forward<std::unique_ptr<ClassTemplate<int,0>,std::default_delete<ClassTemplate<int,0>>>>
(type *t);
-struct default_delete<int[]> *forward<std::default_delete<int[]>>(type *t);
-
struct default_delete<PlainOldStruct> *forward<std::default_delete<PlainOldStruct>>
(type *t);
+struct default_delete<int[]> *forward<std::default_delete<int[]>>(type *t);
+
struct default_delete<ClassTemplate<int,0>> *forward<std::default_delete<ClassTemplate<int,0>>>
(type *t);
diff --git a/tests/stl/oracle/stl_utility.res.oracle b/tests/stl/oracle/stl_utility.res.oracle
index 913743f6..84bf1cd4 100644
--- a/tests/stl/oracle/stl_utility.res.oracle
+++ b/tests/stl/oracle/stl_utility.res.oracle
@@ -190,28 +190,28 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ ensures \valid(\result); */
-type declval<int&&>(void);
+type declval<bool&&>(void);
/*@ ensures \valid(\result); */
-type declval<int&>(void);
+type declval<double&&>(void);
/*@ ensures \valid(\result); */
-type declval<int&>(void);
+type declval<int&&>(void);
/*@ ensures \valid(\result); */
type declval<bool&>(void);
/*@ ensures \valid(\result); */
-type declval<bool&&>(void);
+type declval<double&>(void);
/*@ ensures \valid(\result); */
-type declval<bool&>(void);
+type declval<int&>(void);
/*@ ensures \valid(\result); */
-type declval<double&>(void);
+type declval<bool&>(void);
/*@ ensures \valid(\result); */
-type declval<double&&>(void);
+type declval<int&>(void);
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
{.name = "ok_type",
@@ -626,9 +626,9 @@ _Bool operator><S>(struct S const *x, struct S const *y);
/*@ requires \valid(b);
requires \valid(a); */
-void swap<int>(int *a, int *b)
+void swap<double>(double *a, double *b)
{
- int tmp = *a;
+ double tmp = *a;
*a = *b;
*b = tmp;
return;
@@ -636,9 +636,9 @@ void swap<int>(int *a, int *b)
/*@ requires \valid(b);
requires \valid(a); */
-void swap<double>(double *a, double *b)
+void swap<int>(int *a, int *b)
{
- double tmp = *a;
+ int tmp = *a;
*a = *b;
*b = tmp;
return;
@@ -658,21 +658,21 @@ void swap<int,2>(int (*a)[2], int (*b)[2])
/*@ requires \valid(t);
ensures \valid(\result); */
-int *forward<int>(type *t)
+int *forward<int&>(type *t)
{
return t;
}
/*@ requires \valid(t);
ensures \valid(\result); */
-int *forward<int&>(type *t)
+_Bool *forward<bool>(type *t)
{
return t;
}
/*@ requires \valid(t);
ensures \valid(\result); */
-_Bool *forward<bool>(type *t)
+int *forward<int>(type *t)
{
return t;
}
@@ -686,14 +686,14 @@ int *forward<int>(type *t)
/*@ requires \valid(t);
ensures \valid(\result); */
-type *move<int>(int *t)
+type *move<int&>(int *t)
{
return t;
}
/*@ requires \valid(t);
ensures \valid(\result); */
-type *move<int&>(int *t)
+type *move<int>(int *t)
{
return t;
}
@@ -931,6 +931,10 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
.base_classes = (struct _frama_c_rtti_name_info_content *)0,
.number_of_base_classes = 0,
.pvmt = (struct _frama_c_vmt *)0};
+/*@ requires \valid_read(p);
+ ensures \valid_read(\result); */
+type const *get<0,int,double>(struct pair<int,double> const *p);
+
/*@ requires \valid(p);
ensures \valid(\result); */
type *get<0,int,double>(struct pair<int,double> *p)
@@ -940,6 +944,10 @@ type *get<0,int,double>(struct pair<int,double> *p)
return tmp;
}
+/*@ requires \valid_read(p);
+ ensures \valid_read(\result); */
+type const *get<1,int,double>(struct pair<int,double> const *p);
+
/*@ requires \valid(p);
ensures \valid(\result); */
type *get<1,int,double>(struct pair<int,double> *p)
@@ -949,14 +957,6 @@ type *get<1,int,double>(struct pair<int,double> *p)
return tmp;
}
-/*@ requires \valid_read(p);
- ensures \valid_read(\result); */
-type const *get<0,int,double>(struct pair<int,double> const *p);
-
-/*@ requires \valid_read(p);
- ensures \valid_read(\result); */
-type const *get<1,int,double>(struct pair<int,double> const *p);
-
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
/*@ requires \valid_read(this); */
diff --git a/tests/template/oracle/simple_template.res.oracle b/tests/template/oracle/simple_template.res.oracle
index ece5e5d3..22877445 100644
--- a/tests/template/oracle/simple_template.res.oracle
+++ b/tests/template/oracle/simple_template.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing simple_template.cc (external front-end)
/* Generated by Frama-C */
-int f<int>(int *x)
+_Bool f<bool>(_Bool *x)
{
- int __retres;
+ _Bool __retres;
__retres = *x;
return __retres;
}
-_Bool f<bool>(_Bool *x)
+int f<int>(int *x)
{
- _Bool __retres;
+ int __retres;
__retres = *x;
return __retres;
}
--
GitLab