Bug #7097: 32-bit constants should be casted to appropriate values - Retrascope - Open-Source Projects

Actions

Copy link

Bug #7097

closed

32-bit constants should be casted to appropriate values

Added by Sergey Smolov over 8 years ago. Updated about 7 years ago.

Status:

Closed

Priority:

Normal

Assignee:

Sergey Smolov

Category:

Engine (Parser)

Target version:

0.2

Start date:

04/21/2016

Due date:

% Done:

100%

Estimated time:

Detected in build:

verilog.benchmarks

Platform:

Published in build:

1.0.1-beta-170912

Description

Use verilog.benchmarks auxiliary branch to reproduce this bug:

2016.04.21 17:10:40.724. INFO: Retrascope is starting
2016.04.21 17:10:40.728. INFO: Running: verilog-parser

2016.04.21 17:10:40.728. INFO: Options: {v=[/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v], args=/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v --target efsm}

Including file '/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v'
2016.04.21 17:10:40.999. INFO: Storing: cfg

2016.04.21 17:10:40.999. INFO: Running: cfg-cgaa-transformer

2016.04.21 17:10:40.999. INFO: Options: {args=/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v --target efsm, cfg=<cfg>}

2016.04.21 17:10:41.003. INFO: Storing: cgaa

2016.04.21 17:10:41.003. INFO: Running: cgaa-efsm-transformer

2016.04.21 17:10:41.003. INFO: Options: {cgaa=<cgaa>, args=/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v --target efsm}

Exception in thread "main" java.lang.IllegalArgumentException: Errors in the expression description: [line 6 column 180: invalid function application, sort mismatch on argument at position 2, (declare-const wb_op_dest (_ BitVec 3))
(declare-const mem_op_dest (_ BitVec 3))
(declare-const decoding_op_src1 (_ BitVec 3))
(declare-const ex_op_dest (_ BitVec 3))
(declare-const decoding_op_src2 (_ BitVec 3))
(assert  (and (and (or (= decoding_op_src1 ex_op_dest) (= decoding_op_src1 mem_op_dest) (= decoding_op_src1 wb_op_dest)) (not (= decoding_op_src1 #b00000000000000000000000000000000))) (and (or (= decoding_op_src2 ex_op_dest) (= decoding_op_src2 mem_op_dest) (= decoding_op_src2 wb_op_dest)) (not (= decoding_op_src2 #b00000000000000000000000000000000)))))
(check-sat)
(get-value ( wb_op_dest mem_op_dest decoding_op_src1 ex_op_dest decoding_op_src2))
(get-model)
(exit)
]
    at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:389)
    at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:360)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmDataExtractor.checkInvCompliance(CgaaEfsmDataExtractor.java:231)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmDataExtractor.checkActionReachable(CgaaEfsmDataExtractor.java:217)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmDataExtractor.checkConditionsIfNot(CgaaEfsmDataExtractor.java:211)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmDataExtractor.onBasicBlockBegin(CgaaEfsmDataExtractor.java:200)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitBasicBlock(CfgWalker.java:361)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:186)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitCase(CfgWalker.java:353)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:189)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitSwitch(CfgWalker.java:343)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:192)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitCase(CfgWalker.java:353)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:189)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitSwitch(CfgWalker.java:343)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:192)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72)
    at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitProcess(CfgWalker.java:305)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitModule(CfgWalker.java:279)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitCfgModel(CfgWalker.java:255)
    at ru.ispras.retrascope.model.cfg.walker.CfgWalker.start(CfgWalker.java:156)
    at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:87)
    at ru.ispras.retrascope.basis.Engine.start(Engine.java:214)
    at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:112)
    at ru.ispras.retrascope.basis.Engine.start(Engine.java:214)
    at ru.ispras.retrascope.Retrascope$ToolRun.start(Retrascope.java:207)
    at ru.ispras.retrascope.Retrascope.main(Retrascope.java:414)
    at ru.ispras.retrascope.Retrascope.main(Retrascope.java:367)