On Tue, Dec 1, 2015 at 5:17 PM, Greg Stark <st...@mit.edu> wrote:
> Sorry, I didn't look at it since. At the time I was using Xi Wang's software
> to find the overflow checks that need to be redone. He published a paper on
> it and it's actually pretty impressive. It constructs a constraint problem
> and then throws a kSAT solver at it to find out if there's any code that a
> compiler could optimize away regardless of whether any existant compiler is
> actually capable of detecting the case and optimizing it away.
> https://pdos.csail.mit.edu/papers/stack:sosp13.pdf
I did get this code running again (it was quite a hassle actually).
Attached is the report.
I'm leaning towards using the builtin functions described here
http://clang.llvm.org/docs/LanguageExtensions.html#checked-arithmetic-builtins
https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html
They aren't in older GCC and clang and probably won't be in icc and
the like but we could probably implement replacements. The downside is
that then we wouldn't be able to use the generic one and would have to
use the type-specific ones which would be annoying. The Linux kernel
folk wrote wrappers that don't have that problem but they depend on
type_min() and type_max() which I've never heard of and have no idea
what support they have?
What version of GCC and other compilers did we decide we're targeting now?
--
greg
---
bug: anti-simplify
model: |
%cmp48 = icmp ne i8* %30, null, !dbg !1018
--> true
stack:
- /home/stark/src/pg/postgresql-master/src/backend/storage/lmgr/lmgr.c:712:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/storage/lmgr/lmgr.c:713:0
- null pointer dereference
---
bug: anti-algebra
model: |
%cmp = icmp ult i8* %add.ptr1, %start_address, !dbg !500
--> %16 = icmp slt i64 %15, 0, !dbg !500
************************************************************
(4 + (8 * (sext i32 %7 to i64)) + %start_address) <u %start_address
--> (4 + (8 * (sext i32 %7 to i64))) <s 0
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/time/combocid.c:326:0
ncore: 2
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/time/combocid.c:324:0
- pointer overflow
- /home/stark/src/pg/postgresql-master/src/backend/utils/time/combocid.c:324:0
- pointer overflow
---
bug: anti-simplify
model: |
%cmp3 = icmp slt i32 %add, 0, !dbg !595
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int.c:756:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int.c:754:0
- signed addition overflow
---
bug: anti-algebra
model: |
%cmp2 = icmp slt i32 %add1, %s, !dbg !570
--> %6 = icmp slt i32 %l, 0, !dbg !570
************************************************************
(%s + %l) <s %s
--> %l <s 0
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varbit.c:1063:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varbit.c:1057:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp5 = icmp sle i32 %add, %sl, !dbg !568
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varbit.c:1170:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varbit.c:1169:0
- signed addition overflow
---
bug: anti-algebra
model: |
%cmp3 = icmp slt i32 %add, %start, !dbg !878
--> %2 = icmp slt i32 %length, 0, !dbg !878
************************************************************
(%start + %length) <s %start
--> %length <s 0
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:834:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:828:0
- signed addition overflow
---
bug: anti-algebra
model: |
%cmp31 = icmp slt i32 %add30, %start, !dbg !907
--> %29 = icmp slt i32 %length, 0, !dbg !907
************************************************************
(%start + %length) <s %start
--> %length <s 0
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:898:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:892:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp5 = icmp sle i32 %add, %sl, !dbg !876
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:1047:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:1046:0
- signed addition overflow
---
bug: anti-algebra
model: |
%cmp1 = icmp slt i32 %add, %S, !dbg !875
--> %2 = icmp slt i32 %L, 0, !dbg !875
************************************************************
(%S + %L) <s %S
--> %L <s 0
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:2594:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:2588:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp5 = icmp sle i32 %add, %sl, !dbg !877
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:2666:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/varlena.c:2665:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp19 = icmp slt i64 %mul, 0, !dbg !583
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int8.c:576:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int8.c:561:0
- signed multiplication overflow
---
bug: anti-simplify
model: |
%cmp2 = icmp sgt i64 %1, 0, !dbg !580
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int8.c:711:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int8.c:709:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp2 = icmp slt i64 %1, 0, !dbg !580
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int8.c:755:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/int8.c:753:0
- signed subtraction overflow
---
bug: anti-dce
model: |
%cmp36 = icmp eq i64 %val.1, 0, !dbg !964
--> true
************************************************************
lor.lhs.false38:
%cmp39 = icmp slt i64 %val.0, 0, !dbg !964
br i1 %cmp39, label %if.then41, label %if.end42, !dbg !964
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/numeric.c:5233:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/numeric.c:5233:0
- signed subtraction overflow
---
bug: anti-simplify
model: |
%cmp61 = icmp sle i32 %add58, %mul57, !dbg !542
--> false
stack:
-
/home/stark/src/pg/postgresql-master/src/backend/utils/adt/oracle_compat.c:1056:0
ncore: 1
core:
-
/home/stark/src/pg/postgresql-master/src/backend/utils/adt/oracle_compat.c:1054:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp6 = icmp slt i32 %add5, %sub, !dbg !539
--> false
stack:
-
/home/stark/src/pg/postgresql-master/src/backend/utils/adt/array_userfuncs.c:117:0
ncore: 1
core:
-
/home/stark/src/pg/postgresql-master/src/backend/utils/adt/array_userfuncs.c:114:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp59 = icmp sgt i64 %sub52, 0, !dbg !878
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/datetime.c:1557:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/datetime.c:1556:0
- signed subtraction overflow
---
bug: anti-simplify
model: |
%cmp79 = icmp sgt i64 %sub72, 0, !dbg !882
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/datetime.c:1563:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/datetime.c:1562:0
- signed subtraction overflow
---
bug: anti-simplify
model: |
%cmp105 = icmp slt i32 %add, %conv, !dbg !680
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/float.c:2768:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/float.c:2766:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp136 = icmp slt i32 %add135, %conv, !dbg !700
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/float.c:2784:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/utils/adt/float.c:2782:0
- signed addition overflow
---
bug: anti-dce
model: |
entry:
%call = call i32 @p_isalnum(%struct.TParser* null), !dbg !1025
%call.i = call i32 @p_isalnum(%struct.TParser* null) #7, !dbg !1026
%call2 = call i32 @p_isalpha(%struct.TParser* null), !dbg !1028
%call.i1 = call i32 @p_isalpha(%struct.TParser* null) #7, !dbg !1029
%call4 = call i32 @p_isdigit(%struct.TParser* null), !dbg !1031
%call.i5 = call i32 @p_isdigit(%struct.TParser* null) #7, !dbg !1032, !macro
!1034
%call6 = call fastcc i32 @p_islower(%struct.TParser* null), !dbg !1035
%call.i9 = call fastcc i32 @p_islower(%struct.TParser* null) #7, !dbg !1036,
!macro !1034
%call8 = call fastcc i32 @p_isprint(%struct.TParser* null), !dbg !1038
%call.i13 = call fastcc i32 @p_isprint(%struct.TParser* null) #7, !dbg !1039,
!macro !1034
%call10 = call fastcc i32 @p_ispunct(%struct.TParser* null), !dbg !1041
%call.i17 = call fastcc i32 @p_ispunct(%struct.TParser* null) #7, !dbg !1042,
!macro !1034
%call12 = call i32 @p_isspace(%struct.TParser* null), !dbg !1044
%call.i21 = call i32 @p_isspace(%struct.TParser* null) #7, !dbg !1045, !macro
!1034
%call14 = call fastcc i32 @p_isupper(%struct.TParser* null), !dbg !1047
%call.i25 = call fastcc i32 @p_isupper(%struct.TParser* null) #7, !dbg !1048,
!macro !1034
%call16 = call i32 @p_isxdigit(%struct.TParser* null), !dbg !1050
%call.i29 = call i32 @p_isxdigit(%struct.TParser* null) #7, !dbg !1051,
!macro !1034
call void @opt.bugon(i1 true), !dbg !1053, !bug !1057
call void @opt.bugon(i1 true), !dbg !1053, !bug !1058
%0 = load %struct.TParserPosition** getelementptr (%struct.TParser* null, i32
0, i32 6), align 8, !dbg !1053, !macro !1059
%tobool.i33 = icmp ne %struct.TParserPosition* %0, null, !dbg !1053, !macro
!1059
br i1 %tobool.i33, label %if.end.i, label %if.then.i, !dbg !1053, !macro !1059
stack:
- /home/stark/src/pg/postgresql-master/src/backend/tsearch/wparser_def.c:639:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/tsearch/wparser_def.c:576:0
- buffer overflow
---
bug: anti-simplify
model: |
%cmp33 = icmp sgt i32 %add, 0, !dbg !755
--> true
stack:
- /home/stark/src/pg/postgresql-master/src/backend/tsearch/spell.c:1634:0
ncore: 2
core:
- /home/stark/src/pg/postgresql-master/src/backend/tsearch/spell.c:1624:0
- signed subtraction overflow
- /home/stark/src/pg/postgresql-master/src/backend/tsearch/spell.c:1624:0
- signed addition overflow
---
bug: anti-dce
model: |
%cmp44 = icmp slt i64 %add, %17, !dbg !1346
--> false
************************************************************
if.then46:
%posOverflow = getelementptr inbounds %struct.PortalData* %portal, i32 0, i32
23, !dbg !1348
%20 = icmp eq %struct.PortalData* %portal, null
call void @opt.bugon(i1 %20), !dbg !1348, !bug !1308
store i8 1, i8* %posOverflow, align 1, !dbg !1348
br label %if.end47, !dbg !1348
stack:
- /home/stark/src/pg/postgresql-master/src/backend/tcop/pquery.c:960:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/tcop/pquery.c:957:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp114 = icmp sgt i64 %sub, %39, !dbg !1393
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/tcop/pquery.c:1010:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/tcop/pquery.c:1009:0
- signed subtraction overflow
---
bug: anti-simplify
model: |
%cmp72 = icmp sle i32 %add, 0, !dbg !2117
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/executor/execQual.c:3188:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/executor/execQual.c:3187:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp12 = icmp sle i32 %add, 0, !dbg !824
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/backend/regex/./regc_locale.c:438:0
ncore: 2
core:
- /home/stark/src/pg/postgresql-master/src/backend/regex/./regc_locale.c:437:0
- signed subtraction overflow
- /home/stark/src/pg/postgresql-master/src/backend/regex/./regc_locale.c:437:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp29 = icmp ne i8* %cond, null, !dbg !1083
--> true
stack:
- /home/stark/src/pg/postgresql-master/src/backend/access/gist/gist.c:1007:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/backend/access/gist/gist.c:1004:0
- null pointer dereference
---
bug: anti-simplify
model: |
%tobool36 = icmp ne %struct.List* %rollup_lists.addr.0, null, !dbg !2266
--> true
stack:
-
/home/stark/src/pg/postgresql-master/src/backend/optimizer/plan/planner.c:2548:0
ncore: 1
core:
-
/home/stark/src/pg/postgresql-master/src/backend/optimizer/plan/planner.c:2507:20
- null pointer dereference
---
bug: anti-simplify
model: |
%cmp129 = icmp sgt i32 %sub, %loop_value.0, !dbg !2917
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/pl/plpgsql/src/pl_exec.c:2071:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/pl/plpgsql/src/pl_exec.c:2071:0
- signed subtraction overflow
---
bug: anti-simplify
model: |
%cmp135 = icmp slt i32 %add, %loop_value.0, !dbg !2924
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/pl/plpgsql/src/pl_exec.c:2077:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/pl/plpgsql/src/pl_exec.c:2077:0
- signed addition overflow
---
bug: anti-simplify
model: |
%tobool97 = icmp ne i32 %conv4.i, 0, !dbg !236
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/bin/initdb/localtime.c:1202:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/bin/initdb/localtime.c:1290:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp3 = icmp ne i32 %conv, %conv2, !dbg !197
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/bin/initdb/localtime.c:1291:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/bin/initdb/localtime.c:1290:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp556 = icmp slt i64 %sub555, 0, !dbg !825
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/bin/pgbench/pgbench.c:1533:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/bin/pgbench/pgbench.c:1533:0
- signed subtraction overflow
---
bug: anti-simplify
model: |
%cmp561 = icmp slt i64 %add560, 0, !dbg !825
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/bin/pgbench/pgbench.c:1533:0
ncore: 2
core:
- /home/stark/src/pg/postgresql-master/src/bin/pgbench/pgbench.c:1533:0
- signed subtraction overflow
- /home/stark/src/pg/postgresql-master/src/bin/pgbench/pgbench.c:1533:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp9 = icmp sle i64 %add, %t1, !dbg !402
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2674:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2673:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp12 = icmp sge i64 %add, %t1, !dbg !402
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2674:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2673:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp1 = icmp sle i64 %add, %t1, !dbg !396
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2656:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2655:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp4 = icmp sge i64 %add, %t1, !dbg !396
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2656:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/timezone/zic.c:2655:0
- signed addition overflow
---
bug: anti-simplify
model: |
%tobool97 = icmp ne i32 %conv4.i, 0, !dbg !236
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/timezone/localtime.c:1202:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/timezone/localtime.c:1290:0
- signed addition overflow
---
bug: anti-simplify
model: |
%cmp3 = icmp ne i32 %conv, %conv2, !dbg !197
--> false
stack:
- /home/stark/src/pg/postgresql-master/src/timezone/localtime.c:1291:0
ncore: 1
core:
- /home/stark/src/pg/postgresql-master/src/timezone/localtime.c:1290:0
- signed addition overflow
--
Sent via pgsql-hackers mailing list (pgsql-hackers@postgresql.org)
To make changes to your subscription:
http://www.postgresql.org/mailpref/pgsql-hackers
