From 50ea35fceb52c5f66ccbc4f709df3a3471b12647 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 19 Mar 2019 19:28:03 +0100 Subject: added helper functions but strange idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration --- cfrontend/C2C.ml | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index d70c4dad..f928a5d3 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -294,7 +294,23 @@ let builtins_generic = { "__compcert_i64_umulh", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], - false) + false); + "__compcert_i32_sdiv", + (TInt(IInt, []), + [TInt(IInt, []); TInt(IInt, [])], + false); + "__compcert_i32_udiv", + (TInt(IUInt, []), + [TInt(IUInt, []); TInt(IUInt, [])], + false); + "__compcert_i32_smod", + (TInt(IInt, []), + [TInt(IInt, []); TInt(IInt, [])], + false); + "__compcert_i32_umod", + (TInt(IUInt, []), + [TInt(IUInt, []); TInt(IUInt, [])], + false); ] } -- cgit From c86388b548984dae5f8dd794cad1f4b4505d4307 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 10:38:23 +0100 Subject: ça semble passer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- cfrontend/C2C.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f928a5d3..f0ae4367 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -1214,7 +1214,7 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i64_" +let re_runtime = Str.regexp "__compcert_i" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1227,7 +1227,9 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else - if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) else + if Str.string_match re_runtime id.name 0 + then AST.EF_runtime(id'', sg) + else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.Builtins.functions then AST.EF_builtin(id'', sg) -- cgit From 2638a022276c932ed00dc3f64b0e58bc0114a3d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 12:55:03 +0100 Subject: la division flottante fonctionne --- cfrontend/C2C.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index f0ae4367..bd9b7487 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -311,6 +311,14 @@ let builtins_generic = { (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); + "__compcert_f32_div", + (TFloat(FFloat,[]), + [TFloat(FFloat,[]); TFloat(FFloat,[])], + false); + "__compcert_f64_div", + (TFloat(FDouble,[]), + [TFloat(FDouble,[]); TFloat(FDouble,[])], + false); ] } @@ -1214,7 +1222,10 @@ let convertFundef loc env fd = (** External function declaration *) let re_builtin = Str.regexp "__builtin_" -let re_runtime = Str.regexp "__compcert_i" +let re_runtime64 = Str.regexp "__compcert_i64" +let re_runtime32 = Str.regexp "__compcert_i32" +let re_runtimef32 = Str.regexp "__compcert_f32" +let re_runtimef64 = Str.regexp "__compcert_f64" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = @@ -1227,7 +1238,10 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else - if Str.string_match re_runtime id.name 0 + if Str.string_match re_runtime64 id.name 0 + || Str.string_match re_runtime32 id.name 0 + || Str.string_match re_runtimef64 id.name 0 + || Str.string_match re_runtimef32 id.name 0 then AST.EF_runtime(id'', sg) else if Str.string_match re_builtin id.name 0 -- cgit From 2dca62f38463b0ebce24fff50666c846df50488e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 20:19:24 +0200 Subject: attempts at generating builtins, start --- cfrontend/C2C.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd9b7487..1ab38a2b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -154,6 +154,10 @@ let ais_annot_functions = else [] +let builtin_ternary suffix typ = + ("__builtin_ternary_" ^ suffix), + (typ, [TInt(IInt, []); typ; typ], false);; + let builtins_generic = { Builtins.typedefs = []; Builtins.functions = @@ -180,7 +184,10 @@ let builtins_generic = { TPtr(TVoid [AConst], []); TInt(IULong, []); TInt(IULong, [])], - false); + false); + (* Ternary operator *) + builtin_ternary "uint" (TInt(IUInt, [])); + (* Annotations *) "__builtin_annot", (TVoid [], -- cgit From 4032ed3192424a23dbb0a4f3bd2a539b22625168 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 21:00:46 +0200 Subject: problem in ValueAOp --- cfrontend/C2C.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1ab38a2b..c17ce75a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -187,6 +187,7 @@ let builtins_generic = { false); (* Ternary operator *) builtin_ternary "uint" (TInt(IUInt, [])); + builtin_ternary "ulong" (TInt(IULong, [])); (* Annotations *) "__builtin_annot", -- cgit From ca34ea47f863c074a9d0ca890097786c5829267c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Apr 2019 22:36:22 +0200 Subject: ternary ops for float/double --- cfrontend/C2C.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'cfrontend/C2C.ml') diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index c17ce75a..0f2e3674 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -188,6 +188,10 @@ let builtins_generic = { (* Ternary operator *) builtin_ternary "uint" (TInt(IUInt, [])); builtin_ternary "ulong" (TInt(IULong, [])); + builtin_ternary "int" (TInt(IInt, [])); + builtin_ternary "long" (TInt(ILong, [])); + builtin_ternary "double" (TFloat(FDouble, [])); + builtin_ternary "float" (TFloat(FFloat, [])); (* Annotations *) "__builtin_annot", -- cgit