From 63b7fab72c428df7c357e1cc47b8fd073d62eec8 Mon Sep 17 00:00:00 2001 From: dzaima Date: Wed, 26 Mar 2025 04:10:59 +0200 Subject: [PATCH] better w+x & w-x overflow checks --- src/singeli/src/dyarith.singeli | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/singeli/src/dyarith.singeli b/src/singeli/src/dyarith.singeli index 1f605803..4020a559 100644 --- a/src/singeli/src/dyarith.singeli +++ b/src/singeli/src/dyarith.singeli @@ -18,10 +18,12 @@ def bqn_or{a, b} = (a+b)-(a*b) # + & - -def arithChk1{(__add), M, w:T, x:T, r:T} = tup{'any_top', M{(w^r) & (x^r)}} -def arithChk1{(__sub), M, w:T, x:T, r:T} = tup{'any_top', M{(w^x) & (w^r)}} -def arithChk1{(__add), M, w:T=[_]E, x:T, r:T if not hasarch{'X86_64'} or width{E}<=16} = tup{'anyne', adds{w,x}, r} -def arithChk1{(__sub), M, w:T=[_]E, x:T, r:T if not hasarch{'X86_64'} or width{E}<=16} = tup{'anyne', subs{w,x}, r} +# def arithChk1{(__add), M, w:T, x:T, r:T} = tup{'any_top', M{(w^r) & (x^r)}} +# def arithChk1{(__sub), M, w:T, x:T, r:T} = tup{'any_top', M{(w^x) & (w^r)}} +def arithChk1{(__add), M, w:T=[_]E, x:T, r:T} = tup{'anyne', adds{w,x}, r} +def arithChk1{(__sub), M, w:T=[_]E, x:T, r:T} = tup{'anyne', subs{w,x}, r} +def arithChk1{(__add), M, w:T, x:T, r:T if hasarch{'X86_64'}} = tup{'any_top', M{ty_s{w>r} ^ x}} +def arithChk1{(__sub), M, w:T, x:T, r:T if hasarch{'X86_64'}} = tup{'any_top', M{ty_s{x>w} ^ r}}