Retrascope

Добавил отладочный вывод в случае UNKNOWN-типов у выражений. Выяснилось, что данные проблемы порождаются by Nodes with numeric constants (Literals, which Fortress doesn't know, and not going to know). What should I do having an access to nothing of Node but elaborated type "UNKNOWN" (by getDataType())?

2014.12.11 18:55:21.159. INFO: Retrascope is starting
Running: verilog-parser
Options: {args=src/test/verilog/ram/ram.v --target efsm, v=[src/test/verilog/ram/ram.v]}
Including file 'src/test/verilog/ram/ram.v'
2014.12.11 18:55:21.406. INFO: Start observing module ram.
2014.12.11 18:55:21.407. INFO: add variable clk [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.407. INFO: add variable rst [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable val_rd [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable val_wr [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable addr_in [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.12.11 18:55:21.408. INFO: add variable data_in [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.409. INFO: add variable val_out [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.411. INFO: add variable data_out [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable is_ready [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem0 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem1 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem2 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.412. INFO: add variable mem3 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.413. INFO: add variable result [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.12.11 18:55:21.413. INFO: add variable state [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.12.11 18:55:21.417. INFO: add variable RAM_IDLE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_IDLE is UNKNOWN
[parseAssignment2] DataType of 2'h0 is UNKNOWN
2014.12.11 18:55:21.422. INFO: add variable RAM_READ [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_READ is UNKNOWN
[parseAssignment2] DataType of 2'h1 is UNKNOWN
2014.12.11 18:55:21.422. INFO: add variable RAM_WRITE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_WRITE is UNKNOWN
[parseAssignment2] DataType of 2'h2 is UNKNOWN
2014.12.11 18:55:21.423. INFO: add variable RAM_RESULT [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
[parseAssignment] DataType of RAM_RESULT is UNKNOWN
[parseAssignment2] DataType of 2'h3 is UNKNOWN
[parseAssignment] DataType of is_ready is UNKNOWN
[parseAssignment] DataType of val_out is UNKNOWN
[parseAssignment] DataType of data_out is UNKNOWN
[parseAssignment] DataType of mem0 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem1 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem2 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem3 is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 2'h0 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h1 is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h2 is UNKNOWN
[parseAssignment] DataType of result is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of mem0 is UNKNOWN
[parseAssignment] DataType of mem1 is UNKNOWN
[parseAssignment] DataType of mem2 is UNKNOWN
[parseAssignment] DataType of mem3 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h0 is UNKNOWN
[parseAssignment] DataType of state is UNKNOWN
[parseAssignment2] DataType of 32'h3 is UNKNOWN
Storing: cfg

Running: cfg-cgaa-transformer
Options: {args=src/test/verilog/ram/ram.v --target efsm, cfg=<cfg>}
Storing: cgaa

Running: cgaa-efsm-transformer
Options: {args=src/test/verilog/ram/ram.v --target efsm, cgaa=<cgaa>}
2014.12.11 18:55:21.562. ERROR: The exception has been encountered: java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
at ru.ispras.fortress.solver.engine.z3.SMTStrings.textForData(SMTStrings.java:146)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:378)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:356)
at ru.ispras.fortress.expression.ExprTreeWalker.visitValue(ExprTreeWalker.java:204)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:142)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:117)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:89)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:110)
at ru.ispras.fortress.solver.constraint.ConstraintUtils.solve(ConstraintUtils.java:69)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:307)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:288)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.isSAT(CgaaStateExprVisitor.java:206)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.checkConditionsIfNot(CgaaStateExprVisitor.java:199)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.onBasicBlockBegin(CgaaStateExprVisitor.java:188)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitBasicBlock(CfgWalker.java:261)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSource(CfgWalker.java:219)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:157)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfg(CfgWalker.java:210)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitProcess(CfgWalker.java:201)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitModule(CfgWalker.java:185)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfgModel(CfgWalker.java:172)
at ru.ispras.retrascope.model.cfg.CfgWalker.start(CfgWalker.java:92)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:133)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:115)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:325)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:346)

2014.12.11 18:55:21.564. INFO: Retrascope is shutting down
Exception in thread "main" java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
at ru.ispras.fortress.solver.engine.z3.SMTStrings.textForData(SMTStrings.java:146)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:378)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:356)
at ru.ispras.fortress.expression.ExprTreeWalker.visitValue(ExprTreeWalker.java:204)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:142)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:183)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:150)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:117)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:89)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:110)
at ru.ispras.fortress.solver.constraint.ConstraintUtils.solve(ConstraintUtils.java:69)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:307)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:288)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.isSAT(CgaaStateExprVisitor.java:206)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.checkConditionsIfNot(CgaaStateExprVisitor.java:199)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.onBasicBlockBegin(CgaaStateExprVisitor.java:188)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitBasicBlock(CfgWalker.java:261)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:253)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:235)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSource(CfgWalker.java:219)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:157)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:116)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfg(CfgWalker.java:210)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitProcess(CfgWalker.java:201)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitModule(CfgWalker.java:185)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfgModel(CfgWalker.java:172)
at ru.ispras.retrascope.model.cfg.CfgWalker.start(CfgWalker.java:92)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:133)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:115)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:325)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:346)