diff --git a/dartagnan/src/main/antlr4/LitmusAArch64.g4 b/dartagnan/src/main/antlr4/LitmusAArch64.g4 index edcd35c03b..233215fb1d 100644 --- a/dartagnan/src/main/antlr4/LitmusAArch64.g4 +++ b/dartagnan/src/main/antlr4/LitmusAArch64.g4 @@ -151,30 +151,30 @@ storeExclusiveInstruction locals [String mo] | STLXR {$mo = MO_REL;} ; -arithmeticInstruction locals [IOpBin op] - : ADD { $op = IOpBin.ADD; } +arithmeticInstruction locals [IntBinaryOp op] + : ADD { $op = IntBinaryOp.ADD; } // | ADDS { throw new RuntimeException("Instruction ADDS is not implemented"); } - | SUB { $op = IOpBin.SUB; } + | SUB { $op = IntBinaryOp.SUB; } // | SUBS { throw new RuntimeException("Instruction SUBS is not implemented"); } // | ADC { throw new RuntimeException("Instruction ADC is not implemented"); } // | ADCS { throw new RuntimeException("Instruction ADCS is not implemented"); } // | SBC { throw new RuntimeException("Instruction SBC is not implemented"); } // | SBCS { throw new RuntimeException("Instruction SBCS is not implemented"); } - | AND { $op = IOpBin.AND; } - | ORR { $op = IOpBin.OR; } - | EOR { $op = IOpBin.XOR; } + | AND { $op = IntBinaryOp.AND; } + | ORR { $op = IntBinaryOp.OR; } + | EOR { $op = IntBinaryOp.XOR; } // | BIC { throw new RuntimeException("Instruction BIC is not implemented"); } // | ORN { throw new RuntimeException("Instruction ORN is not implemented"); } // | EON { throw new RuntimeException("Instruction EON is not implemented"); } ; -branchCondition returns [COpBin op] - : EQ {$op = COpBin.EQ;} - | NE {$op = COpBin.NEQ;} - | GE {$op = COpBin.GTE;} - | LE {$op = COpBin.LTE;} - | GT {$op = COpBin.GT;} - | LT {$op = COpBin.LT;} +branchCondition returns [CmpOp op] + : EQ {$op = CmpOp.EQ;} + | NE {$op = CmpOp.NEQ;} + | GE {$op = CmpOp.GTE;} + | LE {$op = CmpOp.LTE;} + | GT {$op = CmpOp.GT;} + | LT {$op = CmpOp.LT;} // | CS // | HS // | CC @@ -188,15 +188,15 @@ branchCondition returns [COpBin op] // | AL ; -branchRegInstruction returns [COpBin op] - : CBZ {$op = COpBin.EQ;} - | CBNZ {$op = COpBin.NEQ;} +branchRegInstruction returns [CmpOp op] + : CBZ {$op = CmpOp.EQ;} + | CBNZ {$op = CmpOp.NEQ;} ; -shiftOperator returns [IOpBin op] - : LSL { $op = IOpBin.LSHIFT; } - | LSR { $op = IOpBin.RSHIFT; } - | ASR { $op = IOpBin.ARSHIFT; } +shiftOperator returns [IntBinaryOp op] + : LSL { $op = IntBinaryOp.LSHIFT; } + | LSR { $op = IntBinaryOp.RSHIFT; } + | ASR { $op = IntBinaryOp.ARSHIFT; } ; expr64 diff --git a/dartagnan/src/main/antlr4/LitmusAssertions.g4 b/dartagnan/src/main/antlr4/LitmusAssertions.g4 index 61b79fb7b5..490858f978 100644 --- a/dartagnan/src/main/antlr4/LitmusAssertions.g4 +++ b/dartagnan/src/main/antlr4/LitmusAssertions.g4 @@ -3,7 +3,7 @@ grammar LitmusAssertions; import BaseLexer; @header{ -import com.dat3m.dartagnan.expression.op.COpBin; +import com.dat3m.dartagnan.expression.op.CmpOp; } assertionFilter @@ -48,13 +48,13 @@ assertionListExpectation : AssertionListExpectationTest Colon AssertionNot? AssertionExists Semi ; -assertionCompare returns [COpBin op] - : (Equals | EqualsEquals) {$op = COpBin.EQ;} - | NotEquals {$op = COpBin.NEQ;} - | GreaterEquals {$op = COpBin.GTE;} - | LessEquals {$op = COpBin.LTE;} - | Less {$op = COpBin.LT;} - | Greater {$op = COpBin.GT;} +assertionCompare returns [CmpOp op] + : (Equals | EqualsEquals) {$op = CmpOp.EQ;} + | NotEquals {$op = CmpOp.NEQ;} + | GreaterEquals {$op = CmpOp.GTE;} + | LessEquals {$op = CmpOp.LTE;} + | Less {$op = CmpOp.LT;} + | Greater {$op = CmpOp.GT;} ; threadId returns [int id] diff --git a/dartagnan/src/main/antlr4/LitmusC.g4 b/dartagnan/src/main/antlr4/LitmusC.g4 index aea0f45e2a..f31b05ba8e 100644 --- a/dartagnan/src/main/antlr4/LitmusC.g4 +++ b/dartagnan/src/main/antlr4/LitmusC.g4 @@ -56,46 +56,46 @@ whileExpression | While LPar re RPar LBrace expression* RBrace ; -re locals [IOpBin op, String mo] - : ( AtomicAddReturn LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_MB;} - | AtomicAddReturnRelaxed LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELAXED;} - | AtomicAddReturnAcquire LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_ACQUIRE;} - | AtomicAddReturnRelease LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELEASE;} - | AtomicSubReturn LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_MB;} - | AtomicSubReturnRelaxed LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELAXED;} - | AtomicSubReturnAcquire LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_ACQUIRE;} - | AtomicSubReturnRelease LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELEASE;} - | AtomicIncReturn LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_MB;} - | AtomicIncReturnRelaxed LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELAXED;} - | AtomicIncReturnAcquire LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_ACQUIRE;} - | AtomicIncReturnRelease LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELEASE;} - | AtomicDecReturn LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_MB;} - | AtomicDecReturnRelaxed LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELAXED;} - | AtomicDecReturnAcquire LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_ACQUIRE;} - | AtomicDecReturnRelease LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELEASE;}) # reAtomicOpReturn +re locals [IntBinaryOp op, String mo] + : ( AtomicAddReturn LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_MB;} + | AtomicAddReturnRelaxed LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELAXED;} + | AtomicAddReturnAcquire LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_ACQUIRE;} + | AtomicAddReturnRelease LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELEASE;} + | AtomicSubReturn LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_MB;} + | AtomicSubReturnRelaxed LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELAXED;} + | AtomicSubReturnAcquire LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_ACQUIRE;} + | AtomicSubReturnRelease LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELEASE;} + | AtomicIncReturn LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_MB;} + | AtomicIncReturnRelaxed LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELAXED;} + | AtomicIncReturnAcquire LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_ACQUIRE;} + | AtomicIncReturnRelease LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELEASE;} + | AtomicDecReturn LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_MB;} + | AtomicDecReturnRelaxed LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELAXED;} + | AtomicDecReturnAcquire LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_ACQUIRE;} + | AtomicDecReturnRelease LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELEASE;}) # reAtomicOpReturn - | ( C11AtomicAdd LPar address = re Comma value = re Comma c11Mo RPar {$op = IOpBin.ADD;} - | C11AtomicSub LPar address = re Comma value = re Comma c11Mo RPar {$op = IOpBin.SUB;} - | C11AtomicOr LPar address = re Comma value = re Comma c11Mo RPar {$op = IOpBin.OR;} - | C11AtomicXor LPar address = re Comma value = re Comma c11Mo RPar {$op = IOpBin.XOR;} - | C11AtomicAnd LPar address = re Comma value = re Comma c11Mo RPar {$op = IOpBin.AND;}) # C11AtomicOp - - | ( AtomicFetchAdd LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_MB;} - | AtomicFetchAddRelaxed LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELAXED;} - | AtomicFetchAddAcquire LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_ACQUIRE;} - | AtomicFetchAddRelease LPar value = re Comma address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELEASE;} - | AtomicFetchSub LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_MB;} - | AtomicFetchSubRelaxed LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELAXED;} - | AtomicFetchSubAcquire LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_ACQUIRE;} - | AtomicFetchSubRelease LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELEASE;} - | AtomicFetchInc LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_MB;} - | AtomicFetchIncRelaxed LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELAXED;} - | AtomicFetchIncAcquire LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_ACQUIRE;} - | AtomicFetchIncRelease LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_RELEASE;} - | AtomicFetchDec LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_MB;} - | AtomicFetchDecRelaxed LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELAXED;} - | AtomicFetchDecAcquire LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_ACQUIRE;} - | AtomicFetchDecRelease LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_RELEASE;}) # reAtomicFetchOp + | ( C11AtomicAdd LPar address = re Comma value = re Comma c11Mo RPar {$op = IntBinaryOp.ADD;} + | C11AtomicSub LPar address = re Comma value = re Comma c11Mo RPar {$op = IntBinaryOp.SUB;} + | C11AtomicOr LPar address = re Comma value = re Comma c11Mo RPar {$op = IntBinaryOp.OR;} + | C11AtomicXor LPar address = re Comma value = re Comma c11Mo RPar {$op = IntBinaryOp.XOR;} + | C11AtomicAnd LPar address = re Comma value = re Comma c11Mo RPar {$op = IntBinaryOp.AND;}) # C11AtomicOp + + | ( AtomicFetchAdd LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_MB;} + | AtomicFetchAddRelaxed LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELAXED;} + | AtomicFetchAddAcquire LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_ACQUIRE;} + | AtomicFetchAddRelease LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELEASE;} + | AtomicFetchSub LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_MB;} + | AtomicFetchSubRelaxed LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELAXED;} + | AtomicFetchSubAcquire LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_ACQUIRE;} + | AtomicFetchSubRelease LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELEASE;} + | AtomicFetchInc LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_MB;} + | AtomicFetchIncRelaxed LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELAXED;} + | AtomicFetchIncAcquire LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_ACQUIRE;} + | AtomicFetchIncRelease LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_RELEASE;} + | AtomicFetchDec LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_MB;} + | AtomicFetchDecRelaxed LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELAXED;} + | AtomicFetchDecAcquire LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_ACQUIRE;} + | AtomicFetchDecRelease LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_RELEASE;}) # reAtomicFetchOp | ( AtomicXchg LPar address = re Comma value = re RPar {$mo = Linux.MO_MB;} | AtomicXchgRelaxed LPar address = re Comma value = re RPar {$mo = Linux.MO_RELAXED;} @@ -120,9 +120,9 @@ re locals [IOpBin op, String mo] | CmpXchgAcquire LPar address = re Comma cmp = re Comma value = re RPar {$mo = Linux.MO_ACQUIRE;} | CmpXchgRelease LPar address = re Comma cmp = re Comma value = re RPar {$mo = Linux.MO_RELEASE;}) # reCmpXchg - | ( AtomicSubAndTest LPar value = re Comma address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_MB;} - | AtomicIncAndTest LPar address = re RPar {$op = IOpBin.ADD; $mo = Linux.MO_MB;} - | AtomicDecAndTest LPar address = re RPar {$op = IOpBin.SUB; $mo = Linux.MO_MB;}) # reAtomicOpAndTest + | ( AtomicSubAndTest LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_MB;} + | AtomicIncAndTest LPar address = re RPar {$op = IntBinaryOp.ADD; $mo = Linux.MO_MB;} + | AtomicDecAndTest LPar address = re RPar {$op = IntBinaryOp.SUB; $mo = Linux.MO_MB;}) # reAtomicOpAndTest | AtomicAddUnless LPar address = re Comma value = re Comma cmp = re RPar # reAtomicAddUnless @@ -153,11 +153,11 @@ re locals [IOpBin op, String mo] | constant # reConst ; -nre locals [IOpBin op, String mo, String name] - : ( AtomicAdd LPar value = re Comma address = re RPar {$op = IOpBin.ADD;} - | AtomicSub LPar value = re Comma address = re RPar {$op = IOpBin.SUB;} - | AtomicInc LPar address = re RPar {$op = IOpBin.ADD;} - | AtomicDec LPar address = re RPar {$op = IOpBin.SUB;}) # nreAtomicOp +nre locals [IntBinaryOp op, String mo, String name] + : ( AtomicAdd LPar value = re Comma address = re RPar {$op = IntBinaryOp.ADD;} + | AtomicSub LPar value = re Comma address = re RPar {$op = IntBinaryOp.SUB;} + | AtomicInc LPar address = re RPar {$op = IntBinaryOp.ADD;} + | AtomicDec LPar address = re RPar {$op = IntBinaryOp.SUB;}) # nreAtomicOp | ( AtomicSet LPar address = re Comma value = re RPar {$mo = Linux.MO_ONCE;} | AtomicSetRelease LPar address = re Comma value = re RPar {$mo = Linux.MO_RELEASE;} @@ -205,26 +205,26 @@ boolConst returns [Boolean value] | False {$value = false;} ; -opBool returns [BOpBin op] - : AmpAmp {$op = BOpBin.AND;} - | BarBar {$op = BOpBin.OR;} +opBool returns [BoolBinaryOp op] + : AmpAmp {$op = BoolBinaryOp.AND;} + | BarBar {$op = BoolBinaryOp.OR;} ; -opCompare returns [COpBin op] - : EqualsEquals {$op = COpBin.EQ;} - | NotEquals {$op = COpBin.NEQ;} - | LessEquals {$op = COpBin.LTE;} - | GreaterEquals {$op = COpBin.GTE;} - | Less {$op = COpBin.LT;} - | Greater {$op = COpBin.GT;} +opCompare returns [CmpOp op] + : EqualsEquals {$op = CmpOp.EQ;} + | NotEquals {$op = CmpOp.NEQ;} + | LessEquals {$op = CmpOp.LTE;} + | GreaterEquals {$op = CmpOp.GTE;} + | Less {$op = CmpOp.LT;} + | Greater {$op = CmpOp.GT;} ; -opArith returns [IOpBin op] - : Plus {$op = IOpBin.ADD;} - | Minus {$op = IOpBin.SUB;} - | Amp {$op = IOpBin.AND;} - | Bar {$op = IOpBin.OR;} - | Circ {$op = IOpBin.XOR;} +opArith returns [IntBinaryOp op] + : Plus {$op = IntBinaryOp.ADD;} + | Minus {$op = IntBinaryOp.SUB;} + | Amp {$op = IntBinaryOp.AND;} + | Bar {$op = IntBinaryOp.OR;} + | Circ {$op = IntBinaryOp.XOR;} ; c11Mo returns [String mo] diff --git a/dartagnan/src/main/antlr4/LitmusPPC.g4 b/dartagnan/src/main/antlr4/LitmusPPC.g4 index 0bc013e306..28dd84ef96 100644 --- a/dartagnan/src/main/antlr4/LitmusPPC.g4 +++ b/dartagnan/src/main/antlr4/LitmusPPC.g4 @@ -134,13 +134,13 @@ offset : DigitSequence ; -cond returns [COpBin op] - : Beq {$op = COpBin.EQ;} - | Bne {$op = COpBin.NEQ;} - | Bge {$op = COpBin.GTE;} - | Ble {$op = COpBin.LTE;} - | Bgt {$op = COpBin.GT;} - | Blt {$op = COpBin.LT;} +cond returns [CmpOp op] + : Beq {$op = CmpOp.EQ;} + | Bne {$op = CmpOp.NEQ;} + | Bge {$op = CmpOp.GTE;} + | Ble {$op = CmpOp.LTE;} + | Bgt {$op = CmpOp.GT;} + | Blt {$op = CmpOp.LT;} ; assertionValue diff --git a/dartagnan/src/main/antlr4/LitmusPTX.g4 b/dartagnan/src/main/antlr4/LitmusPTX.g4 index 43b86f3b23..446831f551 100644 --- a/dartagnan/src/main/antlr4/LitmusPTX.g4 +++ b/dartagnan/src/main/antlr4/LitmusPTX.g4 @@ -207,23 +207,23 @@ register : Register ; -operation locals [IOpBin op] - : Add {$op = IOpBin.ADD;} - | Sub {$op = IOpBin.SUB;} - | Mul {$op = IOpBin.MUL;} - | Div {$op = IOpBin.DIV;} - | And {$op = IOpBin.AND;} - | Or {$op = IOpBin.OR;} - | Xor {$op = IOpBin.XOR;} - ; - -cond returns [COpBin op] - : Beq {$op = COpBin.EQ;} - | Bne {$op = COpBin.NEQ;} - | Bge {$op = COpBin.GTE;} - | Ble {$op = COpBin.LTE;} - | Bgt {$op = COpBin.GT;} - | Blt {$op = COpBin.LT;} +operation locals [IntBinaryOp op] + : Add {$op = IntBinaryOp.ADD;} + | Sub {$op = IntBinaryOp.SUB;} + | Mul {$op = IntBinaryOp.MUL;} + | Div {$op = IntBinaryOp.DIV;} + | And {$op = IntBinaryOp.AND;} + | Or {$op = IntBinaryOp.OR;} + | Xor {$op = IntBinaryOp.XOR;} + ; + +cond returns [CmpOp op] + : Beq {$op = CmpOp.EQ;} + | Bne {$op = CmpOp.NEQ;} + | Bge {$op = CmpOp.GTE;} + | Ble {$op = CmpOp.LTE;} + | Bgt {$op = CmpOp.GT;} + | Blt {$op = CmpOp.LT;} ; assertionValue diff --git a/dartagnan/src/main/antlr4/LitmusRISCV.g4 b/dartagnan/src/main/antlr4/LitmusRISCV.g4 index a009112e08..3a40d12925 100644 --- a/dartagnan/src/main/antlr4/LitmusRISCV.g4 +++ b/dartagnan/src/main/antlr4/LitmusRISCV.g4 @@ -192,13 +192,13 @@ offset : DigitSequence ; -cond returns [COpBin op] - : Beq {$op = COpBin.EQ;} - | Bne {$op = COpBin.NEQ;} - | Bge {$op = COpBin.GTE;} - | Ble {$op = COpBin.LTE;} - | Bgt {$op = COpBin.GT;} - | Blt {$op = COpBin.LT;} +cond returns [CmpOp op] + : Beq {$op = CmpOp.EQ;} + | Bne {$op = CmpOp.NEQ;} + | Bge {$op = CmpOp.GTE;} + | Ble {$op = CmpOp.LTE;} + | Bgt {$op = CmpOp.GT;} + | Blt {$op = CmpOp.LT;} ; assertionValue diff --git a/dartagnan/src/main/antlr4/LitmusVulkan.g4 b/dartagnan/src/main/antlr4/LitmusVulkan.g4 index d1a8b585c1..01c5003354 100644 --- a/dartagnan/src/main/antlr4/LitmusVulkan.g4 +++ b/dartagnan/src/main/antlr4/LitmusVulkan.g4 @@ -253,23 +253,23 @@ avvisSemanticList : (avvisSemantic)* ; -operation locals [IOpBin op] - : Period Add {$op = IOpBin.ADD;} - | Period Sub {$op = IOpBin.SUB;} - | Period Mul {$op = IOpBin.MUL;} - | Period Div {$op = IOpBin.DIV;} - | Period And {$op = IOpBin.AND;} - | Period Or {$op = IOpBin.OR;} - | Period Xor {$op = IOpBin.XOR;} - ; - -cond returns [COpBin op] - : Beq {$op = COpBin.EQ;} - | Bne {$op = COpBin.NEQ;} - | Bge {$op = COpBin.GTE;} - | Ble {$op = COpBin.LTE;} - | Bgt {$op = COpBin.GT;} - | Blt {$op = COpBin.LT;} +operation locals [IntBinaryOp op] + : Period Add {$op = IntBinaryOp.ADD;} + | Period Sub {$op = IntBinaryOp.SUB;} + | Period Mul {$op = IntBinaryOp.MUL;} + | Period Div {$op = IntBinaryOp.DIV;} + | Period And {$op = IntBinaryOp.AND;} + | Period Or {$op = IntBinaryOp.OR;} + | Period Xor {$op = IntBinaryOp.XOR;} + ; + +cond returns [CmpOp op] + : Beq {$op = CmpOp.EQ;} + | Bne {$op = CmpOp.NEQ;} + | Bge {$op = CmpOp.GTE;} + | Ble {$op = CmpOp.LTE;} + | Bgt {$op = CmpOp.GT;} + | Blt {$op = CmpOp.LT;} ; Locations diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java index b76feda76c..d00f3dd831 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/EncodingContext.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.encoding; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.COpBin; +import com.dat3m.dartagnan.expression.op.CmpOp; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; @@ -135,13 +135,13 @@ public Formula encodeExpressionAt(Expression expression, Event event) { return new ExpressionEncoder(this, event).encode(expression); } - public BooleanFormula encodeComparison(COpBin op, Formula lhs, Formula rhs) { + public BooleanFormula encodeComparison(CmpOp op, Formula lhs, Formula rhs) { if (lhs instanceof BooleanFormula l && rhs instanceof BooleanFormula r) { return switch (op) { case EQ -> booleanFormulaManager.equivalence(l, r); case NEQ -> booleanFormulaManager.not(booleanFormulaManager.equivalence(l, r)); default -> throw new UnsupportedOperationException( - String.format("Encoding of COpBin operation %s not supported on boolean formulas.", op)); + String.format("Encoding of CmpOp operation %s not supported on boolean formulas.", op)); }; } if (lhs instanceof IntegerFormula l && rhs instanceof IntegerFormula r) { @@ -160,13 +160,13 @@ public BooleanFormula encodeComparison(COpBin op, Formula lhs, Formula rhs) { return switch (op) { case EQ -> bitvectorFormulaManager.equal(l, r); case NEQ -> booleanFormulaManager.not(bitvectorFormulaManager.equal(l, r)); - case LT, ULT -> bitvectorFormulaManager.lessThan(l, r, op.equals(COpBin.LT)); - case LTE, ULTE -> bitvectorFormulaManager.lessOrEquals(l, r, op.equals(COpBin.LTE)); - case GT, UGT -> bitvectorFormulaManager.greaterThan(l, r, op.equals(COpBin.GT)); - case GTE, UGTE -> bitvectorFormulaManager.greaterOrEquals(l, r, op.equals(COpBin.GTE)); + case LT, ULT -> bitvectorFormulaManager.lessThan(l, r, op.equals(CmpOp.LT)); + case LTE, ULTE -> bitvectorFormulaManager.lessOrEquals(l, r, op.equals(CmpOp.LTE)); + case GT, UGT -> bitvectorFormulaManager.greaterThan(l, r, op.equals(CmpOp.GT)); + case GTE, UGTE -> bitvectorFormulaManager.greaterOrEquals(l, r, op.equals(CmpOp.GTE)); }; } - throw new UnsupportedOperationException("Encoding not supported for COpBin: " + lhs + " " + op + " " + rhs); + throw new UnsupportedOperationException("Encoding not supported for CmpOp: " + lhs + " " + op + " " + rhs); } public BooleanFormula controlFlow(Event event) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java index a817612802..a95a5b60b2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ExpressionEncoder.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.encoding; import com.dat3m.dartagnan.expression.*; -import com.dat3m.dartagnan.expression.op.IOpUn; +import com.dat3m.dartagnan.expression.op.IntUnaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.Type; import com.dat3m.dartagnan.program.Register; @@ -68,12 +68,12 @@ public Formula visit(Atom atom) { } @Override - public Formula visit(BConst bConst) { - return booleanFormulaManager.makeBoolean(bConst.getValue()); + public Formula visit(BoolLiteral boolLiteral) { + return booleanFormulaManager.makeBoolean(boolLiteral.getValue()); } @Override - public Formula visit(BExprBin bBin) { + public Formula visit(BoolBinaryExpr bBin) { BooleanFormula lhs = encodeAsBoolean(bBin.getLHS()); BooleanFormula rhs = encodeAsBoolean(bBin.getRHS()); switch (bBin.getOp()) { @@ -82,30 +82,30 @@ public Formula visit(BExprBin bBin) { case OR: return booleanFormulaManager.or(lhs, rhs); } - throw new UnsupportedOperationException("Encoding not supported for BOpBin " + bBin.getOp()); + throw new UnsupportedOperationException("Encoding not supported for BoolBinaryOp " + bBin.getOp()); } @Override - public Formula visit(BExprUn bUn) { + public Formula visit(BoolUnaryExpr bUn) { BooleanFormula inner = encodeAsBoolean(bUn.getInner()); return booleanFormulaManager.not(inner); } @Override - public Formula visit(BNonDet bNonDet) { - return booleanFormulaManager.makeVariable(Integer.toString(bNonDet.hashCode())); + public Formula visit(NonDetBool nonDetBool) { + return booleanFormulaManager.makeVariable(Integer.toString(nonDetBool.hashCode())); } @Override - public Formula visit(IValue iValue) { + public Formula visit(IntLiteral intLiteral) { - BigInteger value = iValue.getValue(); - Type type = iValue.getType(); + BigInteger value = intLiteral.getValue(); + Type type = intLiteral.getType(); return context.makeLiteral(type, value); } @Override - public Formula visit(IExprBin iBin) { + public Formula visit(IntBinaryExpr iBin) { Formula lhs = encode(iBin.getLHS()); Formula rhs = encode(iBin.getRHS()); if (lhs instanceof IntegerFormula i1 && rhs instanceof IntegerFormula i2) { @@ -176,7 +176,7 @@ public Formula visit(IExprBin iBin) { integerFormulaManager.lessThan(i1, zero)); return booleanFormulaManager.ifThenElse(cond, integerFormulaManager.subtract(modulo, i2), modulo); default: - throw new UnsupportedOperationException("Encoding of IOpBin operation " + iBin.getOp() + " not supported on integer formulas."); + throw new UnsupportedOperationException("Encoding of IntBinaryOp operation " + iBin.getOp() + " not supported on integer formulas."); } } else if (lhs instanceof BitvectorFormula bv1 && rhs instanceof BitvectorFormula bv2) { BitvectorFormulaManager bitvectorFormulaManager = bitvectorFormulaManager(); @@ -218,15 +218,15 @@ public Formula visit(IExprBin iBin) { case ARSHIFT: return bitvectorFormulaManager.shiftRight(bv1, bv2, true); default: - throw new UnsupportedOperationException("Encoding of IOpBin operation " + iBin.getOp() + " not supported on bitvector formulas."); + throw new UnsupportedOperationException("Encoding of IntBinaryOp operation " + iBin.getOp() + " not supported on bitvector formulas."); } } else { - throw new UnsupportedOperationException("Encoding of IOpBin operation " + iBin.getOp() + " not supported on formulas of mismatching type."); + throw new UnsupportedOperationException("Encoding of IntBinaryOp operation " + iBin.getOp() + " not supported on formulas of mismatching type."); } } @Override - public Formula visit(IExprUn iUn) { + public Formula visit(IntUnaryExpr iUn) { Formula inner = encode(iUn.getInner()); switch (iUn.getOp()) { case MINUS -> { @@ -238,7 +238,7 @@ public Formula visit(IExprUn iUn) { } } case CAST_SIGNED, CAST_UNSIGNED -> { - boolean signed = iUn.getOp().equals(IOpUn.CAST_SIGNED); + boolean signed = iUn.getOp().equals(IntUnaryOp.CAST_SIGNED); if (inner instanceof BooleanFormula bool) { return bool; } @@ -284,15 +284,15 @@ public Formula visit(IExprUn iUn) { } @Override - public Formula visit(IfExpr ifExpr) { - BooleanFormula guard = encodeAsBoolean(ifExpr.getGuard()); - Formula tBranch = encode(ifExpr.getTrueBranch()); - Formula fBranch = encode(ifExpr.getFalseBranch()); + public Formula visit(ITEExpr iteExpr) { + BooleanFormula guard = encodeAsBoolean(iteExpr.getGuard()); + Formula tBranch = encode(iteExpr.getTrueBranch()); + Formula fBranch = encode(iteExpr.getFalseBranch()); return booleanFormulaManager.ifThenElse(guard, tBranch, fBranch); } @Override - public Formula visit(INonDet iNonDet) { + public Formula visit(NonDetInt iNonDet) { String name = iNonDet.getName(); Type type = iNonDet.getType(); return context.makeVariable(name, type); @@ -308,10 +308,8 @@ public Formula visit(Register reg) { } @Override - public Formula visit(MemoryObject address) { - BigInteger value = address.getValue(); - Type type = address.getType(); - return context.makeLiteral(type, value); + public Formula visit(MemoryObject memObj) { + return context.makeLiteral(memObj.getType(), memObj.getAddress()); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java index 5fe707af7c..c610776628 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProgramEncoder.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.encoding; -import com.dat3m.dartagnan.expression.INonDet; +import com.dat3m.dartagnan.expression.NonDetInt; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.Thread; @@ -78,7 +78,7 @@ public BooleanFormula encodeFullProgram() { public BooleanFormula encodeConstants() { List enc = new ArrayList<>(); - for (INonDet constant : context.getTask().getProgram().getConstants()) { + for (NonDetInt constant : context.getTask().getProgram().getConstants()) { Formula formula = context.encodeFinalExpression(constant); if (formula instanceof BitvectorFormula bitvector) { boolean signed = constant.isSigned(); @@ -156,7 +156,7 @@ public BooleanFormula encodeMemory() { // For all objects, their 'final' value fetched here represents their constant value. final var addrExprs = new ArrayList(); for (final MemoryObject object : memory.getObjects()) { - final BigInteger addressInteger = object.getValue(); + final BigInteger addressInteger = object.getAddress(); final Formula addressVariable = context.encodeFinalExpression(object); if (addressVariable instanceof BitvectorFormula bitvectorVariable) { final BitvectorFormulaManager bvmgr = fmgr.getBitvectorFormulaManager(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Atom.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Atom.java index fa50af3bae..6212cc970e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Atom.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Atom.java @@ -1,64 +1,64 @@ package com.dat3m.dartagnan.expression; -import com.dat3m.dartagnan.expression.op.COpBin; +import com.dat3m.dartagnan.expression.op.CmpOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.program.Register; import com.google.common.collect.ImmutableSet; -public class Atom extends BExpr { - - private final Expression lhs; - private final Expression rhs; - private final COpBin op; - - public Atom(BooleanType type, Expression lhs, COpBin op, Expression rhs) { - super(type); - this.lhs = lhs; - this.rhs = rhs; - this.op = op; - } +public class Atom extends BoolExpr { - @Override - public ImmutableSet getRegs() { - return new ImmutableSet.Builder().addAll(lhs.getRegs()).addAll(rhs.getRegs()).build(); - } + private final Expression lhs; + private final Expression rhs; + private final CmpOp op; + + Atom(BooleanType type, Expression lhs, CmpOp op, Expression rhs) { + super(type); + this.lhs = lhs; + this.rhs = rhs; + this.op = op; + } + + @Override + public ImmutableSet getRegs() { + return new ImmutableSet.Builder().addAll(lhs.getRegs()).addAll(rhs.getRegs()).build(); + } @Override public String toString() { return lhs + " " + op + " " + rhs; } - public COpBin getOp() { - return op; + public CmpOp getOp() { + return op; } - + public Expression getLHS() { - return lhs; + return lhs; } - + public Expression getRHS() { - return rhs; + return rhs; } - @Override - public T accept(ExpressionVisitor visitor) { - return visitor.visit(this); - } + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visit(this); + } - @Override - public int hashCode() { - return op.hashCode() * lhs.hashCode() + rhs.hashCode(); - } + @Override + public int hashCode() { + return op.hashCode() * lhs.hashCode() + rhs.hashCode(); + } - @Override - public boolean equals(Object obj) { - if (obj == this) { - return true; - } else if (obj == null || obj.getClass() != getClass()) { - return false; - } - Atom expr = (Atom) obj; - return expr.op == op && expr.lhs.equals(lhs) && expr.rhs.equals(rhs); - } + @Override + public boolean equals(Object obj) { + if (obj == this) { + return true; + } else if (obj == null || obj.getClass() != getClass()) { + return false; + } + Atom expr = (Atom) obj; + return expr.op == op && expr.lhs.equals(lhs) && expr.rhs.equals(rhs); + } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BConst.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BConst.java deleted file mode 100644 index dd77f7d404..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BConst.java +++ /dev/null @@ -1,43 +0,0 @@ -package com.dat3m.dartagnan.expression; - -import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; -import com.dat3m.dartagnan.expression.type.BooleanType; - -public class BConst extends BExpr { - - private final boolean value; - - public BConst(BooleanType type, boolean value) { - super(type); - this.value = value; - } - - @Override - public String toString() { - return value ? "True" : "False"; - } - - public boolean getValue() { - return value; - } - - @Override - public T accept(ExpressionVisitor visitor) { - return visitor.visit(this); - } - - @Override - public int hashCode() { - return Boolean.hashCode(value); - } - - @Override - public boolean equals(Object obj) { - if (obj == this) { - return true; - } else if (obj == null || obj.getClass() != getClass()) { - return false; - } - return ((BConst)obj).value == value; - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BNonDet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BNonDet.java deleted file mode 100644 index 5f8e7b9950..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BNonDet.java +++ /dev/null @@ -1,22 +0,0 @@ -package com.dat3m.dartagnan.expression; - -import com.dat3m.dartagnan.expression.type.BooleanType; -import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; - -//TODO instances of this class should be managed by the program -public class BNonDet extends BExpr { - - public BNonDet(BooleanType type) { - super(type); - } - - @Override - public String toString() { - return "nondet_bool()"; - } - - @Override - public T accept(ExpressionVisitor visitor) { - return visitor.visit(this); - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExprBin.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolBinaryExpr.java similarity index 81% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExprBin.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolBinaryExpr.java index 12f4316db6..e2cc94bb06 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExprBin.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolBinaryExpr.java @@ -1,18 +1,18 @@ package com.dat3m.dartagnan.expression; -import com.dat3m.dartagnan.expression.op.BOpBin; +import com.dat3m.dartagnan.expression.op.BoolBinaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.program.Register; import com.google.common.collect.ImmutableSet; -public class BExprBin extends BExpr { +public class BoolBinaryExpr extends BoolExpr { private final Expression b1; private final Expression b2; - private final BOpBin op; + private final BoolBinaryOp op; - public BExprBin(BooleanType type, Expression b1, BOpBin op, Expression b2) { + BoolBinaryExpr(BooleanType type, Expression b1, BoolBinaryOp op, Expression b2) { super(type); this.b1 = b1; this.b2 = b2; @@ -27,7 +27,7 @@ public Expression getRHS() { return b2; } - public BOpBin getOp() { + public BoolBinaryOp getOp() { return op; } @@ -58,7 +58,7 @@ public boolean equals(Object obj) { } else if (obj == null || obj.getClass() != getClass()) { return false; } - BExprBin expr = (BExprBin) obj; + BoolBinaryExpr expr = (BoolBinaryExpr) obj; return expr.op == op && expr.b1.equals(b1) && expr.b2.equals(b2); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolExpr.java similarity index 76% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExpr.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolExpr.java index 7ca7458a21..4c4d4a9707 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExpr.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolExpr.java @@ -4,11 +4,11 @@ import static com.google.common.base.Preconditions.checkNotNull; -public abstract class BExpr implements Expression { +public abstract class BoolExpr implements Expression { private final BooleanType type; - protected BExpr(BooleanType type) { + protected BoolExpr(BooleanType type) { this.type = checkNotNull(type); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolLiteral.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolLiteral.java new file mode 100644 index 0000000000..77ce5d9148 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolLiteral.java @@ -0,0 +1,43 @@ +package com.dat3m.dartagnan.expression; + +import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; +import com.dat3m.dartagnan.expression.type.BooleanType; + +public final class BoolLiteral extends BoolExpr { + + private final boolean value; + + BoolLiteral(BooleanType type, boolean value) { + super(type); + this.value = value; + } + + @Override + public String toString() { + return value ? "True" : "False"; + } + + public boolean getValue() { + return value; + } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visit(this); + } + + @Override + public int hashCode() { + return Boolean.hashCode(value); + } + + @Override + public boolean equals(Object obj) { + if (obj == this) { + return true; + } else if (obj == null || obj.getClass() != getClass()) { + return false; + } + return ((BoolLiteral) obj).value == value; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExprUn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolUnaryExpr.java similarity index 79% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExprUn.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolUnaryExpr.java index fdb9357da1..2d998aaacf 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BExprUn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/BoolUnaryExpr.java @@ -1,23 +1,23 @@ package com.dat3m.dartagnan.expression; -import com.dat3m.dartagnan.expression.op.BOpUn; +import com.dat3m.dartagnan.expression.op.BoolUnaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.program.Register; import com.google.common.collect.ImmutableSet; -public class BExprUn extends BExpr { +public class BoolUnaryExpr extends BoolExpr { private final Expression b; - private final BOpUn op; + private final BoolUnaryOp op; - public BExprUn(BooleanType type, BOpUn op, Expression b) { + BoolUnaryExpr(BooleanType type, BoolUnaryOp op, Expression b) { super(type); this.b = b; this.op = op; } - public BOpUn getOp() { + public BoolUnaryOp getOp() { return op; } @@ -52,7 +52,7 @@ public boolean equals(Object obj) { } else if (obj == null || obj.getClass() != getClass()) { return false; } - BExprUn expr = (BExprUn) obj; + BoolUnaryExpr expr = (BoolUnaryExpr) obj; return expr.op == op && expr.b.equals(b); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java index 213da3d5f0..82e064f9e3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/Expression.java @@ -15,7 +15,7 @@ default ImmutableSet getRegs() { T accept(ExpressionVisitor visitor); - default IConst reduce() { + default IntLiteral reduce() { throw new UnsupportedOperationException("Reduce not supported for " + this); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java index 2dd8b39bbc..f693fd80ce 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ExpressionFactory.java @@ -14,8 +14,8 @@ public final class ExpressionFactory { private final TypeFactory types = TypeFactory.getInstance(); private final BooleanType booleanType = types.getBooleanType(); - private final BConst falseConstant = new BConst(booleanType, false); - private final BConst trueConstant = new BConst(booleanType, true); + private final BoolLiteral falseConstant = new BoolLiteral(booleanType, false); + private final BoolLiteral trueConstant = new BoolLiteral(booleanType, true); private ExpressionFactory() {} @@ -26,36 +26,36 @@ public static ExpressionFactory getInstance() { // ----------------------------------------------------------------------------------------------------------------- // Boolean - public BConst makeTrue() { + public BoolLiteral makeTrue() { return trueConstant; } - public BConst makeFalse() { + public BoolLiteral makeFalse() { return falseConstant; } - public BConst makeValue(boolean value) { + public BoolLiteral makeValue(boolean value) { return value ? makeTrue() : makeFalse(); } public Expression makeNot(Expression operand) { - return makeUnary(BOpUn.NOT, operand); + return makeUnary(BoolUnaryOp.NOT, operand); } - public Expression makeUnary(BOpUn operator, Expression operand) { - return new BExprUn(types.getBooleanType(), operator, operand); + public Expression makeUnary(BoolUnaryOp operator, Expression operand) { + return new BoolUnaryExpr(types.getBooleanType(), operator, operand); } public Expression makeAnd(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, BOpBin.AND, rightOperand); + return makeBinary(leftOperand, BoolBinaryOp.AND, rightOperand); } public Expression makeOr(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, BOpBin.OR, rightOperand); + return makeBinary(leftOperand, BoolBinaryOp.OR, rightOperand); } - public Expression makeBinary(Expression leftOperand, BOpBin operator, Expression rightOperand) { - return new BExprBin(booleanType, leftOperand, operator, rightOperand); + public Expression makeBinary(Expression leftOperand, BoolBinaryOp operator, Expression rightOperand) { + return new BoolBinaryExpr(booleanType, leftOperand, operator, rightOperand); } public Expression makeGeneralZero(Type type) { @@ -81,24 +81,24 @@ public Expression makeGeneralZero(Type type) { } } - public IValue makeZero(IntegerType type) { + public IntLiteral makeZero(IntegerType type) { return makeValue(BigInteger.ZERO, type); } - public IValue makeOne(IntegerType type) { + public IntLiteral makeOne(IntegerType type) { return makeValue(BigInteger.ONE, type); } - public IValue parseValue(String text, IntegerType type) { + public IntLiteral parseValue(String text, IntegerType type) { return makeValue(new BigInteger(text), type); } - public IValue makeValue(long value, IntegerType type) { + public IntLiteral makeValue(long value, IntegerType type) { return makeValue(BigInteger.valueOf(value), type); } - public IValue makeValue(BigInteger value, IntegerType type) { - return new IValue(value, type); + public IntLiteral makeValue(BigInteger value, IntegerType type) { + return new IntLiteral(value, type); } public Expression makeCast(Expression expression, Type type, boolean signed) { @@ -115,8 +115,8 @@ public Expression makeCast(Expression expression, Type type) { return makeCast(expression, type, false); } - public Expression makeConditional(Expression condition, Expression ifTrue, Expression ifFalse) { - return new IfExpr(condition, ifTrue, ifFalse); + public Expression makeITE(Expression condition, Expression ifTrue, Expression ifFalse) { + return new ITEExpr(condition, ifTrue, ifFalse); } public Expression makeBooleanCast(Expression operand) { @@ -130,102 +130,102 @@ public Expression makeBooleanCast(Expression operand) { } public Expression makeEQ(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, COpBin.EQ, rightOperand); + return makeBinary(leftOperand, CmpOp.EQ, rightOperand); } public Expression makeNEQ(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, COpBin.NEQ, rightOperand); + return makeBinary(leftOperand, CmpOp.NEQ, rightOperand); } public Expression makeLT(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? COpBin.LT : COpBin.ULT, rightOperand); + return makeBinary(leftOperand, signed ? CmpOp.LT : CmpOp.ULT, rightOperand); } public Expression makeGT(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? COpBin.GT : COpBin.UGT, rightOperand); + return makeBinary(leftOperand, signed ? CmpOp.GT : CmpOp.UGT, rightOperand); } public Expression makeLTE(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? COpBin.LTE : COpBin.ULTE, rightOperand); + return makeBinary(leftOperand, signed ? CmpOp.LTE : CmpOp.ULTE, rightOperand); } public Expression makeGTE(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? COpBin.GTE : COpBin.UGTE, rightOperand); + return makeBinary(leftOperand, signed ? CmpOp.GTE : CmpOp.UGTE, rightOperand); } - public Expression makeBinary(Expression leftOperand, COpBin operator, Expression rightOperand) { + public Expression makeBinary(Expression leftOperand, CmpOp operator, Expression rightOperand) { return new Atom(types.getBooleanType(), leftOperand, operator, rightOperand); } public Expression makeNEG(Expression operand, IntegerType targetType) { - return makeUnary(IOpUn.MINUS, operand, targetType); + return makeUnary(IntUnaryOp.MINUS, operand, targetType); } public Expression makeCTLZ(Expression operand, IntegerType targetType) { - return makeUnary(IOpUn.CTLZ, operand, targetType); + return makeUnary(IntUnaryOp.CTLZ, operand, targetType); } public Expression makeIntegerCast(Expression operand, IntegerType targetType, boolean signed) { if (operand.getType() instanceof BooleanType) { - return makeConditional(operand, makeOne(targetType), makeZero(targetType)); + return makeITE(operand, makeOne(targetType), makeZero(targetType)); } - return makeUnary(signed ? IOpUn.CAST_SIGNED : IOpUn.CAST_UNSIGNED, operand, targetType); + return makeUnary(signed ? IntUnaryOp.CAST_SIGNED : IntUnaryOp.CAST_UNSIGNED, operand, targetType); } - public Expression makeUnary(IOpUn operator, Expression operand, IntegerType targetType) { + public Expression makeUnary(IntUnaryOp operator, Expression operand, IntegerType targetType) { Preconditions.checkArgument(operand.getType() instanceof IntegerType, "Non-integer operand for %s %s.", operator, operand); - return new IExprUn(operator, operand, targetType); + return new IntUnaryExpr(operator, operand, targetType); } public Expression makeADD(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.ADD, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.ADD, rightOperand); } public Expression makeSUB(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.SUB, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.SUB, rightOperand); } public Expression makeMUL(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.MUL, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.MUL, rightOperand); } public Expression makeDIV(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? IOpBin.DIV : IOpBin.UDIV, rightOperand); + return makeBinary(leftOperand, signed ? IntBinaryOp.DIV : IntBinaryOp.UDIV, rightOperand); } public Expression makeMOD(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.MOD, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.MOD, rightOperand); } public Expression makeREM(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? IOpBin.SREM : IOpBin.UREM, rightOperand); + return makeBinary(leftOperand, signed ? IntBinaryOp.SREM : IntBinaryOp.UREM, rightOperand); } public Expression makeAND(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.AND, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.AND, rightOperand); } public Expression makeOR(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.OR, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.OR, rightOperand); } public Expression makeXOR(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.XOR, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.XOR, rightOperand); } public Expression makeLSH(Expression leftOperand, Expression rightOperand) { - return makeBinary(leftOperand, IOpBin.LSHIFT, rightOperand); + return makeBinary(leftOperand, IntBinaryOp.LSHIFT, rightOperand); } public Expression makeRSH(Expression leftOperand, Expression rightOperand, boolean signed) { - return makeBinary(leftOperand, signed ? IOpBin.ARSHIFT : IOpBin.RSHIFT, rightOperand); + return makeBinary(leftOperand, signed ? IntBinaryOp.ARSHIFT : IntBinaryOp.RSHIFT, rightOperand); } - public Expression makeBinary(Expression leftOperand, IOpBin operator, Expression rightOperand) { + public Expression makeBinary(Expression leftOperand, IntBinaryOp operator, Expression rightOperand) { Preconditions.checkState(leftOperand.getType() instanceof IntegerType, "Non-integer left operand %s %s %s.", leftOperand, operator, rightOperand); - return new IExprBin((IntegerType) leftOperand.getType(), leftOperand, operator, rightOperand); + return new IntBinaryExpr((IntegerType) leftOperand.getType(), leftOperand, operator, rightOperand); } // ----------------------------------------------------------------------------------------------------------------- diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IConst.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IConst.java deleted file mode 100644 index 686d4d6cf4..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IConst.java +++ /dev/null @@ -1,31 +0,0 @@ -package com.dat3m.dartagnan.expression; - -import com.dat3m.dartagnan.expression.type.IntegerType; - -import java.math.BigInteger; - -/** - * Expressions whose results are known before an execution starts. - */ -public abstract class IConst extends IExpr { - - protected IConst(IntegerType type) { - super(type); - } - - /** - * @return - * The concrete result that all valid executions agree with. - */ - public abstract BigInteger getValue(); - - public int getValueAsInt() { - return getValue().intValue(); - } - - - @Override - public IConst reduce() { - return this; - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExpr.java deleted file mode 100644 index cf9e9f483c..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExpr.java +++ /dev/null @@ -1,19 +0,0 @@ -package com.dat3m.dartagnan.expression; - -import com.dat3m.dartagnan.expression.type.IntegerType; - -import static com.google.common.base.Preconditions.checkNotNull; - -public abstract class IExpr implements Expression { - - private final IntegerType type; - - protected IExpr(IntegerType type) { - this.type = checkNotNull(type); - } - - @Override - public final IntegerType getType() { - return type; - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ITEExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ITEExpr.java new file mode 100644 index 0000000000..5c5e22230d --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/ITEExpr.java @@ -0,0 +1,76 @@ +package com.dat3m.dartagnan.expression; + +import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; +import com.dat3m.dartagnan.expression.type.BooleanType; +import com.dat3m.dartagnan.expression.type.IntegerType; +import com.dat3m.dartagnan.program.Register; +import com.google.common.collect.ImmutableSet; + +import static com.google.common.base.Preconditions.checkArgument; + +public class ITEExpr extends IntExpr { + + private final Expression guard; + private final Expression tbranch; + private final Expression fbranch; + + ITEExpr(Expression guard, Expression tbranch, Expression fbranch) { + super(checkIntegerType(tbranch)); + checkArgument(guard.getType() instanceof BooleanType, "IfThenElse with non-boolean guard %s.", guard); + checkArgument(tbranch.getType().equals(fbranch.getType()), + "IfThenElse with mismatching branches %s and %s.", tbranch, fbranch); + this.guard = guard; + this.tbranch = tbranch; + this.fbranch = fbranch; + } + + private static IntegerType checkIntegerType(Expression tbranch) { + if (tbranch.getType() instanceof IntegerType integerType) { + return integerType; + } + throw new IllegalArgumentException(String.format("IfThenElse with non-integer branch %s.", tbranch)); + } + + @Override + public ImmutableSet getRegs() { + return new ImmutableSet.Builder().addAll(guard.getRegs()).addAll(tbranch.getRegs()).addAll(fbranch.getRegs()).build(); + } + + @Override + public String toString() { + return "(if " + guard + " then " + tbranch + " else " + fbranch + ")"; + } + + public Expression getGuard() { + return guard; + } + + public Expression getTrueBranch() { + return tbranch; + } + + public Expression getFalseBranch() { + return fbranch; + } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visit(this); + } + + @Override + public int hashCode() { + return guard.hashCode() ^ tbranch.hashCode() + fbranch.hashCode(); + } + + @Override + public boolean equals(Object obj) { + if (obj == this) { + return true; + } else if (obj == null || obj.getClass() != getClass()) { + return false; + } + ITEExpr expr = (ITEExpr) obj; + return expr.guard.equals(guard) && expr.fbranch.equals(fbranch) && expr.tbranch.equals(tbranch); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IfExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IfExpr.java deleted file mode 100644 index 95963cb3f1..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IfExpr.java +++ /dev/null @@ -1,76 +0,0 @@ -package com.dat3m.dartagnan.expression; - -import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; -import com.dat3m.dartagnan.expression.type.BooleanType; -import com.dat3m.dartagnan.expression.type.IntegerType; -import com.dat3m.dartagnan.program.Register; -import com.google.common.collect.ImmutableSet; - -import static com.google.common.base.Preconditions.checkArgument; - -public class IfExpr extends IExpr { - - private final Expression guard; - private final Expression tbranch; - private final Expression fbranch; - - public IfExpr(Expression guard, Expression tbranch, Expression fbranch) { - super(checkIntegerType(tbranch)); - checkArgument(guard.getType() instanceof BooleanType, "IfThenElse with non-boolean guard %s.", guard); - checkArgument(tbranch.getType().equals(fbranch.getType()), - "IfThenElse with mismatching branches %s and %s.", tbranch, fbranch); - this.guard = guard; - this.tbranch = tbranch; - this.fbranch = fbranch; - } - - private static IntegerType checkIntegerType(Expression tbranch) { - if (tbranch.getType() instanceof IntegerType integerType) { - return integerType; - } - throw new IllegalArgumentException(String.format("IfThenElse with non-integer branch %s.", tbranch)); - } - - @Override - public ImmutableSet getRegs() { - return new ImmutableSet.Builder().addAll(guard.getRegs()).addAll(tbranch.getRegs()).addAll(fbranch.getRegs()).build(); - } - - @Override - public String toString() { - return "(if " + guard + " then " + tbranch + " else " + fbranch + ")"; - } - - public Expression getGuard() { - return guard; - } - - public Expression getTrueBranch() { - return tbranch; - } - - public Expression getFalseBranch() { - return fbranch; - } - - @Override - public T accept(ExpressionVisitor visitor) { - return visitor.visit(this); - } - - @Override - public int hashCode() { - return guard.hashCode() ^ tbranch.hashCode() + fbranch.hashCode(); - } - - @Override - public boolean equals(Object obj) { - if (obj == this) { - return true; - } else if (obj == null || obj.getClass() != getClass()) { - return false; - } - IfExpr expr = (IfExpr) obj; - return expr.guard.equals(guard) && expr.fbranch.equals(fbranch) && expr.tbranch.equals(tbranch); - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprBin.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntBinaryExpr.java similarity index 63% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprBin.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntBinaryExpr.java index 18bcd72b76..ae5c41224f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprBin.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntBinaryExpr.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Register; @@ -9,15 +9,15 @@ import java.math.BigInteger; -public class IExprBin extends IExpr { +public class IntBinaryExpr extends IntExpr { private final Expression lhs; private final Expression rhs; - private final IOpBin op; + private final IntBinaryOp op; - public IExprBin(IntegerType type, Expression lhs, IOpBin op, Expression rhs) { + IntBinaryExpr(IntegerType type, Expression lhs, IntBinaryOp op, Expression rhs) { super(type); - Preconditions.checkArgument(lhs.getType().equals(rhs.getType()), + Preconditions.checkArgument(lhs.getType().equals(rhs.getType()), "The types of %s and %s do not match.", lhs, rhs); this.lhs = lhs; this.rhs = rhs; @@ -35,23 +35,23 @@ public String toString() { } @Override - public IConst reduce() { - BigInteger v1 = lhs.reduce().getValue(); - BigInteger v2 = rhs.reduce().getValue(); - return new IValue(op.combine(v1, v2), getType()); - } - - public IOpBin getOp() { - return op; - } - - public Expression getRHS() { - return rhs; - } + public IntLiteral reduce() { + BigInteger v1 = lhs.reduce().getValue(); + BigInteger v2 = rhs.reduce().getValue(); + return new IntLiteral(op.combine(v1, v2), getType()); + } + + public IntBinaryOp getOp() { + return op; + } - public Expression getLHS() { - return lhs; - } + public Expression getRHS() { + return rhs; + } + + public Expression getLHS() { + return lhs; + } @Override public T accept(ExpressionVisitor visitor) { @@ -60,9 +60,9 @@ public T accept(ExpressionVisitor visitor) { @Override public int hashCode() { - if(op.equals(IOpBin.RSHIFT)) { - return lhs.hashCode() >>> rhs.hashCode(); - } + if (op.equals(IntBinaryOp.RSHIFT)) { + return lhs.hashCode() >>> rhs.hashCode(); + } return (op.combine(BigInteger.valueOf(lhs.hashCode()), BigInteger.valueOf(rhs.hashCode()))).intValue(); } @@ -73,7 +73,7 @@ public boolean equals(Object obj) { } else if (obj == null || obj.getClass() != getClass()) { return false; } - IExprBin expr = (IExprBin) obj; + IntBinaryExpr expr = (IntBinaryExpr) obj; return expr.op == op && expr.lhs.equals(lhs) && expr.rhs.equals(rhs); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntExpr.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntExpr.java new file mode 100644 index 0000000000..3d84cf57e2 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntExpr.java @@ -0,0 +1,19 @@ +package com.dat3m.dartagnan.expression; + +import com.dat3m.dartagnan.expression.type.IntegerType; + +import static com.google.common.base.Preconditions.checkNotNull; + +public abstract class IntExpr implements Expression { + + private final IntegerType type; + + protected IntExpr(IntegerType type) { + this.type = checkNotNull(type); + } + + @Override + public final IntegerType getType() { + return type; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IValue.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntLiteral.java similarity index 71% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/IValue.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntLiteral.java index 6709a91f3a..5bf86388e1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IValue.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntLiteral.java @@ -5,23 +5,28 @@ import java.math.BigInteger; -/** - * Immutable constant integer values. - */ -public final class IValue extends IConst { +public final class IntLiteral extends IntExpr { private final BigInteger value; - public IValue(BigInteger value, IntegerType type) { + IntLiteral(BigInteger value, IntegerType type) { super(type); this.value = value; } - @Override public BigInteger getValue() { return value; } + public int getValueAsInt() { + return value.intValueExact(); + } + + @Override + public IntLiteral reduce() { + return this; + } + public boolean isOne() { return value.equals(BigInteger.ONE); } public boolean isZero() { return value.equals(BigInteger.ZERO); } @@ -37,7 +42,7 @@ public int hashCode() { @Override public boolean equals(Object o) { - return this == o || o instanceof IValue val && getType().equals(val.getType()) && value.equals(val.value); + return this == o || o instanceof IntLiteral val && getType().equals(val.getType()) && value.equals(val.value); } @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprUn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntUnaryExpr.java similarity index 78% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprUn.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntUnaryExpr.java index 4c78bae856..69834686ca 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IExprUn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/IntUnaryExpr.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.expression; -import com.dat3m.dartagnan.expression.op.IOpUn; +import com.dat3m.dartagnan.expression.op.IntUnaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Register; @@ -8,22 +8,22 @@ import java.math.BigInteger; -import static com.dat3m.dartagnan.expression.op.IOpUn.CAST_SIGNED; -import static com.dat3m.dartagnan.expression.op.IOpUn.CAST_UNSIGNED; +import static com.dat3m.dartagnan.expression.op.IntUnaryOp.CAST_SIGNED; +import static com.dat3m.dartagnan.expression.op.IntUnaryOp.CAST_UNSIGNED; import static com.google.common.base.Verify.verify; -public class IExprUn extends IExpr { +public class IntUnaryExpr extends IntExpr { private final Expression b; - private final IOpUn op; + private final IntUnaryOp op; - public IExprUn(IOpUn op, Expression b, IntegerType t) { + IntUnaryExpr(IntUnaryOp op, Expression b, IntegerType t) { super(t); this.b = b; this.op = op; } - public IOpUn getOp() { + public IntUnaryOp getOp() { return op; } @@ -45,11 +45,11 @@ public String toString() { } @Override - public IConst reduce() { + public IntLiteral reduce() { if (!(b.getType() instanceof IntegerType innerType)) { throw new IllegalStateException(String.format("Non-integer operand %s.", b)); } - IConst inner = b.reduce(); + IntLiteral inner = b.reduce(); verify(inner.getType().equals(innerType), "Reduced to wrong type %s instead of %s.", inner.getType(), innerType); BigInteger value = inner.getValue(); @@ -64,17 +64,17 @@ public IConst reduce() { for (int i = targetType.getBitWidth(); i < value.bitLength(); i++) { v = v.clearBit(i); } - return new IValue(v, targetType); + return new IntLiteral(v, targetType); } if (!innerType.isMathematical()) { verify(innerType.canContain(value), ""); BigInteger result = innerType.applySign(value, signed); - return new IValue(result, targetType); + return new IntLiteral(result, targetType); } - return new IValue(value, targetType); + return new IntLiteral(value, targetType); } case MINUS -> { - return new IValue(value.negate(), targetType); + return new IntLiteral(value.negate(), targetType); } case CTLZ -> { if (innerType.isMathematical()) { @@ -82,12 +82,12 @@ public IConst reduce() { String.format("Counting leading zeroes in mathematical integer %s.", inner)); } if (value.signum() == -1) { - return new IValue(BigInteger.ZERO, targetType); + return new IntLiteral(BigInteger.ZERO, targetType); } int bitWidth = innerType.getBitWidth(); int length = value.bitLength(); verify(length <= bitWidth, "Value %s returned by %s not in range of type %s.", value); - return new IValue(BigInteger.valueOf(bitWidth - length), targetType); + return new IntLiteral(BigInteger.valueOf(bitWidth - length), targetType); } default -> throw new UnsupportedOperationException("Reduce not supported for " + this); } @@ -110,7 +110,7 @@ public boolean equals(Object obj) { } else if (obj == null || obj.getClass() != getClass()) { return false; } - IExprUn expr = (IExprUn) obj; + IntUnaryExpr expr = (IntUnaryExpr) obj; return expr.op == op && expr.b.equals(b); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/NonDetBool.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/NonDetBool.java new file mode 100644 index 0000000000..cbeba89d8e --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/NonDetBool.java @@ -0,0 +1,22 @@ +package com.dat3m.dartagnan.expression; + +import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; +import com.dat3m.dartagnan.expression.type.BooleanType; + +//TODO instances of this class should be managed by the program +public class NonDetBool extends BoolExpr { + + public NonDetBool(BooleanType type) { + super(type); + } + + @Override + public String toString() { + return "nondet_bool()"; + } + + @Override + public T accept(ExpressionVisitor visitor) { + return visitor.visit(this); + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/INonDet.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/NonDetInt.java similarity index 87% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/INonDet.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/NonDetInt.java index bb025c159f..e7315b734a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/INonDet.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/NonDetInt.java @@ -6,8 +6,8 @@ import java.math.BigInteger; import java.util.Optional; -// TODO why is INonDet not a IConst? -public class INonDet extends IExpr { +// TODO why is NonDetInt not a IntConst? +public class NonDetInt extends IntExpr { private final int id; private final boolean signed; @@ -16,7 +16,7 @@ public class INonDet extends IExpr { private String sourceName; // Should only be accessed from Program - public INonDet(int id, IntegerType type, boolean signed) { + public NonDetInt(int id, IntegerType type, boolean signed) { super(type); this.id = id; this.signed = signed; @@ -51,9 +51,9 @@ public void setSourceName(String name) { } @Override - public IConst reduce() { + public IntLiteral reduce() { if (min.equals(max)) { - return new IValue(min, getType()); + return new IntLiteral(min, getType()); } return super.reduce(); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BOpBin.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BOpBin.java deleted file mode 100644 index 57846c19f4..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BOpBin.java +++ /dev/null @@ -1,26 +0,0 @@ -package com.dat3m.dartagnan.expression.op; - -public enum BOpBin { - AND, OR; - - @Override - public String toString() { - switch(this){ - case AND: - return "&&"; - case OR: - return "||"; - } - return super.toString(); - } - - public boolean combine(boolean a, boolean b){ - switch(this){ - case AND: - return a && b; - case OR: - return a || b; - } - throw new UnsupportedOperationException("Illegal operator " + this + " in BOpBin"); - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BoolBinaryOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BoolBinaryOp.java new file mode 100644 index 0000000000..d7288a0e2a --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BoolBinaryOp.java @@ -0,0 +1,20 @@ +package com.dat3m.dartagnan.expression.op; + +public enum BoolBinaryOp { + AND, OR; + + @Override + public String toString() { + return switch (this) { + case AND -> "&&"; + case OR -> "||"; + }; + } + + public boolean combine(boolean a, boolean b){ + return switch (this) { + case AND -> a && b; + case OR -> a || b; + }; + } +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BOpUn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BoolUnaryOp.java similarity index 88% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BOpUn.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BoolUnaryOp.java index e93fb48393..c3459138a0 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BOpUn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/BoolUnaryOp.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.expression.op; -public enum BOpUn { +public enum BoolUnaryOp { NOT; @Override diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/COpBin.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/COpBin.java deleted file mode 100644 index fe120fafe2..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/COpBin.java +++ /dev/null @@ -1,115 +0,0 @@ -package com.dat3m.dartagnan.expression.op; - -import java.math.BigInteger; - -public enum COpBin { - EQ, NEQ, GTE, LTE, GT, LT, UGTE, ULTE, UGT, ULT; - - @Override - public String toString() { - switch(this){ - case EQ: - return "=="; - case NEQ: - return "!="; - case GTE: - case UGTE: - return ">="; - case LTE: - case ULTE: - return "<="; - case GT: - case UGT: - return ">"; - case LT: - case ULT: - return "<"; - } - return super.toString(); - } - - public COpBin inverted() { - switch(this){ - case EQ: - return NEQ; - case NEQ: - return EQ; - case GTE: - return LT; - case UGTE: - return ULT; - case LTE: - return GT; - case ULTE: - return UGT; - case GT: - return LTE; - case UGT: - return ULTE; - case LT: - return GTE; - case ULT: - return UGTE; - default: - throw new UnsupportedOperationException(this + " cannot be inverted"); - } - } - - public boolean isSigned() { - switch(this){ - case EQ: case NEQ: - case GTE: case LTE: case GT: case LT: - return true; - case UGTE: case ULTE: case UGT: case ULT: - return false; - default: - throw new UnsupportedOperationException("isSigned() not implemented for " + this); - } - } - - public boolean combine(BigInteger a, BigInteger b){ - switch(this){ - case EQ: - return a.compareTo(b) == 0; - case NEQ: - return a.compareTo(b) != 0; - case LT: - case ULT: - return a.compareTo(b) < 0; - case LTE: - case ULTE: - return a.compareTo(b) <= 0; - case GT: - case UGT: - return a.compareTo(b) > 0; - case GTE: - case UGTE: - return a.compareTo(b) >= 0; - } - throw new UnsupportedOperationException("Illegal operator " + this + " in COpBin"); - } - - // Due to constant propagation, and the lack of a proper type system - // we can end up with comparisons like "False == 1", thus the following two methods - public boolean combine(boolean a, BigInteger b){ - switch(this){ - case EQ: - return ((b.compareTo(BigInteger.ONE) == 0) == a); - case NEQ: - return ((b.compareTo(BigInteger.ONE) == 0) != a); - default: - throw new UnsupportedOperationException("Illegal operator " + this + " in COpBin"); - } - } - - public boolean combine(BigInteger a, boolean b){ - switch(this){ - case EQ: - return ((a.compareTo(BigInteger.ONE) == 0) == b); - case NEQ: - return ((a.compareTo(BigInteger.ONE) == 0) != b); - default: - throw new UnsupportedOperationException("Illegal operator " + this + " in COpBin"); - } - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/CmpOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/CmpOp.java new file mode 100644 index 0000000000..0f8623ea75 --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/CmpOp.java @@ -0,0 +1,53 @@ +package com.dat3m.dartagnan.expression.op; + +import java.math.BigInteger; + +public enum CmpOp { + EQ, NEQ, GTE, LTE, GT, LT, UGTE, ULTE, UGT, ULT; + + @Override + public String toString() { + return switch (this) { + case EQ -> "=="; + case NEQ -> "!="; + case GTE, UGTE -> ">="; + case LTE, ULTE -> "<="; + case GT, UGT -> ">"; + case LT, ULT -> "<"; + }; + } + + public CmpOp inverted() { + return switch (this) { + case EQ -> NEQ; + case NEQ -> EQ; + case GTE -> LT; + case UGTE -> ULT; + case LTE -> GT; + case ULTE -> UGT; + case GT -> LTE; + case UGT -> ULTE; + case LT -> GTE; + case ULT -> UGTE; + }; + } + + public boolean isSigned() { + return switch (this) { + case EQ, NEQ, GTE, LTE, GT, LT -> true; + case UGTE, ULTE, UGT, ULT -> false; + }; + } + + public boolean combine(BigInteger a, BigInteger b){ + return switch (this) { + case EQ -> a.compareTo(b) == 0; + case NEQ -> a.compareTo(b) != 0; + case LT, ULT -> a.compareTo(b) < 0; + case LTE, ULTE -> a.compareTo(b) <= 0; + case GT, UGT -> a.compareTo(b) > 0; + case GTE, UGTE -> a.compareTo(b) >= 0; + }; + } + +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IOpBin.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IntBinaryOp.java similarity index 52% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IOpBin.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IntBinaryOp.java index 9f3f31105e..48cdbb43c6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IOpBin.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IntBinaryOp.java @@ -1,61 +1,44 @@ package com.dat3m.dartagnan.expression.op; import java.math.BigInteger; -import java.util.Arrays; -import java.util.List; -public enum IOpBin { +public enum IntBinaryOp { ADD, SUB, MUL, DIV, UDIV, MOD, AND, OR, XOR, LSHIFT, RSHIFT, ARSHIFT, SREM, UREM; - - public static List BWOps = Arrays.asList(UDIV, AND, OR, XOR, LSHIFT, RSHIFT, ARSHIFT, SREM, UREM); - + @Override public String toString() { - switch(this){ - case ADD: - return "+"; - case SUB: - return "-"; - case MUL: - return "*"; - case DIV: - return "/"; - case MOD: - return "%"; - case AND: - return "&"; - case OR: - return "|"; - case XOR: - return "^"; - case LSHIFT: - return "<<"; - case RSHIFT: - return ">>>"; - case ARSHIFT: - return ">>"; - default: - return super.toString(); - } + return switch (this) { + case ADD -> "+"; + case SUB -> "-"; + case MUL -> "*"; + case DIV -> "/"; + case MOD -> "%"; + case AND -> "&"; + case OR -> "|"; + case XOR -> "^"; + case LSHIFT -> "<<"; + case RSHIFT -> ">>>"; + case ARSHIFT -> ">>"; + default -> super.toString(); + }; } - public String getName(){ + public String getName() { return this.name().toLowerCase(); } - public static IOpBin intToOp(int i) { - switch(i) { - case 0: return ADD; - case 1: return SUB; - case 2: return AND; - case 3: return OR; - default: - throw new UnsupportedOperationException("The binary operator is not recognized"); - } + public static IntBinaryOp intToOp(int i) { + return switch (i) { + case 0 -> ADD; + case 1 -> SUB; + case 2 -> AND; + case 3 -> OR; + default -> throw new UnsupportedOperationException("The binary operator is not recognized"); + }; } - public BigInteger combine(BigInteger a, BigInteger b){ - switch(this){ + public BigInteger combine(BigInteger a, BigInteger b) { + switch (this) { case ADD: return a.add(b); case SUB: @@ -87,6 +70,6 @@ public BigInteger combine(BigInteger a, BigInteger b){ case ARSHIFT: return a.shiftRight(b.intValue()); } - throw new UnsupportedOperationException("Illegal operator " + this + " in IOpBin"); + throw new UnsupportedOperationException("Illegal operator " + this + " in IntBinaryOp"); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IOpUn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IntUnaryOp.java similarity index 93% rename from dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IOpUn.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IntUnaryOp.java index 28b9db5f54..ead0a60b51 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IOpUn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/op/IntUnaryOp.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.expression.op; -public enum IOpUn { +public enum IntUnaryOp { CAST_SIGNED, CAST_UNSIGNED, CTLZ, diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java index f26c6be800..948bdf060e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprSimplifier.java @@ -1,15 +1,13 @@ package com.dat3m.dartagnan.expression.processing; import com.dat3m.dartagnan.expression.*; -import com.dat3m.dartagnan.expression.op.BOpUn; -import com.dat3m.dartagnan.expression.op.COpBin; -import com.dat3m.dartagnan.expression.op.IOpBin; -import com.dat3m.dartagnan.expression.type.BooleanType; +import com.dat3m.dartagnan.expression.op.BoolUnaryOp; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.memory.MemoryObject; import java.math.BigInteger; -import static com.dat3m.dartagnan.expression.op.IOpBin.RSHIFT; +import static com.dat3m.dartagnan.expression.op.IntBinaryOp.RSHIFT; public class ExprSimplifier extends ExprTransformer { @@ -18,49 +16,24 @@ public Expression visit(Atom atom) { Expression lhs = atom.getLHS().accept(this); Expression rhs = atom.getRHS().accept(this); if (lhs.equals(rhs)) { - switch(atom.getOp()) { - case EQ: - case LTE: - case ULTE: - case GTE: - case UGTE: - return expressions.makeTrue(); - case NEQ: - case LT: - case ULT: - case GT: - case UGT: - return expressions.makeFalse(); - } - } - if (lhs instanceof IConst lc && rhs instanceof IConst rc) { - return expressions.makeValue(atom.getOp().combine(lc.getValue(), rc.getValue())); - } - // Due to constant propagation, and the lack of a proper type system - // we can end up with comparisons like "False == 1" - if (lhs instanceof BConst lc && rhs instanceof IConst rc) { - return expressions.makeValue(atom.getOp().combine(lc.getValue(), rc.getValue())); + return switch (atom.getOp()) { + case EQ, LTE, ULTE, GTE, UGTE -> expressions.makeTrue(); + case NEQ, LT, ULT, GT, UGT -> expressions.makeFalse(); + }; } - if (lhs instanceof IConst lc && rhs instanceof BConst rc) { + if (lhs instanceof IntLiteral lc && rhs instanceof IntLiteral rc) { return expressions.makeValue(atom.getOp().combine(lc.getValue(), rc.getValue())); } - if (lhs.getType() instanceof BooleanType && rhs instanceof IConst rc) { - // Simplify "cond == 1" to just "cond" - // TODO: If necessary, add versions for "cond == 0" and for "cond != 0/1" - if (atom.getOp() == COpBin.EQ && rc.getValue().intValue() == 1) { - return lhs; - } - } return expressions.makeBinary(lhs, atom.getOp(), rhs); } @Override - public Expression visit(BExprBin bBin) { + public Expression visit(BoolBinaryExpr bBin) { Expression l = bBin.getLHS().accept(this); Expression r = bBin.getRHS().accept(this); - Expression left = l instanceof BConst || !(r instanceof BConst) ? l : r; + Expression left = l instanceof BoolLiteral || !(r instanceof BoolLiteral) ? l : r; Expression right = left == l ? r : l; - if (left instanceof BConst constant) { + if (left instanceof BoolLiteral constant) { boolean value = constant.getValue(); boolean neutralValue = switch (bBin.getOp()) { case OR -> false; @@ -78,13 +51,13 @@ public Expression visit(BExprBin bBin) { } @Override - public Expression visit(BExprUn bUn) { + public Expression visit(BoolUnaryExpr bUn) { Expression inner = bUn.getInner().accept(this); - assert bUn.getOp() == BOpUn.NOT; - if (inner instanceof BConst constant) { + assert bUn.getOp() == BoolUnaryOp.NOT; + if (inner instanceof BoolLiteral constant) { return expressions.makeValue(!constant.getValue()); } - if (inner instanceof BExprUn innerUnary && innerUnary.getOp() == BOpUn.NOT) { + if (inner instanceof BoolUnaryExpr innerUnary && innerUnary.getOp() == BoolUnaryOp.NOT) { return innerUnary.getInner(); } @@ -96,10 +69,10 @@ public Expression visit(BExprUn bUn) { } @Override - public Expression visit(IExprBin iBin) { + public Expression visit(IntBinaryExpr iBin) { Expression lhs = iBin.getLHS().accept(this); Expression rhs = iBin.getRHS().accept(this); - IOpBin op = iBin.getOp(); + IntBinaryOp op = iBin.getOp(); if (lhs.equals(rhs)) { switch(op) { case AND: @@ -109,10 +82,10 @@ public Expression visit(IExprBin iBin) { return expressions.makeZero(iBin.getType()); } } - if (! (lhs instanceof IConst || rhs instanceof IConst)) { + if (! (lhs instanceof IntLiteral || rhs instanceof IntLiteral)) { return expressions.makeBinary(lhs, op, rhs); - } else if (lhs instanceof IConst && rhs instanceof IConst) { - // If we reduce MemoryObject as a normal IConst, we loose the fact that it is a Memory Object + } else if (lhs instanceof IntLiteral && rhs instanceof IntLiteral) { + // If we reduce MemoryObject as a normal IntLiteral, we loose the fact that it is a Memory Object // We cannot call reduce for RSHIFT (lack of implementation) if(!(lhs instanceof MemoryObject) && op != RSHIFT) { return expressions.makeBinary(lhs, op, rhs).reduce(); @@ -123,7 +96,7 @@ public Expression visit(IExprBin iBin) { } } - if (lhs instanceof IConst lc) { + if (lhs instanceof IntLiteral lc) { BigInteger val = lc.getValue(); switch (op) { case MUL: @@ -141,7 +114,7 @@ public Expression visit(IExprBin iBin) { return expressions.makeBinary(lhs, op, rhs); } - IConst rc = (IConst)rhs; + IntLiteral rc = (IntLiteral)rhs; BigInteger val = rc.getValue(); switch (op) { case MUL: @@ -157,10 +130,10 @@ public Expression visit(IExprBin iBin) { if(val.equals(BigInteger.ZERO)) { return lhs; } - // Rule for associativity (rhs is IConst) since we cannot reduce MemoryObjects + // Rule for associativity (rhs is IntLiteral) since we cannot reduce MemoryObjects // Either op can be +/-, but this does not affect correctness // e.g. (&mem + x) - y -> &mem + reduced(x - y) - if(lhs instanceof IExprBin lhsBin && lhsBin.getRHS() instanceof IConst && lhsBin.getOp() != RSHIFT) { + if(lhs instanceof IntBinaryExpr lhsBin && lhsBin.getRHS() instanceof IntLiteral && lhsBin.getOp() != RSHIFT) { Expression newLHS = lhsBin.getLHS(); Expression newRHS = expressions.makeBinary(lhsBin.getRHS(), lhsBin.getOp(), rhs).reduce(); return expressions.makeBinary(newLHS, op, newRHS); @@ -171,18 +144,18 @@ public Expression visit(IExprBin iBin) { } @Override - public Expression visit(IExprUn iUn) { + public Expression visit(IntUnaryExpr iUn) { // TODO: Add simplifications return super.visit(iUn); } @Override - public Expression visit(IfExpr ifExpr) { - Expression cond = ifExpr.getGuard().accept(this); - Expression t = ifExpr.getTrueBranch().accept(this); - Expression f = ifExpr.getFalseBranch().accept(this); + public Expression visit(ITEExpr iteExpr) { + Expression cond = iteExpr.getGuard().accept(this); + Expression t = iteExpr.getTrueBranch().accept(this); + Expression f = iteExpr.getFalseBranch().accept(this); - if (cond instanceof BConst constantGuard) { + if (cond instanceof BoolLiteral constantGuard) { return constantGuard.getValue() ? t : f; } else if (t.equals(f)) { return t; @@ -190,15 +163,15 @@ public Expression visit(IfExpr ifExpr) { // Simplifies "ITE(cond, 1, 0)" to "cond" and "ITE(cond, 0, 1) to "!cond" // TODO: It is not clear if this gives performance improvements or not - if (t instanceof IConst tConstant && tConstant.getType().isMathematical() && tConstant.getValueAsInt() == 1 - && f instanceof IConst fConstant && fConstant.getType().isMathematical() && fConstant.getValueAsInt() == 0) { + if (t instanceof IntLiteral tConstant && tConstant.getType().isMathematical() && tConstant.getValueAsInt() == 1 + && f instanceof IntLiteral fConstant && fConstant.getType().isMathematical() && fConstant.getValueAsInt() == 0) { return cond; - } else if (t instanceof IConst tConstant && tConstant.getType().isMathematical() && tConstant.getValueAsInt() == 0 - && f instanceof IConst fConstant && fConstant.getType().isMathematical() && fConstant.getValueAsInt() == 1) { + } else if (t instanceof IntLiteral tConstant && tConstant.getType().isMathematical() && tConstant.getValueAsInt() == 0 + && f instanceof IntLiteral fConstant && fConstant.getType().isMathematical() && fConstant.getValueAsInt() == 1) { return expressions.makeNot(cond); } - return expressions.makeConditional(cond, t, f); + return expressions.makeITE(cond, t, f); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java index 4aeb60e6c1..ea21d9ebf5 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExprTransformer.java @@ -20,50 +20,50 @@ public Expression visit(Atom atom) { } @Override - public Expression visit(BConst bConst) { - return bConst; + public Expression visit(BoolLiteral boolLiteral) { + return boolLiteral; } @Override - public Expression visit(BExprBin bBin) { + public Expression visit(BoolBinaryExpr bBin) { return expressions.makeBinary(bBin.getLHS().accept(this), bBin.getOp(), bBin.getRHS().accept(this)); } @Override - public Expression visit(BExprUn bUn) { + public Expression visit(BoolUnaryExpr bUn) { return expressions.makeUnary(bUn.getOp(), bUn.getInner().accept(this)); } @Override - public Expression visit(BNonDet bNonDet) { - return bNonDet; + public Expression visit(NonDetBool nonDetBool) { + return nonDetBool; } @Override - public Expression visit(IValue iValue) { - return iValue; + public Expression visit(IntLiteral intLiteral) { + return intLiteral; } @Override - public Expression visit(IExprBin iBin) { + public Expression visit(IntBinaryExpr iBin) { return expressions.makeBinary(iBin.getLHS().accept(this), iBin.getOp(), iBin.getRHS().accept(this)); } @Override - public Expression visit(IExprUn iUn) { + public Expression visit(IntUnaryExpr iUn) { return expressions.makeUnary(iUn.getOp(), iUn.getInner().accept(this), iUn.getType()); } @Override - public Expression visit(IfExpr ifExpr) { - return expressions.makeConditional( - ifExpr.getGuard().accept(this), - ifExpr.getTrueBranch().accept(this), - ifExpr.getFalseBranch().accept(this)); + public Expression visit(ITEExpr iteExpr) { + return expressions.makeITE( + iteExpr.getGuard().accept(this), + iteExpr.getTrueBranch().accept(this), + iteExpr.getFalseBranch().accept(this)); } @Override - public Expression visit(INonDet iNonDet) { + public Expression visit(NonDetInt iNonDet) { return iNonDet; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionInspector.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionInspector.java index 2851321ba2..fc41113b9f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionInspector.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionInspector.java @@ -17,33 +17,33 @@ default Expression visit(Atom atom) { return atom; } - default Expression visit(BExprBin bBin) { + default Expression visit(BoolBinaryExpr bBin) { bBin.getLHS().accept(this); bBin.getRHS().accept(this); return bBin; } - default Expression visit(BExprUn bUn) { + default Expression visit(BoolUnaryExpr bUn) { bUn.getInner().accept(this); return bUn; } - default Expression visit(IExprBin iBin) { + default Expression visit(IntBinaryExpr iBin) { iBin.getLHS().accept(this); iBin.getRHS().accept(this); return iBin; } - default Expression visit(IExprUn iUn) { + default Expression visit(IntUnaryExpr iUn) { iUn.getInner().accept(this); return iUn; } - default Expression visit(IfExpr ifExpr) { - ifExpr.getGuard().accept(this); - ifExpr.getFalseBranch().accept(this); - ifExpr.getTrueBranch().accept(this); - return ifExpr; + default Expression visit(ITEExpr iteExpr) { + iteExpr.getGuard().accept(this); + iteExpr.getFalseBranch().accept(this); + iteExpr.getTrueBranch().accept(this); + return iteExpr; } default Expression visit(Construction construction) { @@ -66,10 +66,10 @@ default Expression visit(Location location) { return location; } - default Expression visit(BConst bConst) { return bConst; } - default Expression visit(BNonDet bNonDet) { return bNonDet; } - default Expression visit(IValue iValue) { return iValue; } - default Expression visit(INonDet iNonDet) { return iNonDet; } + default Expression visit(BoolLiteral boolLiteral) { return boolLiteral; } + default Expression visit(NonDetBool nonDetBool) { return nonDetBool; } + default Expression visit(IntLiteral intLiteral) { return intLiteral; } + default Expression visit(NonDetInt iNonDet) { return iNonDet; } default Expression visit(Register reg) { return reg; } default Expression visit(MemoryObject address) { return address; } default Expression visit(Function function) { return function; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionVisitor.java b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionVisitor.java index f1c2b5c229..6e782b2da1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionVisitor.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/expression/processing/ExpressionVisitor.java @@ -8,15 +8,15 @@ public interface ExpressionVisitor { default T visit(Atom atom) { return null; } - default T visit(BConst bConst) { return null; } - default T visit(BExprBin bBin) { return null; } - default T visit(BExprUn bUn) { return null; } - default T visit(BNonDet bNonDet) { return null; } - default T visit(IValue iValue) { return null; } - default T visit(IExprBin iBin) { return null; } - default T visit(IExprUn iUn) { return null; } - default T visit(IfExpr ifExpr) { return null; } - default T visit(INonDet iNonDet) { return null; } + default T visit(BoolLiteral boolLiteral) { return null; } + default T visit(BoolBinaryExpr bBin) { return null; } + default T visit(BoolUnaryExpr bUn) { return null; } + default T visit(NonDetBool nonDetBool) { return null; } + default T visit(IntLiteral intLiteral) { return null; } + default T visit(IntBinaryExpr iBin) { return null; } + default T visit(IntUnaryExpr iUn) { return null; } + default T visit(ITEExpr iteExpr) { return null; } + default T visit(NonDetInt iNonDet) { return null; } default T visit(Register reg) { return null; } default T visit(MemoryObject address) { return null; } default T visit(Location location) { return null; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java index a6d27bc139..5c5443ce8b 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/utils/ProgramBuilder.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IConst; -import com.dat3m.dartagnan.expression.INonDet; +import com.dat3m.dartagnan.expression.IntLiteral; +import com.dat3m.dartagnan.expression.NonDetInt; import com.dat3m.dartagnan.expression.type.FunctionType; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; @@ -23,6 +23,7 @@ import com.dat3m.dartagnan.program.memory.VirtualMemoryObject; import com.dat3m.dartagnan.program.processing.IdReassignment; import com.dat3m.dartagnan.program.specification.AbstractAssert; +import com.google.common.base.Preconditions; import com.google.common.base.Verify; import com.google.common.collect.Iterables; @@ -189,8 +190,8 @@ public MemoryObject newMemoryObject(String name, int size) { return mem; } - public INonDet newConstant(IntegerType type, boolean signed) { - var constant = new INonDet(program.getConstants().size(), type, signed); + public NonDetInt newConstant(IntegerType type, boolean signed) { + var constant = new NonDetInt(program.getConstants().size(), type, signed); program.addConstant(constant); return constant; } @@ -220,8 +221,9 @@ public void initRegEqLocVal(int regThread, String regName, String locName, Type addChild(regThread, EventFactory.newLocal(reg,getInitialValue(locName))); } - public void initRegEqConst(int regThread, String regName, IConst iValue){ - addChild(regThread, EventFactory.newLocal(getOrNewRegister(regThread, regName, iValue.getType()), iValue)); + public void initRegEqConst(int regThread, String regName, Expression value){ + Preconditions.checkArgument(value.getRegs().isEmpty()); + addChild(regThread, EventFactory.newLocal(getOrNewRegister(regThread, regName, value.getType()), value)); } private Expression getInitialValue(String name) { @@ -287,7 +289,7 @@ public void newScopedThread(Arch arch, int id, int ...ids) { newScopedThread(arch, String.valueOf(id), id, ids); } - public void initVirLocEqCon(String leftName, IConst iValue){ + public void initVirLocEqCon(String leftName, IntLiteral iValue){ MemoryObject object = locations.computeIfAbsent( leftName, k->program.getMemory().allocateVirtual(1, true, true, null)); object.setCVar(leftName); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java index 9395147ecf..a84472d9ef 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusAArch64.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusAArch64BaseVisitor; @@ -208,7 +208,7 @@ public Object visitBranchRegister(LitmusAArch64Parser.BranchRegisterContext ctx) if (!(register.getType() instanceof IntegerType integerType)) { throw new ParsingException("Comparing non-integer register."); } - IValue zero = expressions.makeZero(integerType); + IntLiteral zero = expressions.makeZero(integerType); Expression expr = expressions.makeBinary(register, ctx.branchRegInstruction().op, zero); Label label = programBuilder.getOrCreateLabel(mainThread, ctx.label().getText()); return programBuilder.addChild(mainThread, EventFactory.newJump(expr, label)); @@ -228,7 +228,7 @@ public Object visitFence(LitmusAArch64Parser.FenceContext ctx) { public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegister64Context ctx) { Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register64().id, archType); if(ctx.shift() != null){ - IValue val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); + IntLiteral val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); expr = expressions.makeBinary(expr, ctx.shift().shiftOperator().op, val); } return expr; @@ -238,7 +238,7 @@ public Expression visitExpressionRegister64(LitmusAArch64Parser.ExpressionRegist public Expression visitExpressionRegister32(LitmusAArch64Parser.ExpressionRegister32Context ctx) { Expression expr = programBuilder.getOrNewRegister(mainThread, ctx.register32().id, archType); if(ctx.shift() != null){ - IValue val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); + IntLiteral val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); expr = expressions.makeBinary(expr, ctx.shift().shiftOperator().op, val); } return expr; @@ -248,7 +248,7 @@ public Expression visitExpressionRegister32(LitmusAArch64Parser.ExpressionRegist public Expression visitExpressionImmediate(LitmusAArch64Parser.ExpressionImmediateContext ctx) { Expression expr = expressions.parseValue(ctx.immediate().constant().getText(), archType); if(ctx.shift() != null){ - IValue val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); + IntLiteral val = expressions.parseValue(ctx.shift().immediate().constant().getText(), archType); expr = expressions.makeBinary(expr, ctx.shift().shiftOperator().op, val); } return expr; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java index a126788b8a..40b3b31bac 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusC.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.parsers.LitmusCBaseVisitor; import com.dat3m.dartagnan.parsers.LitmusCParser; @@ -72,7 +72,7 @@ public Program visitMain(LitmusCParser.MainContext ctx) { @Override public Object visitGlobalDeclaratorLocation(LitmusCParser.GlobalDeclaratorLocationContext ctx) { if (ctx.initConstantValue() != null) { - IValue value = expressions.parseValue(ctx.initConstantValue().constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.initConstantValue().constant().getText(), archType); programBuilder.initLocEqConst(ctx.varName().getText(), value); } return null; @@ -83,7 +83,7 @@ public Object visitGlobalDeclaratorRegister(LitmusCParser.GlobalDeclaratorRegist if (ctx.initConstantValue() != null) { // FIXME: We visit declarators before threads, so we need to create threads early programBuilder.getOrNewThread(ctx.threadId().id); - IValue value = expressions.parseValue(ctx.initConstantValue().constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.initConstantValue().constant().getText(), archType); programBuilder.initRegEqConst(ctx.threadId().id,ctx.varName().getText(), value); } return null; @@ -435,7 +435,7 @@ public Expression visitReVarName(LitmusCParser.ReVarNameContext ctx){ @Override public Expression visitReConst(LitmusCParser.ReConstContext ctx){ Register register = getReturnRegister(false); - IValue result = expressions.parseValue(ctx.getText(), archType); + IntLiteral result = expressions.parseValue(ctx.getText(), archType); return assignToReturnRegister(register, result); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusLISA.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusLISA.java index e959b53b42..366e7c72ce 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusLISA.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusLISA.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.parsers.LitmusLISABaseVisitor; import com.dat3m.dartagnan.parsers.LitmusLISAParser; @@ -54,14 +54,14 @@ public Object visitMain(LitmusLISAParser.MainContext ctx) { @Override public Object visitVariableDeclaratorLocation(LitmusLISAParser.VariableDeclaratorLocationContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initLocEqConst(ctx.location().getText(), value); return null; } @Override public Object visitVariableDeclaratorRegister(LitmusLISAParser.VariableDeclaratorRegisterContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initRegEqConst(ctx.threadId().id, ctx.register().getText(), value); return null; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java index 8babca5754..d837858778 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusPPCBaseVisitor; @@ -77,14 +77,14 @@ public Object visitMain(LitmusPPCParser.MainContext ctx) { @Override public Object visitVariableDeclaratorLocation(LitmusPPCParser.VariableDeclaratorLocationContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initLocEqConst(ctx.location().getText(), value); return null; } @Override public Object visitVariableDeclaratorRegister(LitmusPPCParser.VariableDeclaratorRegisterContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initRegEqConst(ctx.threadId().id, ctx.register().getText(), value); return null; } @@ -130,7 +130,7 @@ public Object visitInstructionRow(LitmusPPCParser.InstructionRowContext ctx) { @Override public Object visitLi(LitmusPPCParser.LiContext ctx) { Register register = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant)); } @@ -171,7 +171,7 @@ public Object visitMr(LitmusPPCParser.MrContext ctx) { public Object visitAddi(LitmusPPCParser.AddiContext ctx) { Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText()); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeADD(r2, constant))); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java index 0a60d40f88..a6b5002424 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IConst; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.IntLiteral; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusPTXBaseVisitor; @@ -67,14 +67,14 @@ public Object visitMain(LitmusPTXParser.MainContext ctx) { @Override public Object visitVariableDeclaratorLocation(LitmusPTXParser.VariableDeclaratorLocationContext ctx) { programBuilder.initVirLocEqCon(ctx.location().getText(), - (IConst) ctx.constant().accept(this)); + (IntLiteral) ctx.constant().accept(this)); return null; } @Override public Object visitVariableDeclaratorRegister(LitmusPTXParser.VariableDeclaratorRegisterContext ctx) { programBuilder.initRegEqConst(ctx.threadId().id, ctx.register().getText(), - (IConst) ctx.constant().accept(this)); + (IntLiteral) ctx.constant().accept(this)); return null; } @@ -226,7 +226,7 @@ public Object visitAtomOp(LitmusPTXParser.AtomOpContext ctx) { Register register_destination = (Register) ctx.register().accept(this); MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); Expression value = (Expression) ctx.value().accept(this); - IOpBin op = ctx.operation().op; + IntBinaryOp op = ctx.operation().op; String mo = ctx.mo().content; String scope = ctx.scope().content; if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { @@ -272,7 +272,7 @@ public Object visitAtomExchange(LitmusPTXParser.AtomExchangeContext ctx) { public Object visitRedInstruction(LitmusPTXParser.RedInstructionContext ctx) { MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); Expression value = (Expression) ctx.value().accept(this); - IOpBin op = ctx.operation().op; + IntBinaryOp op = ctx.operation().op; String mo = ctx.mo().content; String scope = ctx.scope().content; if (!(mo.equals(Tag.PTX.ACQ) || mo.equals(Tag.PTX.REL) || mo.equals(Tag.PTX.ACQ_REL) || mo.equals(Tag.PTX.RLX))) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java index 4ff717b582..14e63d576f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusRISCV.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.processing.ExprTransformer; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.IntegerType; @@ -87,14 +87,14 @@ public Expression visit(Register reg) { @Override public Object visitVariableDeclaratorLocation(LitmusRISCVParser.VariableDeclaratorLocationContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initLocEqConst(ctx.location().getText(), value); return null; } @Override public Object visitVariableDeclaratorRegister(LitmusRISCVParser.VariableDeclaratorRegisterContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initRegEqConst(ctx.threadId().id, ctx.register().getText(), value); return null; } @@ -140,7 +140,7 @@ public Object visitInstructionRow(LitmusRISCVParser.InstructionRowContext ctx) { @Override public Object visitLi(LitmusRISCVParser.LiContext ctx) { Register register = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant)); } @@ -184,7 +184,7 @@ public Object visitAdd(LitmusRISCVParser.AddContext ctx) { public Object visitXori(LitmusRISCVParser.XoriContext ctx) { Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText()); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeXOR(r2, constant))); } @@ -192,7 +192,7 @@ public Object visitXori(LitmusRISCVParser.XoriContext ctx) { public Object visitAndi(LitmusRISCVParser.AndiContext ctx) { Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); Register r2 = programBuilder.getOrErrorRegister(mainThread, ctx.register(1).getText()); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeAND(r2, constant))); } @@ -200,7 +200,7 @@ public Object visitAndi(LitmusRISCVParser.AndiContext ctx) { public Object visitOri(LitmusRISCVParser.OriContext ctx) { Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); Register r2 = programBuilder.getOrNewRegister(mainThread, ctx.register(1).getText(), archType); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeOR(r2, constant))); } @@ -208,7 +208,7 @@ public Object visitOri(LitmusRISCVParser.OriContext ctx) { public Object visitAddi(LitmusRISCVParser.AddiContext ctx) { Register r1 = programBuilder.getOrNewRegister(mainThread, ctx.register(0).getText(), archType); Register r2 = programBuilder.getOrNewRegister(mainThread, ctx.register(1).getText(), archType); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(r1, expressions.makeADD(r2, constant))); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java index 134e2d4f79..c7cd10ae15 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java @@ -4,8 +4,8 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IConst; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.IntLiteral; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusVulkanBaseVisitor; @@ -77,14 +77,14 @@ public Object visitMain(LitmusVulkanParser.MainContext ctx) { @Override public Object visitVariableDeclaratorLocation(LitmusVulkanParser.VariableDeclaratorLocationContext ctx) { programBuilder.initVirLocEqCon(ctx.location().getText(), - (IConst) ctx.constant().accept(this)); + (IntLiteral) ctx.constant().accept(this)); return null; } @Override public Object visitVariableDeclaratorRegister(LitmusVulkanParser.VariableDeclaratorRegisterContext ctx) { programBuilder.initRegEqConst(ctx.threadId().id, ctx.register().getText(), - (IConst) ctx.constant().accept(this)); + (IntLiteral) ctx.constant().accept(this)); return null; } @@ -307,7 +307,7 @@ public Object visitRmwOp(LitmusVulkanParser.RmwOpContext ctx) { String avvis = (ctx.avvis() != null) ? ctx.avvis().content : ""; String scope = (ctx.scope() != null) ? ctx.scope().content : ""; String storageClass = ctx.storageClass().content; - IOpBin op = ctx.operation().op; + IntBinaryOp op = ctx.operation().op; List storageClassSemantics = (List) ctx.storageClassSemanticList().accept(this); List avvisSemantics = (List) ctx.avvisSemanticList().accept(this); VulkanRMWOp rmw = EventFactory.Vulkan.newRMWOp(location, register, value, op, mo, scope); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java index f51aa513dd..9db0707de9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.configuration.Arch; import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.LitmusX86BaseVisitor; @@ -62,14 +62,14 @@ public Object visitMain(LitmusX86Parser.MainContext ctx) { @Override public Object visitVariableDeclaratorLocation(LitmusX86Parser.VariableDeclaratorLocationContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initLocEqConst(ctx.location().getText(), value); return null; } @Override public Object visitVariableDeclaratorRegister(LitmusX86Parser.VariableDeclaratorRegisterContext ctx) { - IValue value = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral value = expressions.parseValue(ctx.constant().getText(), archType); programBuilder.initRegEqConst(ctx.threadId().id, ctx.register().getText(), value); return null; } @@ -115,7 +115,7 @@ public Object visitInstructionRow(LitmusX86Parser.InstructionRowContext ctx) { @Override public Object visitLoadValueToRegister(LitmusX86Parser.LoadValueToRegisterContext ctx) { Register register = programBuilder.getOrNewRegister(mainThread, ctx.register().getText(), archType); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newLocal(register, constant)); } @@ -129,7 +129,7 @@ public Object visitLoadLocationToRegister(LitmusX86Parser.LoadLocationToRegister @Override public Object visitStoreValueToLocation(LitmusX86Parser.StoreValueToLocationContext ctx) { MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText()); - IValue constant = expressions.parseValue(ctx.constant().getText(), archType); + IntLiteral constant = expressions.parseValue(ctx.constant().getText(), archType); return programBuilder.addChild(mainThread, EventFactory.newStore(object, constant)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java index 1d2bc7db9c..07e888e7e7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLlvm.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.expression.*; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.parsers.LLVMIRBaseVisitor; @@ -626,17 +626,17 @@ public Expression visitXorInst(XorInstContext ctx) { final Expression left = visitTypeValue(ctx.typeValue()); final Expression right = checkExpression(left.getType(), ctx.value()); final Expression xorExpr; - if ((right instanceof IValue iValue && iValue.getType().isMathematical() - && (iValue.isZero() || iValue.isOne()))) { + if ((right instanceof IntLiteral intLiteral && intLiteral.getType().isMathematical() + && (intLiteral.isZero() || intLiteral.isOne()))) { // NOTE: If we parse the program with mathematical integers, we try to eliminate "xor 1" expressions. // The reason is that "xor 1" is used to implement boolean negations, i.e., even if the C source program // has no bitwise operators, "xor 1" is frequently added by the compiler. // Not eliminating this operator frequently results in theory-mixing that the SMT-backend cannot handle. - if (iValue.isZero()) { + if (intLiteral.isZero()) { xorExpr = left; } else { //FIXME: This is only valid on "xor 1" applied to "i1" operators, but is unsound for any other bit-width. - xorExpr = expressions.makeConditional( + xorExpr = expressions.makeITE( expressions.makeEQ(left, expressions.makeGeneralZero(left.getType())), expressions.makeOne((IntegerType) left.getType()), expressions.makeZero((IntegerType) left.getType()) @@ -709,7 +709,7 @@ public Expression visitSelectInst(SelectInstContext ctx) { final Expression trueValue = visitTypeValue(ctx.typeValue(1)); final Expression falseValue = visitTypeValue(ctx.typeValue(2)); final Expression cast = expressions.makeBooleanCast(guard); - return assignToRegister(expressions.makeConditional(cast, trueValue, falseValue)); + return assignToRegister(expressions.makeITE(cast, trueValue, falseValue)); } @Override @@ -747,12 +747,12 @@ public Expression visitAtomicRMWInst(AtomicRMWInstContext ctx) { if (operator.equals("xchg")) { event = Llvm.newExchange(register, address, operand, mo); } else { - final IOpBin op = switch (operator) { - case "add" -> IOpBin.ADD; - case "sub" -> IOpBin.SUB; - case "and" -> IOpBin.AND; - case "or" -> IOpBin.OR; - case "xor" -> IOpBin.XOR; + final IntBinaryOp op = switch (operator) { + case "add" -> IntBinaryOp.ADD; + case "sub" -> IntBinaryOp.SUB; + case "and" -> IntBinaryOp.AND; + case "or" -> IntBinaryOp.OR; + case "xor" -> IntBinaryOp.XOR; //TODO nand, min, umin, max, umax, uinc_wrap, udec_wrap, fadd, fsub, fmax, fmin default -> throw new UnsupportedOperationException(String.format("Unknown atomic operand %s.", ctx.getText())); }; @@ -1024,7 +1024,7 @@ public Expression visitSelectExpr(SelectExprContext ctx) { final Expression trueValue = visitTypeConst(ctx.typeConst(1)); final Expression falseValue = visitTypeConst(ctx.typeConst(2)); final Expression cast = expressions.makeBooleanCast(guard); - return expressions.makeConditional(cast, trueValue, falseValue); + return expressions.makeITE(cast, trueValue, falseValue); } @Override @@ -1301,13 +1301,13 @@ public Expression makeNonDetOfType(Type type) { } return expressions.makeConstruct(elements); } else if (type instanceof IntegerType intType) { - final INonDet value = new INonDet(program.getConstants().size(), intType, true); + final NonDetInt value = new NonDetInt(program.getConstants().size(), intType, true); value.setMin(intType.getMinimumValue(true)); value.setMax(intType.getMaximumValue(true)); program.addConstant(value); return value; } else if (type instanceof BooleanType) { - return new BNonDet(types.getBooleanType()); + return new NonDetBool(types.getBooleanType()); } else { throw new UnsupportedOperationException("Cannot create non-deterministic value of type " + type); } @@ -1435,7 +1435,7 @@ private interface MdNode extends Expression { @Override default T accept(ExpressionVisitor visitor) { return null;} @Override - default IConst reduce() { throw new UnsupportedOperationException(); } + default IntLiteral reduce() { throw new UnsupportedOperationException(); } } private static final MdNode MD_NULL = new MdNode() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java index 82ada61e1e..546a27d871 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Function.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.IConst; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.FunctionType; import com.dat3m.dartagnan.expression.type.Type; @@ -189,7 +189,7 @@ public T accept(ExpressionVisitor visitor) { } @Override - public IConst reduce() { + public IntLiteral reduce() { throw new UnsupportedOperationException("Cannot reduce functions"); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java index 55dcb5cc8e..53b6f1133e 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/IRHelper.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program; -import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.expression.BoolLiteral; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.functions.AbortIf; @@ -31,7 +31,7 @@ public static Set bulkDelete(Set toBeDeleted) { */ public static boolean isAlwaysBranching(Event e) { return e instanceof Return - || e instanceof AbortIf abort && abort.getCondition() instanceof BConst b && b.getValue() + || e instanceof AbortIf abort && abort.getCondition() instanceof BoolLiteral b && b.getValue() || e instanceof CondJump jump && jump.isGoto(); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java index c0ce860333..a5179e4b46 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/Program.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program; import com.dat3m.dartagnan.configuration.Arch; -import com.dat3m.dartagnan.expression.INonDet; +import com.dat3m.dartagnan.expression.NonDetInt; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.memory.Memory; import com.dat3m.dartagnan.program.specification.AbstractAssert; @@ -19,7 +19,7 @@ public enum SourceLanguage { LITMUS, LLVM, SPV } private AbstractAssert filterSpec; // Acts like "assume" statements, filtering out executions private final List threads; private final List functions; - private final List constants = new ArrayList<>(); + private final List constants = new ArrayList<>(); private final Memory memory; private Arch arch; private int unrollingBound = 0; @@ -117,11 +117,11 @@ public Optional getFunctionByName(String name) { return functions.stream().filter(f -> f.getName().equals(name)).findFirst(); } - public void addConstant(INonDet constant) { + public void addConstant(NonDetInt constant) { constants.add(constant); } - public Collection getConstants() { + public Collection getConstants() { return Collections.unmodifiableCollection(constants); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java index e3d6d1e187..e59f0c51e2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/AndersenAliasAnalysis.java @@ -1,8 +1,8 @@ package com.dat3m.dartagnan.program.analysis.alias; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.IConst; -import com.dat3m.dartagnan.expression.IExprBin; +import com.dat3m.dartagnan.expression.IntBinaryExpr; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.MemoryEvent; @@ -22,7 +22,7 @@ import java.util.stream.Collectors; import java.util.stream.IntStream; -import static com.dat3m.dartagnan.expression.op.IOpBin.ADD; +import static com.dat3m.dartagnan.expression.op.IntBinaryOp.ADD; /** * Inclusion-based pointer analysis by Andersen. @@ -154,7 +154,7 @@ private void processRegs(Local e) { if (expr instanceof Register) { // r1 = r2 -> add edge r2 --> r1 addEdge(expr, register); - } else if (expr instanceof IExprBin iBin && iBin.getLHS() instanceof Register) { + } else if (expr instanceof IntBinaryExpr iBin && iBin.getLHS() instanceof Register) { addAllAddresses(register, maxAddressSet); variables.add(register); } else if (expr instanceof MemoryObject mem) { @@ -206,14 +206,13 @@ private void processResults(Local e) { addTarget(reg, new Location(mem, 0)); return; } - if (!(exp instanceof IExprBin iBin)) { + if (!(exp instanceof IntBinaryExpr iBin)) { return; } Expression base = iBin.getLHS(); if (base instanceof MemoryObject mem) { Expression rhs = iBin.getRHS(); - //FIXME Address extends IConst - if (rhs instanceof IConst ic) { + if (rhs instanceof IntLiteral ic) { addTarget(reg, new Location(mem, ic.getValueAsInt())); } else { addTargetArray(reg, (MemoryObject) base); @@ -225,9 +224,8 @@ private void processResults(Local e) { } //accept register2 = register1 + constant for (Location target : targets.getOrDefault(base, Set.of())) { - Expression rhs = ((IExprBin) exp).getRHS(); - //FIXME Address extends IConst - if (rhs instanceof IConst ic) { + Expression rhs = ((IntBinaryExpr) exp).getRHS(); + if (rhs instanceof IntLiteral ic) { int o = target.offset + ic.getValueAsInt(); if (o < target.base.size()) { addTarget(reg, new Location(target.base, o)); @@ -253,7 +251,7 @@ private void processResults(MemoryCoreEvent e) { addresses = ImmutableSet.of(addressConstant.location); } } - if (addresses.size() == 0) { + if (addresses.isEmpty()) { addresses = maxAddressSet; } eventAddressSpaceMap.put(e, ImmutableSet.copyOf(addresses)); @@ -269,15 +267,20 @@ private static final class Constant { * Tries to match an expression as a constant address. */ Constant(Expression x) { - if (x instanceof IConst) { - location = x instanceof MemoryObject mem ? new Location(mem, 0) : null; + if (x instanceof MemoryObject mem) { + location = new Location(mem, 0); failed = false; return; } - if (x instanceof IExprBin iBin && iBin.getOp() == ADD) { + if (x instanceof IntLiteral) { + location = null; + failed = false; + return; + } + if (x instanceof IntBinaryExpr iBin && iBin.getOp() == ADD) { Expression lhs = iBin.getLHS(); Expression rhs = iBin.getRHS(); - if (lhs instanceof MemoryObject mem && rhs instanceof IConst ic && !(rhs instanceof MemoryObject)) { + if (lhs instanceof MemoryObject mem && rhs instanceof IntLiteral ic) { location = new Location(mem, ic.getValueAsInt()); failed = false; return; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java index 50c2d4c8f1..ace3739627 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/alias/FieldSensitiveAndersen.java @@ -21,8 +21,8 @@ import java.math.BigInteger; import java.util.*; -import static com.dat3m.dartagnan.expression.op.IOpBin.*; -import static com.dat3m.dartagnan.expression.op.IOpUn.MINUS; +import static com.dat3m.dartagnan.expression.op.IntBinaryOp.*; +import static com.dat3m.dartagnan.expression.op.IntUnaryOp.MINUS; import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Verify.verify; import static java.util.stream.Collectors.toList; @@ -306,7 +306,7 @@ List> register() { } @Override - public Result visit(IExprBin x) { + public Result visit(IntBinaryExpr x) { Result l = x.getLHS().accept(this); Result r = x.getRHS().accept(this); if (l == null || r == null || x.getOp() == RSHIFT) { @@ -347,14 +347,14 @@ public Result visit(IExprBin x) { } @Override - public Result visit(IExprUn x) { + public Result visit(IntUnaryExpr x) { Result i = x.getInner().accept(this); return i == null ? null : x.getOp() != MINUS ? i : new Result(null, null, i.offset.negate(), i.alignment == 0 ? 1 : i.alignment); } @Override - public Result visit(IfExpr x) { + public Result visit(ITEExpr x) { x.getTrueBranch().accept(this); x.getFalseBranch().accept(this); return null; @@ -373,7 +373,7 @@ public Result visit(Register r) { } @Override - public Result visit(IValue v) { + public Result visit(IntLiteral v) { return new Result(null, null, v.getValue(), 0); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index 30fcfeb28a..d14e31a6eb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.program.event; -import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.expression.BoolLiteral; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.type.FunctionType; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; @@ -190,7 +190,7 @@ public static CondJump newJump(Expression cond, Label target) { } public static CondJump newJumpUnless(Expression cond, Label target) { - if (cond instanceof BConst constant && !constant.getValue()) { + if (cond instanceof BoolLiteral constant && !constant.getValue()) { return newGoto(target); } return new CondJump(expressions.makeNot(cond), target); @@ -344,12 +344,12 @@ public static AtomicCmpXchg newCompareExchange(Register register, Expression add return newCompareExchange(register, address, expectedAddr, desiredValue, mo, false); } - public static AtomicFetchOp newFetchOp(Register register, Expression address, Expression value, IOpBin op, String mo) { + public static AtomicFetchOp newFetchOp(Register register, Expression address, Expression value, IntBinaryOp op, String mo) { return new AtomicFetchOp(register, address, op, value, mo); } public static AtomicFetchOp newFADD(Register register, Expression address, Expression value, String mo) { - return newFetchOp(register, address, value, IOpBin.ADD, mo); + return newFetchOp(register, address, value, IntBinaryOp.ADD, mo); } public static AtomicFetchOp newIncrement(Register register, Expression address, String mo) { @@ -357,7 +357,7 @@ public static AtomicFetchOp newIncrement(Register register, Expression address, throw new IllegalArgumentException( String.format("Non-integer type %s for increment operation.", register.getType())); } - return newFetchOp(register, address, expressions.makeOne(integerType), IOpBin.ADD, mo); + return newFetchOp(register, address, expressions.makeOne(integerType), IntBinaryOp.ADD, mo); } public static AtomicLoad newLoad(Register register, Expression address, String mo) { @@ -404,7 +404,7 @@ public static LlvmCmpXchg newCompareExchange(Register oldValueRegister, Register return newCompareExchange(oldValueRegister, cmpRegister, address, expectedAddr, desiredValue, mo, false); } - public static LlvmRMW newRMW(Register register, Expression address, Expression value, IOpBin op, String mo) { + public static LlvmRMW newRMW(Register register, Expression address, Expression value, IntBinaryOp op, String mo) { return new LlvmRMW(register, address, op, value, mo); } @@ -523,19 +523,19 @@ public static LKMMCmpXchg newRMWCompareExchange(Expression address, Register reg return new LKMMCmpXchg(register, address, cmp, value, mo); } - public static LKMMFetchOp newRMWFetchOp(Expression address, Register register, Expression value, IOpBin op, String mo) { + public static LKMMFetchOp newRMWFetchOp(Expression address, Register register, Expression value, IntBinaryOp op, String mo) { return new LKMMFetchOp(register, address, op, value, mo); } - public static LKMMOpNoReturn newRMWOp(Expression address, Expression value, IOpBin op) { + public static LKMMOpNoReturn newRMWOp(Expression address, Expression value, IntBinaryOp op) { return new LKMMOpNoReturn(address, op, value); } - public static LKMMOpAndTest newRMWOpAndTest(Expression address, Register register, Expression value, IOpBin op) { + public static LKMMOpAndTest newRMWOpAndTest(Expression address, Register register, Expression value, IntBinaryOp op) { return new LKMMOpAndTest(register, address, op, value); } - public static LKMMOpReturn newRMWOpReturn(Expression address, Register register, Expression value, IOpBin op, String mo) { + public static LKMMOpReturn newRMWOpReturn(Expression address, Register register, Expression value, IntBinaryOp op, String mo) { return new LKMMOpReturn(register, address, op, value, mo); } @@ -692,7 +692,7 @@ public static class PTX { private PTX() {} public static PTXAtomOp newAtomOp(Expression address, Register register, Expression value, - IOpBin op, String mo, String scope) { + IntBinaryOp op, String mo, String scope) { // PTX (currently) only generates memory orders ACQ_REL and RLX for atom. PTXAtomOp atom = new PTXAtomOp(register, address, op, value, mo); atom.addTags(scope); @@ -714,7 +714,7 @@ public static PTXAtomExch newAtomExch(Expression address, Register register, } public static PTXRedOp newRedOp(Expression address, Expression value, - IOpBin op, String mo, String scope) { + IntBinaryOp op, String mo, String scope) { // PTX (currently) only generates memory orders ACQ_REL and RLX for red. PTXRedOp red = new PTXRedOp(address, value, op, mo); red.addTags(scope); @@ -743,7 +743,7 @@ public static VulkanRMW newRMW(Expression address, Register register, Expression } public static VulkanRMWOp newRMWOp(Expression address, Register register, Expression value, - IOpBin op, String mo, String scope) { + IntBinaryOp op, String mo, String scope) { return new VulkanRMWOp(register, address, op, value, mo, scope); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java index 9d4a4b9b6f..e0a4389645 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXAtomOp.java @@ -1,14 +1,14 @@ package com.dat3m.dartagnan.program.event.arch.ptx; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; public class PTXAtomOp extends RMWOpResultBase { - public PTXAtomOp(Register register, Expression address, IOpBin op, Expression operand, String mo) { + public PTXAtomOp(Register register, Expression address, IntBinaryOp op, Expression operand, String mo) { super(register, address, op, operand, mo); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java index 4663f6d676..9eb9f5a2d4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/ptx/PTXRedOp.java @@ -1,13 +1,13 @@ package com.dat3m.dartagnan.program.event.arch.ptx; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpBase; public class PTXRedOp extends RMWOpBase { - public PTXRedOp(Expression address, Expression value, IOpBin op, String mo) { + public PTXRedOp(Expression address, Expression value, IntBinaryOp op, String mo) { super(address, op, value, mo); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java index 74ed76f7c5..0c6d6808a9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/arch/vulkan/VulkanRMWOp.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.arch.vulkan; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; @@ -9,7 +9,7 @@ public class VulkanRMWOp extends RMWOpResultBase { - public VulkanRMWOp(Register register, Expression address, IOpBin op, Expression operand, String mo, String scope) { + public VulkanRMWOp(Register register, Expression address, IntBinaryOp op, Expression operand, String mo, String scope) { super(register, address, op, operand, mo); this.addTags(Tag.Vulkan.ATOM, scope); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpBase.java index e6cee622f2..682b853180 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpBase.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.common; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.MemoryAccess; @@ -16,10 +16,10 @@ @NoInterface public abstract class RMWOpBase extends SingleAccessMemoryEvent { - protected IOpBin operator; + protected IntBinaryOp operator; protected Expression operand; - protected RMWOpBase(Expression address, IOpBin operator, Expression operand, String mo) { + protected RMWOpBase(Expression address, IntBinaryOp operator, Expression operand, String mo) { super(address, operand.getType(), mo); this.operator = operator; this.operand = operand; @@ -35,8 +35,8 @@ protected RMWOpBase(RMWOpBase other) { public Expression getOperand() { return operand; } public void setOperand(Expression operand) { this.operand = operand; } - public IOpBin getOperator() { return this.operator; } - public void setOperator(IOpBin operator) { this.operator = operator; } + public IntBinaryOp getOperator() { return this.operator; } + public void setOperator(IntBinaryOp operator) { this.operator = operator; } @Override public void transformExpressions(ExpressionVisitor exprTransformer) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java index 2bf35642b5..20204fd276 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/common/RMWOpResultBase.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.common; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.RegWriter; @@ -14,7 +14,7 @@ public abstract class RMWOpResultBase extends RMWOpBase implements RegWriter { protected Register resultRegister; - protected RMWOpResultBase(Register register, Expression address, IOpBin operator, Expression operand, String mo) { + protected RMWOpResultBase(Register register, Expression address, IntBinaryOp operator, Expression operand, String mo) { super(address, operator, operand, mo); this.resultRegister = register; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java index 557c928266..c2483ad49c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/CondJump.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.event.core; -import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.expression.BoolLiteral; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.BooleanType; @@ -35,11 +35,11 @@ protected CondJump(CondJump other) { } public boolean isGoto() { - return guard instanceof BConst constant && constant.getValue(); + return guard instanceof BoolLiteral constant && constant.getValue(); } public boolean isDead() { - return guard instanceof BConst constant && !constant.getValue(); + return guard instanceof BoolLiteral constant && !constant.getValue(); } public Label getLabel() { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java index 228ceba3f7..e7d1785e30 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/Alloc.java @@ -3,7 +3,7 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; @@ -58,14 +58,14 @@ protected Alloc(Alloc other) { public Expression getArraySize() { return arraySize; } public boolean isHeapAllocation() { return isHeapAllocation; } - public boolean isSimpleAllocation() { return (arraySize instanceof IValue size && size.isOne()); } + public boolean isSimpleAllocation() { return (arraySize instanceof IntLiteral size && size.isOne()); } public boolean isArrayAllocation() { return !isSimpleAllocation(); } public Expression getAllocationSize() { final ExpressionFactory expressions = ExpressionFactory.getInstance(); final TypeFactory types = TypeFactory.getInstance(); final Expression allocationSize; - if (arraySize instanceof IValue value) { + if (arraySize instanceof IntLiteral value) { allocationSize = expressions.makeValue( BigInteger.valueOf(types.getMemorySizeInBytes(allocationType)).multiply(value.getValue()), types.getArchType() diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java index f1b6df6ac9..f41e99defe 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/catomic/AtomicFetchOp.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.catomic; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; @@ -9,7 +9,7 @@ public class AtomicFetchOp extends RMWOpResultBase { - public AtomicFetchOp(Register register, Expression address, IOpBin operator, Expression operand, String mo) { + public AtomicFetchOp(Register register, Expression address, IntBinaryOp operator, Expression operand, String mo) { super(register, address, operator, operand, mo); Preconditions.checkArgument(!mo.isEmpty(), "Atomic events cannot have empty memory order"); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java index 276e4bfd2a..a33eb93175 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMFetchOp.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.linux; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; @@ -9,7 +9,7 @@ public class LKMMFetchOp extends RMWOpResultBase { - public LKMMFetchOp(Register register, Expression address, IOpBin op, Expression operand, String mo) { + public LKMMFetchOp(Register register, Expression address, IntBinaryOp op, Expression operand, String mo) { super(register, address, op, operand, mo); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java index 3e5b1c4319..ab5f30db2d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpAndTest.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.linux; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; @@ -9,7 +9,7 @@ public class LKMMOpAndTest extends RMWOpResultBase { - public LKMMOpAndTest(Register register, Expression address, IOpBin op, Expression operand) { + public LKMMOpAndTest(Register register, Expression address, IntBinaryOp op, Expression operand) { super(register, address, op, operand, Tag.Linux.MO_MB); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java index 3b71319977..3d8d0231d8 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpNoReturn.java @@ -1,14 +1,14 @@ package com.dat3m.dartagnan.program.event.lang.linux; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.program.event.common.RMWOpBase; public class LKMMOpNoReturn extends RMWOpBase { - public LKMMOpNoReturn(Expression address, IOpBin operator, Expression operand) { + public LKMMOpNoReturn(Expression address, IntBinaryOp operator, Expression operand) { super(address, operator, operand, Tag.Linux.MO_ONCE); addTags(Tag.Linux.NORETURN); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java index 604ada0356..dd5af72adc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/linux/LKMMOpReturn.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.linux; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.Tag; @@ -9,7 +9,7 @@ public class LKMMOpReturn extends RMWOpResultBase { - public LKMMOpReturn(Register register, Expression address, IOpBin op, Expression operand, String mo) { + public LKMMOpReturn(Register register, Expression address, IntBinaryOp op, Expression operand, String mo) { super(register, address, op, operand, mo); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java index 3577ed3269..76e46fc78f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/lang/llvm/LlvmRMW.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.event.lang.llvm; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.program.Register; import com.dat3m.dartagnan.program.event.EventVisitor; import com.dat3m.dartagnan.program.event.common.RMWOpResultBase; @@ -9,7 +9,7 @@ public class LlvmRMW extends RMWOpResultBase { - public LlvmRMW(Register register, Expression address, IOpBin op, Expression operand, String mo) { + public LlvmRMW(Register register, Expression address, IntBinaryOp op, Expression operand, String mo) { super(register, address, op, operand, mo); Preconditions.checkArgument(!mo.isEmpty(), "LLVM events cannot have empty memory order"); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java index 9827f94f7e..43fd9eb346 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/Location.java @@ -1,10 +1,10 @@ package com.dat3m.dartagnan.program.memory; -import com.dat3m.dartagnan.expression.IExpr; +import com.dat3m.dartagnan.expression.IntExpr; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.TypeFactory; -public class Location extends IExpr { +public class Location extends IntExpr { private final String name; private final MemoryObject base; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java index 4a809f37bf..c5f95b52d9 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/memory/MemoryObject.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IConst; +import com.dat3m.dartagnan.expression.IntExpr; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.TypeFactory; @@ -16,10 +16,10 @@ /** * Associated with an array of memory locations. */ -public class MemoryObject extends IConst { +public class MemoryObject extends IntExpr { private final int index; - private int size; + private final int size; BigInteger address; private String cVar; private boolean isThreadLocal; @@ -92,17 +92,6 @@ public void setInitialValue(int offset, Expression value) { initialValues.put(offset, value); } - /** - * Updates the initial value at a certain field of this array. - * - * @param offset Non-negative number of fields before the target. - * @param value New value to be read at the start of each execution. - */ - public void appendInitialValue(int offset, Expression value) { - checkArgument(offset >= 0, "array index out of bounds"); - initialValues.put(offset, value); - } - public boolean isAtomic() { return atomic; } @@ -110,11 +99,6 @@ public void markAsAtomic() { this.atomic = true; } - @Override - public BigInteger getValue() { - return address != null ? address : BigInteger.valueOf(index); - } - @Override public String toString() { return cVar != null ? cVar : ("&mem" + index); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java index 227eff4fee..9183414722 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/GEPToAddition.java @@ -4,7 +4,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; import com.dat3m.dartagnan.expression.GEPExpression; -import com.dat3m.dartagnan.expression.IConst; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.processing.ExprTransformer; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.program.Function; @@ -49,7 +49,7 @@ public Expression visit(GEPExpression getElementPointer) { Type type = getElementPointer.getIndexingType(); Expression result = getElementPointer.getBaseExpression().accept(this); final List offsets = getElementPointer.getOffsetExpressions(); - assert offsets.size() > 0; + assert !offsets.isEmpty(); result = expressions.makeADD(result, expressions.makeMUL( expressions.makeValue(types.getMemorySizeInBytes(type), archType), @@ -67,7 +67,7 @@ public Expression visit(GEPExpression getElementPointer) { if (!(type instanceof AggregateType aggregateType)) { throw new MalformedProgramException(String.format("GEP from non-compound type %s.", type)); } - if (!(offset instanceof IConst constant)) { + if (!(offset instanceof IntLiteral constant)) { throw new MalformedProgramException( String.format("Non-constant field index %s for aggregate of type %s.", offset, type)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java index 8a4aea81a6..06200fb15a 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Intrinsics.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.expression.*; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.type.*; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Program; @@ -508,7 +508,7 @@ private List inlinePthreadCondTimedwait(FunctionCall call) { //final Expression condAddress = call.getArguments().get(0); final Expression lockAddress = call.getArguments().get(1); //final Expression timespec = call.getArguments().get(2); - final var errorValue = new INonDet(constantId++, (IntegerType) errorRegister.getType(), true); + final var errorValue = new NonDetInt(constantId++, (IntegerType) errorRegister.getType(), true); errorValue.setMin(BigInteger.ZERO); call.getFunction().getProgram().addConstant(errorValue); return List.of( @@ -727,7 +727,7 @@ private List inlinePthreadRwlockTryWrlock(FunctionCall call) { final Register errorRegister = getResultRegisterAndCheckArguments(1, call); final Expression lockAddress = call.getArguments().get(0); final Register successRegister = call.getFunction().newRegister(types.getBooleanType()); - final var error = new INonDet(constantId++, (IntegerType) errorRegister.getType(), true); + final var error = new NonDetInt(constantId++, (IntegerType) errorRegister.getType(), true); call.getFunction().getProgram().addConstant(error); final Expression success = expressions.makeGeneralZero(errorRegister.getType()); return List.of( @@ -756,7 +756,7 @@ private List inlinePthreadRwlockRdlock(FunctionCall call) { final Register oldValueRegister = call.getFunction().newRegister(getRwlockDatatype()); final Register successRegister = call.getFunction().newRegister(types.getBooleanType()); final Expression lockAddress = call.getArguments().get(0); - final var expected = new INonDet(constantId++, getRwlockDatatype(), true); + final var expected = new NonDetInt(constantId++, getRwlockDatatype(), true); call.getFunction().getProgram().addConstant(expected); return List.of( // Expect any other value than write-locked. @@ -777,9 +777,9 @@ private List inlinePthreadRwlockTryRdlock(FunctionCall call) { final Register oldValueRegister = call.getFunction().newRegister(getRwlockDatatype()); final Register successRegister = call.getFunction().newRegister(types.getBooleanType()); final Expression lockAddress = call.getArguments().get(0); - final var expected = new INonDet(constantId++, getRwlockDatatype(), true); + final var expected = new NonDetInt(constantId++, getRwlockDatatype(), true); call.getFunction().getProgram().addConstant(expected); - final var error = new INonDet(constantId++, (IntegerType) errorRegister.getType(), true); + final var error = new NonDetInt(constantId++, (IntegerType) errorRegister.getType(), true); call.getFunction().getProgram().addConstant(error); final Expression success = expressions.makeGeneralZero(errorRegister.getType()); return List.of( @@ -801,7 +801,7 @@ private Event newRwlockTryRdlock(FunctionCall call, Register oldValueRegister, R successRegister, lockAddress, expected, - expressions.makeConditional( + expressions.makeITE( expressions.makeEQ(expected, getRwlockUnlockedValue()), expressions.makeValue(BigInteger.TWO, getRwlockDatatype()), expressions.makeADD(expected, expressions.makeOne(getRwlockDatatype())) @@ -815,16 +815,16 @@ private List inlinePthreadRwlockUnlock(FunctionCall call) { final Register errorRegister = getResultRegisterAndCheckArguments(1, call); final Register oldValueRegister = call.getFunction().newRegister(getRwlockDatatype()); final Expression lockAddress = call.getArguments().get(0); - final var decrement = new INonDet(constantId++, getRwlockDatatype(), true); + final var decrement = new NonDetInt(constantId++, getRwlockDatatype(), true); call.getFunction().getProgram().addConstant(decrement); final Expression one = expressions.makeOne(getRwlockDatatype()); final Expression two = expressions.makeValue(BigInteger.TWO, getRwlockDatatype()); final Expression lastReader = expressions.makeEQ(oldValueRegister, two); - final Expression properDecrement = expressions.makeConditional(lastReader, two, one); + final Expression properDecrement = expressions.makeITE(lastReader, two, one); //TODO does not recognize whether the calling thread is allowed to unlock return List.of( // decreases the lock value by 1, if not the last reader, or else 2. - EventFactory.Llvm.newRMW(oldValueRegister, lockAddress, decrement, IOpBin.SUB, Tag.C11.MO_RELEASE), + EventFactory.Llvm.newRMW(oldValueRegister, lockAddress, decrement, IntBinaryOp.SUB, Tag.C11.MO_RELEASE), EventFactory.newAssume(expressions.makeEQ(decrement, properDecrement)), assignSuccess(errorRegister) ); @@ -834,13 +834,13 @@ private IntegerType getRwlockDatatype() { return types.getArchType(); } - private IValue getRwlockUnlockedValue() { + private IntLiteral getRwlockUnlockedValue() { //FIXME this assumes that the lock is initialized with pthread_rwlock_init, // but some programs may explicitly initialize it with other platform-dependent values. return expressions.makeZero(getRwlockDatatype()); } - private IValue getRwlockWriteLockedValue() { + private IntLiteral getRwlockWriteLockedValue() { return expressions.makeOne(getRwlockDatatype()); } @@ -985,7 +985,7 @@ private List inlineLLVMCtpop(ValueFunctionCall call) { final Expression testBit = expressions.makeEQ(expressions.makeAND(input, testMask), testMask); replacement.add( - EventFactory.newLocal(resultReg, expressions.makeConditional(testBit, increment, resultReg)) + EventFactory.newLocal(resultReg, expressions.makeITE(testBit, increment, resultReg)) ); } @@ -1001,7 +1001,7 @@ private List inlineLLVMMinMax(ValueFunctionCall call) { final boolean signed = name.startsWith("llvm.smax.") || name.startsWith("llvm.smin."); final boolean isMax = name.startsWith("llvm.smax.") || name.startsWith("llvm.umax."); final Expression isLess = expressions.makeLT(left, right, signed); - final Expression result = expressions.makeConditional(isLess, isMax ? right : left, isMax ? left : right); + final Expression result = expressions.makeITE(isLess, isMax ? right : left, isMax ? left : right); return List.of(EventFactory.newLocal(call.getResultRegister(), result)); } @@ -1038,14 +1038,14 @@ private List inlineLLVMSaturatedSub(ValueFunctionCall call) { ); return List.of( - EventFactory.newLocal(resultReg, expressions.makeConditional(leftIsNegative, min, max)), - EventFactory.newLocal(resultReg, expressions.makeConditional(noOverflow, expressions.makeSUB(x, y), resultReg)) + EventFactory.newLocal(resultReg, expressions.makeITE(leftIsNegative, min, max)), + EventFactory.newLocal(resultReg, expressions.makeITE(noOverflow, expressions.makeSUB(x, y), resultReg)) ); } else { final Expression noUnderflow = expressions.makeGT(x, y, false); final Expression zero = expressions.makeZero(type); return List.of( - EventFactory.newLocal(resultReg, expressions.makeConditional(noUnderflow, expressions.makeSUB(x, y), zero)) + EventFactory.newLocal(resultReg, expressions.makeITE(noUnderflow, expressions.makeSUB(x, y), zero)) ); } } @@ -1081,24 +1081,24 @@ private List inlineLLVMSaturatedAdd(ValueFunctionCall call) { ); return List.of( - EventFactory.newLocal(resultReg, expressions.makeConditional(leftIsNegative, min, max)), - EventFactory.newLocal(resultReg, expressions.makeConditional(noOverflow, expressions.makeADD(x, y), resultReg)) + EventFactory.newLocal(resultReg, expressions.makeITE(leftIsNegative, min, max)), + EventFactory.newLocal(resultReg, expressions.makeITE(noOverflow, expressions.makeADD(x, y), resultReg)) ); } private List inlineLLVMSAddWithOverflow(ValueFunctionCall call) { - return inlineLLVMSOpWithOverflow(call, IOpBin.ADD); + return inlineLLVMSOpWithOverflow(call, IntBinaryOp.ADD); } private List inlineLLVMSSubWithOverflow(ValueFunctionCall call) { - return inlineLLVMSOpWithOverflow(call, IOpBin.SUB); + return inlineLLVMSOpWithOverflow(call, IntBinaryOp.SUB); } private List inlineLLVMSMulWithOverflow(ValueFunctionCall call) { - return inlineLLVMSOpWithOverflow(call, IOpBin.MUL); + return inlineLLVMSOpWithOverflow(call, IntBinaryOp.MUL); } - private List inlineLLVMSOpWithOverflow(ValueFunctionCall call, IOpBin op) { + private List inlineLLVMSOpWithOverflow(ValueFunctionCall call, IntBinaryOp op) { final Register resultReg = call.getResultRegister(); final List arguments = call.getArguments(); final Expression x = arguments.get(0); @@ -1158,53 +1158,53 @@ private List handleLKMMIntrinsic(FunctionCall call) { final Expression p3 = args.size() > 3 ? args.get(3) : null; final String mo; - final IOpBin op; + final IntBinaryOp op; final List result = new ArrayList<>(); switch (call.getCalledFunction().getName()) { case "__LKMM_LOAD" -> { - checkArgument(p1 instanceof IConst, "No support for variable memory order."); - mo = Tag.Linux.intToMo(((IConst) p1).getValueAsInt()); + checkArgument(p1 instanceof IntLiteral, "No support for variable memory order."); + mo = Tag.Linux.intToMo(((IntLiteral) p1).getValueAsInt()); result.add(EventFactory.Linux.newLKMMLoad(reg, p0, mo)); } case "__LKMM_STORE" -> { - checkArgument(p2 instanceof IConst, "No support for variable memory order."); - mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); + checkArgument(p2 instanceof IntLiteral, "No support for variable memory order."); + mo = Tag.Linux.intToMo(((IntLiteral) p2).getValueAsInt()); result.add(EventFactory.Linux.newLKMMStore(p0, p1, mo.equals(Tag.Linux.MO_MB) ? Tag.Linux.MO_ONCE : mo)); if (mo.equals(Tag.Linux.MO_MB)) { result.add(EventFactory.Linux.newMemoryBarrier()); } } case "__LKMM_XCHG" -> { - checkArgument(p2 instanceof IConst, "No support for variable memory order."); - mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); + checkArgument(p2 instanceof IntLiteral, "No support for variable memory order."); + mo = Tag.Linux.intToMo(((IntLiteral) p2).getValueAsInt()); result.add(EventFactory.Linux.newRMWExchange(p0, reg, p1, mo)); } case "__LKMM_CMPXCHG" -> { - checkArgument(p3 instanceof IConst, "No support for variable memory order."); - mo = Tag.Linux.intToMo(((IConst) p3).getValueAsInt()); + checkArgument(p3 instanceof IntLiteral, "No support for variable memory order."); + mo = Tag.Linux.intToMo(((IntLiteral) p3).getValueAsInt()); result.add(EventFactory.Linux.newRMWCompareExchange(p0, reg, p1, p2, mo)); } case "__LKMM_ATOMIC_FETCH_OP" -> { - checkArgument(p2 instanceof IConst, "No support for variable memory order."); - mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); - checkArgument(p3 instanceof IConst, "No support for variable operator."); - op = IOpBin.intToOp(((IConst) p3).getValueAsInt()); + checkArgument(p2 instanceof IntLiteral, "No support for variable memory order."); + mo = Tag.Linux.intToMo(((IntLiteral) p2).getValueAsInt()); + checkArgument(p3 instanceof IntLiteral, "No support for variable operator."); + op = IntBinaryOp.intToOp(((IntLiteral) p3).getValueAsInt()); result.add(EventFactory.Linux.newRMWFetchOp(p0, reg, p1, op, mo)); } case "__LKMM_ATOMIC_OP_RETURN" -> { - checkArgument(p2 instanceof IConst, "No support for variable memory order."); - mo = Tag.Linux.intToMo(((IConst) p2).getValueAsInt()); - checkArgument(p3 instanceof IConst, "No support for variable operator."); - op = IOpBin.intToOp(((IConst) p3).getValueAsInt()); + checkArgument(p2 instanceof IntLiteral, "No support for variable memory order."); + mo = Tag.Linux.intToMo(((IntLiteral) p2).getValueAsInt()); + checkArgument(p3 instanceof IntLiteral, "No support for variable operator."); + op = IntBinaryOp.intToOp(((IntLiteral) p3).getValueAsInt()); result.add(EventFactory.Linux.newRMWOpReturn(p0, reg, p1, op, mo)); } case "__LKMM_ATOMIC_OP" -> { - checkArgument(p2 instanceof IConst, "No support for variable operator."); - op = IOpBin.intToOp(((IConst) p2).getValueAsInt()); + checkArgument(p2 instanceof IntLiteral, "No support for variable operator."); + op = IntBinaryOp.intToOp(((IntLiteral) p2).getValueAsInt()); result.add(EventFactory.Linux.newRMWOp(p0, p1, op)); } case "__LKMM_FENCE" -> { - String fence = Tag.Linux.intToMo(((IConst) p0).getValueAsInt()); + String fence = Tag.Linux.intToMo(((IntLiteral) p0).getValueAsInt()); result.add(EventFactory.Linux.newLKMMFence(fence)); } case "__LKMM_SPIN_LOCK" -> { @@ -1255,7 +1255,7 @@ private List inlineNonDet(FunctionCall call) { // Nondeterministic booleans if (suffix.equals("bool")) { BooleanType booleanType = types.getBooleanType(); - var nondeterministicExpression = new BNonDet(booleanType); + var nondeterministicExpression = new NonDetBool(booleanType); Expression cast = expressions.makeCast(nondeterministicExpression, register.getType()); return List.of(EventFactory.newLocal(register, cast)); } @@ -1286,7 +1286,7 @@ private List inlineNonDet(FunctionCall call) { if (!(register.getType() instanceof IntegerType type)) { throw new MalformedProgramException(String.format("Non-integer result register %s.", register)); } - var expression = new INonDet(constantId++, type, signed); + var expression = new NonDetInt(constantId++, type, signed); expression.setMin(min); expression.setMax(max); call.getFunction().getProgram().addConstant(expression); @@ -1304,7 +1304,7 @@ private List inlineMemCpy(FunctionCall call) { final Expression countExpr = call.getArguments().get(2); // final Expression isVolatile = call.getArguments.get(3) // LLVM's memcpy has an extra argument - if (!(countExpr instanceof IValue countValue)) { + if (!(countExpr instanceof IntLiteral countValue)) { final String error = "Cannot handle memcpy with dynamic count argument: " + call; throw new UnsupportedOperationException(error); } @@ -1338,7 +1338,7 @@ private List inlineMemCmp(FunctionCall call) { final Expression numExpr = call.getArguments().get(2); final Register returnReg = ((ValueFunctionCall)call).getResultRegister(); - if (!(numExpr instanceof IValue numValue)) { + if (!(numExpr instanceof IntLiteral numValue)) { final String error = "Cannot handle memcmp with dynamic num argument: " + call; throw new UnsupportedOperationException(error); } @@ -1382,11 +1382,11 @@ private List inlineMemSet(FunctionCall call) { logger.warn("Treating call to \"__memset_chk\" as call to \"memset\": skipping bound checks."); } - if (!(countExpr instanceof IValue countValue)) { + if (!(countExpr instanceof IntLiteral countValue)) { final String error = "Cannot handle memset with dynamic count argument: " + call; throw new UnsupportedOperationException(error); } - if (!(fillExpr instanceof IValue fillValue && fillValue.isZero())) { + if (!(fillExpr instanceof IntLiteral fillValue && fillValue.isZero())) { //FIXME: We can soundly handle only 0 (and possibly -1) because the concatenation of // byte-sized 0's results in 0's of larger types. This makes the value robust against mixed-sized accesses. final String error = "Cannot handle memset with non-zero fill argument: " + call; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java index 0b3b4cc350..925da6c4cc 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/MemToReg.java @@ -2,9 +2,9 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IExprBin; -import com.dat3m.dartagnan.expression.IValue; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.IntBinaryExpr; +import com.dat3m.dartagnan.expression.IntLiteral; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.type.BooleanType; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.Type; @@ -120,7 +120,7 @@ private void promoteAll(Function function, Matcher matcher) { } private List getPrimitiveReplacementTypes(Alloc allocation) { - if (!(allocation.getArraySize() instanceof IValue sizeExpression)) { + if (!(allocation.getArraySize() instanceof IntLiteral sizeExpression)) { return null; } final int size = sizeExpression.getValueAsInt(); @@ -329,9 +329,9 @@ private void publishRegisters(Set registers) { private RegisterOffset matchGEP(Expression expression) { int sum = 0; while (!(expression instanceof Register register)) { - if (!(expression instanceof IExprBin bin) || - bin.getOp() != IOpBin.ADD || - !(bin.getRHS() instanceof IValue offset)) { + if (!(expression instanceof IntBinaryExpr bin) || + bin.getOp() != IntBinaryOp.ADD || + !(bin.getRHS() instanceof IntLiteral offset)) { return null; } sum += offset.getValueAsInt(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java index f1e3b57b38..3c9ed3e2ce 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/NaiveDevirtualisation.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.processing.ExprTransformer; import com.dat3m.dartagnan.expression.processing.ExpressionInspector; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; @@ -102,7 +102,7 @@ private void findAndTransformAddressTakenFunctions( } } - private boolean assignAddressToFunction(Function func, Map func2AddressMap) { + private boolean assignAddressToFunction(Function func, Map func2AddressMap) { final IntegerType ptrType = TypeFactory.getInstance().getArchType(); final ExpressionFactory expressions = ExpressionFactory.getInstance(); if (!func2AddressMap.containsKey(func)) { @@ -130,7 +130,7 @@ private void applyTransformerToEvent(Event e, ExpressionVisitor tran } } - private void devirtualise(Function function, Map func2AddressMap) { + private void devirtualise(Function function, Map func2AddressMap) { final ExpressionFactory expressions = ExpressionFactory.getInstance(); int devirtCounter = 0; @@ -158,7 +158,7 @@ private void devirtualise(Function function, Map func2AddressM final Expression funcPtr = getFunctionPointer(call); // Construct call table for (Function possibleTarget : possibleTargets) { - final IValue targetAddress = func2AddressMap.get(possibleTarget); + final IntLiteral targetAddress = func2AddressMap.get(possibleTarget); final Label caseLabel = EventFactory.newLabel(String.format("__Ldevirt_%s#%s", targetAddress.getValue(), devirtCounter)); final CondJump caseJump = EventFactory.newJump(expressions.makeEQ(funcPtr, targetAddress), caseLabel); caseLabels.add(caseLabel); @@ -193,7 +193,7 @@ private boolean needsDevirtualization(FunctionCall call) { && !(call.getArguments().get(2) instanceof Function)); } - private List getPossibleTargets(FunctionCall call, Map func2AddressMap) { + private List getPossibleTargets(FunctionCall call, Map func2AddressMap) { final List possibleTargets; if (!call.isDirectCall()) { possibleTargets = func2AddressMap.keySet().stream() @@ -259,7 +259,7 @@ public Expression visit(Function function) { private static class FunctionToAddressTransformer extends ExprTransformer { - private final Map func2AddressMap = new HashMap<>(); + private final Map func2AddressMap = new HashMap<>(); @Override public Expression visit(Function function) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java index ff6c98bcb0..47960554c3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/RemoveDeadCondJumps.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.processing; import com.dat3m.dartagnan.expression.Atom; -import com.dat3m.dartagnan.expression.BExprUn; +import com.dat3m.dartagnan.expression.BoolUnaryExpr; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.event.Event; import com.dat3m.dartagnan.program.event.Tag; @@ -118,8 +118,8 @@ private boolean mutuallyExclusiveIfs(CondJump jump, Event e) { if (!(e instanceof CondJump other)) { return false; } - if (jump.getGuard() instanceof BExprUn jumpGuard && jumpGuard.getInner().equals(other.getGuard()) - || other.getGuard() instanceof BExprUn otherGuard && otherGuard.getInner().equals(jump.getGuard())) { + if (jump.getGuard() instanceof BoolUnaryExpr jumpGuard && jumpGuard.getInner().equals(other.getGuard()) + || other.getGuard() instanceof BoolUnaryExpr otherGuard && otherGuard.getInner().equals(jump.getGuard())) { return true; } if (jump.getGuard() instanceof Atom a1 && other.getGuard() instanceof Atom a2) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java index 39d813ff80..7031ec1210 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ResolveLLVMObjectSizeCalls.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.processing; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.event.Event; @@ -45,9 +45,9 @@ public void run(Function function) { private void resolveObjectSizeCall(ValueFunctionCall call) { //final Expression ptr = call.getArguments().get(0); - final IValue zeroIfUnknown = (IValue)call.getArguments().get(1); // else -1 if unknown - //final IValue nullIsUnknown = (IValue)call.getArguments().get(2); - //final IValue isDynamic = (IValue) call.getArguments().get(3); // Meaning of this is unclear + final IntLiteral zeroIfUnknown = (IntLiteral)call.getArguments().get(1); // else -1 if unknown + //final IntLiteral nullIsUnknown = (IntLiteral)call.getArguments().get(2); + //final IntLiteral isDynamic = (IntLiteral) call.getArguments().get(3); // Meaning of this is unclear // TODO: We treat all pointers as unknown for now. final ExpressionFactory exprs = ExpressionFactory.getInstance(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java index c48e06011c..36598c0c63 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/Simplifier.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.processing; -import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.expression.BoolLiteral; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.event.Event; @@ -63,7 +63,7 @@ private boolean simplifyJump(CondJump jump) { final Label jumpTarget = jump.getLabel(); final Event successor = jump.getSuccessor(); final Expression guard = jump.getGuard(); - if(jumpTarget.equals(successor) && guard instanceof BConst) { + if(jumpTarget.equals(successor) && guard instanceof BoolLiteral) { return jump.tryDelete(); } return false; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java index 17dc3f6e30..c6d7972ba7 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SparseConditionalConstantPropagation.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.program.processing; import com.dat3m.dartagnan.expression.*; -import com.dat3m.dartagnan.expression.op.IOpBin; +import com.dat3m.dartagnan.expression.op.IntBinaryOp; import com.dat3m.dartagnan.expression.processing.ExprTransformer; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.IRHelper; @@ -14,6 +14,7 @@ import com.dat3m.dartagnan.program.event.core.CondJump; import com.dat3m.dartagnan.program.event.core.Label; import com.dat3m.dartagnan.program.event.core.Local; +import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.base.Preconditions; import com.google.common.base.Verify; import org.apache.logging.log4j.LogManager; @@ -28,8 +29,8 @@ import static com.dat3m.dartagnan.configuration.OptionNames.CONSTANT_PROPAGATION; import static com.dat3m.dartagnan.configuration.OptionNames.PROPAGATE_COPY_ASSIGNMENTS; -import static com.dat3m.dartagnan.expression.op.IOpUn.CAST_SIGNED; -import static com.dat3m.dartagnan.expression.op.IOpUn.CAST_UNSIGNED; +import static com.dat3m.dartagnan.expression.op.IntUnaryOp.CAST_SIGNED; +import static com.dat3m.dartagnan.expression.op.IntUnaryOp.CAST_UNSIGNED; /* Sparse conditional constant propagation performs both CP and DCE simultaneously. @@ -67,8 +68,8 @@ public static SparseConditionalConstantPropagation fromConfig(Configuration conf @Override public void run(Function func) { final Predicate checkDoPropagate = propagateCopyAssignments - ? (expr -> expr instanceof IConst || expr instanceof BConst || expr instanceof Register) - : (expr -> expr instanceof IConst || expr instanceof BConst); + ? (expr -> expr instanceof MemoryObject || expr instanceof IntLiteral || expr instanceof BoolLiteral || expr instanceof Register) + : (expr -> expr instanceof MemoryObject || expr instanceof IntLiteral || expr instanceof BoolLiteral); Set reachableEvents = new HashSet<>(); Map> inflowMap = new HashMap<>(); @@ -195,7 +196,7 @@ public Expression visit(Register reg) { public Expression visit(Atom atom) { Expression lhs = transform(atom.getLHS()); Expression rhs = transform(atom.getRHS()); - if (lhs instanceof IValue left && rhs instanceof IValue right) { + if (lhs instanceof IntLiteral left && rhs instanceof IntLiteral right) { return expressions.makeValue(atom.getOp().combine(left.getValue(), right.getValue())); } else { return expressions.makeBinary(lhs, atom.getOp(), rhs); @@ -203,10 +204,10 @@ public Expression visit(Atom atom) { } @Override - public Expression visit(BExprBin bBin) { + public Expression visit(BoolBinaryExpr bBin) { Expression lhs = transform(bBin.getLHS()); Expression rhs = transform(bBin.getRHS()); - if (lhs instanceof BConst left && rhs instanceof BConst right) { + if (lhs instanceof BoolLiteral left && rhs instanceof BoolLiteral right) { return expressions.makeValue(bBin.getOp().combine(left.getValue(), right.getValue())); } else { return expressions.makeBinary(lhs, bBin.getOp(), rhs); @@ -214,9 +215,9 @@ public Expression visit(BExprBin bBin) { } @Override - public Expression visit(BExprUn bUn) { + public Expression visit(BoolUnaryExpr bUn) { Expression inner = transform(bUn.getInner()); - if (inner instanceof BConst bc) { + if (inner instanceof BoolLiteral bc) { return expressions.makeValue(bUn.getOp().combine(bc.getValue())); } else { return expressions.makeUnary(bUn.getOp(), inner); @@ -224,12 +225,12 @@ public Expression visit(BExprUn bUn) { } @Override - public Expression visit(IExprBin iBin) { + public Expression visit(IntBinaryExpr iBin) { Expression lhs = transform(iBin.getLHS()); Expression rhs = transform(iBin.getRHS()); - if (lhs instanceof IValue left && rhs instanceof IValue right) { + if (lhs instanceof IntLiteral left && rhs instanceof IntLiteral right) { return expressions.makeValue(iBin.getOp().combine(left.getValue(), right.getValue()), left.getType()); - } else if ((iBin.getOp() == IOpBin.ADD || iBin.getOp() == IOpBin.SUB) && rhs instanceof IValue right && right.isZero()) { + } else if ((iBin.getOp() == IntBinaryOp.ADD || iBin.getOp() == IntBinaryOp.SUB) && rhs instanceof IntLiteral right && right.isZero()) { return lhs; } else { return expressions.makeBinary(lhs, iBin.getOp(), rhs); @@ -237,7 +238,7 @@ public Expression visit(IExprBin iBin) { } @Override - public Expression visit(IExprUn iUn) { + public Expression visit(IntUnaryExpr iUn) { Expression inner = transform(iUn.getInner()); Expression result; if ((iUn.getOp() == CAST_SIGNED || iUn.getOp() == CAST_UNSIGNED) && iUn.getType() == inner.getType()) { @@ -245,25 +246,25 @@ public Expression visit(IExprUn iUn) { } else { result = expressions.makeUnary(iUn.getOp(), inner, iUn.getType()); } - if (inner instanceof IValue) { + if (inner instanceof IntLiteral) { return result.reduce(); } return result; } @Override - public Expression visit(IfExpr ifExpr) { - Expression guard = transform(ifExpr.getGuard()); - Expression trueBranch = transform(ifExpr.getTrueBranch()); - Expression falseBranch = transform(ifExpr.getFalseBranch()); + public Expression visit(ITEExpr iteExpr) { + Expression guard = transform(iteExpr.getGuard()); + Expression trueBranch = transform(iteExpr.getTrueBranch()); + Expression falseBranch = transform(iteExpr.getFalseBranch()); // We optimize ITEs only if all subexpressions are constant to avoid messing up data dependencies - if (guard instanceof BConst constant && constant.getValue() && falseBranch.getRegs().isEmpty()) { + if (guard instanceof BoolLiteral constant && constant.getValue() && falseBranch.getRegs().isEmpty()) { return trueBranch; } - if (guard instanceof BConst constant && !constant.getValue() && trueBranch.getRegs().isEmpty()) { + if (guard instanceof BoolLiteral constant && !constant.getValue() && trueBranch.getRegs().isEmpty()) { return falseBranch; } - return expressions.makeConditional(guard, trueBranch, falseBranch); + return expressions.makeITE(guard, trueBranch, falseBranch); } private Expression transform(Expression expression) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java index 273f89c795..311cd0bc65 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ThreadCreation.java @@ -4,8 +4,7 @@ import com.dat3m.dartagnan.exception.MalformedProgramException; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; -import com.dat3m.dartagnan.expression.IConst; -import com.dat3m.dartagnan.expression.IValue; +import com.dat3m.dartagnan.expression.IntLiteral; import com.dat3m.dartagnan.expression.processing.ExprTransformer; import com.dat3m.dartagnan.expression.processing.ExpressionVisitor; import com.dat3m.dartagnan.expression.type.IntegerType; @@ -105,7 +104,7 @@ public void run(Program program) { // We collect the communication addresses we use for each thread id. // These are used later to lower pthread_join. - final Map tid2ComAddrMap = new LinkedHashMap<>(); + final Map tid2ComAddrMap = new LinkedHashMap<>(); for (FunctionCall call : thread.getEvents(FunctionCall.class)) { if (!call.isDirectCall()) { continue; @@ -123,7 +122,7 @@ public void run(Program program) { assert resultRegister.getType() instanceof IntegerType; final ThreadCreate createEvent = newThreadCreate(List.of(argument)); - final IValue tidExpr = expressions.makeValue(nextTid, archType); + final IntLiteral tidExpr = expressions.makeValue(nextTid, archType); final MemoryObject comAddress = program.getMemory().allocate(1, true); comAddress.setCVar("__com" + nextTid + "__" + targetFunction.getName()); @@ -169,7 +168,7 @@ public void run(Program program) { This method replaces in all pthread_join calls by a switch over all possible tids. Each candidate thread gets a switch-case which tries to synchronize with that thread. */ - private void handlePthreadJoins(Thread thread, Map tid2ComAddrMap) { + private void handlePthreadJoins(Thread thread, Map tid2ComAddrMap) { final TypeFactory types = TypeFactory.getInstance(); final ExpressionFactory expressions = ExpressionFactory.getInstance(); int joinCounter = 0; @@ -197,11 +196,11 @@ private void handlePthreadJoins(Thread thread, Map tid2ComAd // ----- Construct a switch case for each possible tid ----- final Map> tid2joinCases = new LinkedHashMap<>(); - for (IValue tidCandidate : tid2ComAddrMap.keySet()) { + for (IntLiteral tidCandidate : tid2ComAddrMap.keySet()) { final int tid = tidCandidate.getValueAsInt(); final Expression comAddrOfThreadToJoinWith = tid2ComAddrMap.get(tidCandidate); - if (tidExpr instanceof IConst iConst && iConst.getValueAsInt() != tid) { + if (tidExpr instanceof IntLiteral iConst && iConst.getValueAsInt() != tid) { // Little optimization if we join with a constant address continue; } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java index 1986100df4..205fc917e4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/UnreachableCodeElimination.java @@ -1,6 +1,6 @@ package com.dat3m.dartagnan.program.processing; -import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.expression.BoolLiteral; import com.dat3m.dartagnan.program.Function; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.event.Event; @@ -76,7 +76,7 @@ private void collectReachableEvents(Event start, Set reachable) { private boolean isTerminator(Event e) { return e instanceof Return - || e instanceof AbortIf abort && abort.getCondition() instanceof BConst b && b.getValue(); + || e instanceof AbortIf abort && abort.getCondition() instanceof BoolLiteral b && b.getValue(); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java index a4b90d00cc..101a8e7f2c 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/compilation/VisitorPTX.java @@ -48,7 +48,7 @@ public List visitPtxAtomCAS(PTXAtomCAS e) { Expression address = e.getAddress(); Expression expected = e.getExpectedValue(); Expression newValue = e.getStoreValue(); - Expression storeValue = expressions.makeConditional(expressions.makeEQ(resultRegister, expected), + Expression storeValue = expressions.makeITE(expressions.makeEQ(resultRegister, expected), newValue, resultRegister); Load load = newRMWLoadWithMo(resultRegister, address, Tag.PTX.loadMO(mo)); RMWStore store = newRMWStoreWithMo(load, address, storeValue, Tag.PTX.storeMO(mo)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java index f4f6771a8b..31c8b8b3ee 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/specification/AssertBasic.java @@ -2,7 +2,7 @@ import com.dat3m.dartagnan.encoding.EncodingContext; import com.dat3m.dartagnan.expression.Expression; -import com.dat3m.dartagnan.expression.op.COpBin; +import com.dat3m.dartagnan.expression.op.CmpOp; import com.dat3m.dartagnan.program.Register; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -13,9 +13,9 @@ public class AssertBasic extends AbstractAssert { private final Expression e1; private final Expression e2; - private final COpBin op; + private final CmpOp op; - public AssertBasic(Expression e1, COpBin op, Expression e2) { + public AssertBasic(Expression e1, CmpOp op, Expression e2) { this.e1 = e1; this.e2 = e2; this.op = op; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java index 3802beeacd..19ebe011ee 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java @@ -1,7 +1,7 @@ package com.dat3m.dartagnan.witness; import com.dat3m.dartagnan.encoding.EncodingContext; -import com.dat3m.dartagnan.expression.BConst; +import com.dat3m.dartagnan.expression.BoolLiteral; import com.dat3m.dartagnan.program.Program; import com.dat3m.dartagnan.program.Thread; import com.dat3m.dartagnan.program.event.Event; @@ -188,7 +188,7 @@ private List getSCExecutionOrder(Model model) { Map> map = new HashMap<>(); for (Event e : execEvents) { // TODO improve this: these events correspond to return statements - if (e instanceof Store store && store.getMemValue() instanceof BConst bVal && !bVal.getValue()) { + if (e instanceof Store store && store.getMemValue() instanceof BoolLiteral bVal && !bVal.getValue()) { continue; } BigInteger var = model.evaluate(context.clockVariable("hb", e)); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java index 2c90f0d275..08c31ee49e 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/miscellaneous/AnalysisTest.java @@ -1,9 +1,9 @@ package com.dat3m.dartagnan.miscellaneous; import com.dat3m.dartagnan.configuration.Alias; -import com.dat3m.dartagnan.expression.BNonDet; import com.dat3m.dartagnan.expression.Expression; import com.dat3m.dartagnan.expression.ExpressionFactory; +import com.dat3m.dartagnan.expression.NonDetBool; import com.dat3m.dartagnan.expression.type.IntegerType; import com.dat3m.dartagnan.expression.type.TypeFactory; import com.dat3m.dartagnan.parsers.program.utils.ProgramBuilder; @@ -54,7 +54,7 @@ public void dependencyMustOverride() throws InvalidConfigurationException { Register r1 = b.getOrNewRegister(0, "r1"); Register r2 = b.getOrNewRegister(0, "r2"); Label alt = b.getOrCreateLabel(0, "alt"); - b.addChild(0, newJump(new BNonDet(types.getBooleanType()), alt)); + b.addChild(0, newJump(new NonDetBool(types.getBooleanType()), alt)); Local e0 = newLocal(r0, value(1)); b.addChild(0, e0); Local e1 = newLocal(r1, r0);