Error: Atom's argument type is not a subtype of its declared type

[shmichael]

I am running securify2 on Ubuntu 22. Installed dependencies, python3.7 and followed the installation instructions (not using docker).

$ securify -b 0x3b1417C1f204607DEdA4767929497256e4ff540C --key ~/.local/api_key.txt 
Traceback (most recent call last):
  File "/home/dev/projects/securify2/venv/bin/securify", line 33, in <module>
    sys.exit(load_entry_point('securify', 'console_scripts', 'securify')())
  File "/home/dev/projects/securify2/securify/__main__.py", line 272, in main
    severity_exc=args.exclude_severity)
  File "/home/dev/projects/securify2/securify/__main__.py", line 15, in get_list_of_patterns
    pattern_classes = discover_patterns()
  File "/home/dev/projects/securify2/securify/analyses/analysis.py", line 123, in discover_patterns
    patterns.update(c.get())
  File "/home/dev/projects/securify2/securify/analyses/patterns/static/static_analysis_patterns.py", line 16, in get
    patterns = cls.__list_static_patterns()
  File "/home/dev/projects/securify2/securify/analyses/patterns/static/static_analysis_patterns.py", line 23, in __list_static_patterns
    patterns = static_analysis.discover_patterns()
  File "/home/dev/projects/securify2/securify/staticanalysis/static_analysis.py", line 69, in discover_patterns
    souffle_kwargs=kw_args_souffle)
  File "/home/dev/projects/securify2/securify/staticanalysis/souffle/souffle.py", line 62, in run_souffle
    **(souffle_kwargs or {}))
  File "/home/dev/projects/securify2/securify/staticanalysis/souffle/wrapper.py", line 119, in souffle_wrapper
    stderr_data=codecs.decode(stderrdata),
securify.staticanalysis.souffle.exceptions.SouffleError: Error during souffle execution:  

Warning: Deprecated type declaration used in util-sets.dl:5:2
Warning: No rules/facts defined for relation patternIncorrectInequalityPattern.compliantInContext in abstract-context-pattern.dl:9:8
Warning: Variable comment only occurs once in abstract-context-pattern.dl:26:38
Warning: Variable ctxString only occurs once in abstract-context-pattern.dl:26:81
Warning: Variable from only occurs once in analysis-dataflow.dl:87:35
Warning: Deprecated type declaration used in analysis-input.dl:3:1
Warning: Deprecated type declaration used in analysis-input.dl:4:1
Warning: Deprecated type declaration used in analysis-input.dl:5:1
Warning: Deprecated type declaration used in analysis-input.dl:6:1
Warning: Deprecated type declaration used in analysis-input.dl:7:1
Warning: Deprecated type declaration used in analysis-input.dl:8:1
Warning: Deprecated type declaration used in analysis-input.dl:9:1
Warning: Deprecated type declaration used in analysis-patterns.dl:1:1
Warning: Deprecated type declaration used in analysis-patterns.dl:4:1
Warning: Deprecated type declaration used in analysis-patterns.dl:5:1
Warning: Deprecated type declaration used in analysis-patterns.dl:6:1
Warning: No rules/facts defined for relation patternUnusedStateVariablePattern.compliance in analysis-patterns.dl:29:8
Warning: Deprecated type declaration used in callstack-context.dl:3:1
Warning: Variable callerFunction only occurs once in callstack-context.dl:20:26
Warning: Variable callerFunction only occurs once in callstack-context.dl:28:26
Warning: Variable callerTag only occurs once in callstack-context.dl:28:59
Warning: Variable callerFunction only occurs once in callstack-context.dl:37:26
Warning: Variable callerTransfers only occurs once in callstack-context.dl:37:42
Warning: Variable callerTag only occurs once in callstack-context.dl:37:59
Error: Atom's argument type is not a subtype of its declared type in locked-ether.dl:15:24
The argument's declared type is Contract in abstract-contract-pattern.dl:26:37
Warning: Variable argInContext only occurs once in pass.dl:27:38
Error: Atom's argument type is not a subtype of its declared type in timestamp.dl:53:40
The argument's declared type is Element in timestamp.dl:52:77
Error: Atom's argument type is not a subtype of its declared type in tx-origin.dl:37:14
The argument's declared type is Transfer in tx-origin.dl:36:26
Warning: Variable valueCtx only occurs once in unrestricted-ether-flow.dl:38:38
Warning: Variable thisBlock only occurs once in unused-return.dl:11:22
Warning: Variable _c marked as singleton but occurs more than once in __semantics__.dl:23:146
Warning: Variable _c marked as singleton but occurs more than once in __semantics__.dl:24:144
Warning: Variable _c marked as singleton but occurs more than once in __semantics__.dl:27:111
Warning: Variable _c marked as singleton but occurs more than once in __semantics__.dl:31:109
Warning: Variable _c marked as singleton but occurs more than once in __semantics__.dl:33:141
Error: Atom's argument type is not a subtype of its declared type in trusted-variable.dl:29:32
The argument's declared type is Set in trusted-variable.dl:12:55
Error: Ambiguous record in trusted-variable.dl:29:46
Warning: No rules/facts defined for relation warnings in util-debug.dl:5:7
5 errors generated, evaluation aborted

[vishnuram1999]

Even I'm facing the same problem. Where you able to find a solution for this?

[jason-gigastar]

I suppose I'll have to punt on this project being useless in the present state, but in case it helps someone:

Here's an incomplete solution that seems to solve the first 4 of 5 errors above.

My changes were to versions of ubuntu, SOLC, souffle, python, and I added the --legacy argument for souffle (documented here). Here's the updated Dockerfile.txt (you'll need to remove the .txt extension).

However, I still get the following error:

Error: Ambiguous record in trusted-variable.dl:29:46
1 errors generated, evaluation aborted
The command '/bin/sh -c cd /sec/securify/staticanalysis/souffle_analysis &&         souffle --dl-program=../dl-program         --fact-dir=/sec/securify/staticanalysis/facts_in         --output-dir=/sec/securify/staticanalysis/facts_out         -L../libfunctors -w analysis.dl --legacy' returned a non-zero code: 1

We can see the error message in the souffle code here and below but I don't see the next step to debug this.

 void TypeCheckerImpl::visitRecordInit(const RecordInit& rec) {
     TypeSet types = typeAnalysis.getTypes(&rec);
  
     if (!isOfKind(types, TypeAttribute::Record) || types.size() != 1) {
         report.addError("Ambiguous record", rec.getSrcLoc());
         return;
     }

     // At this point we know that there is exactly one type in set, so we can take it.
     auto& recordType = *as<analysis::RecordType>(*types.begin());
  
     if (recordType.getFields().size() != rec.getArguments().size()) {
         report.addError("Wrong number of arguments given to record", rec.getSrcLoc());
         return;
     }
 }

[LLrber]

Hello, has anyone solved this problem? I am trying to learn about securify2 for my undergraduate graduation project, but it may be beyond my current ability to solve.

[lipeizechuan]

I have solved this problem. In general, it is the problem of version dependency. From the source code, we can find that this program is for the solc0.5.0-0.6.0, so all the other dependencies need to matching for it. It means the other dependencies version's period need to superposition to the period of the solc0.5.0-0.6.0. Such as souffle, you need to use the souffle 1.6.2.