flintlang / flint

The Flint Programming Language for Smart Contracts
MIT License
245 stars 18 forks source link

Multidimensional array looping requires an outer array identifier for verification #435

Open mrRachar opened 5 years ago

mrRachar commented 5 years ago

Earlier, multidimensional arrays wouldn't initialise or update the inner loops length at all, which has been fixed, however, due to limitations currently the fix requires getting the name of the outer array and appending the shadow length array prefix onto it. This means it won't work for any Boogie expression, as you can only do this name changing if you have an identifier. The current fix (and thus also the problem) comes from commit bbe65a40ab8b0e37e96c7b8d58c45b191aeb29f6 in Statement+Expression.swift

switch loopVariableType {
  case .dictionaryType: break
  case .arrayType, .fixedSizeArrayType:
    guard case .identifier(let arrayIdentifer) = indexableExpr else {
      print("Currently, only variable multidimensional arrays may work, fatal error")
      fatalError()
    }
    let bStatement = BStatement.assignment(
        .identifier(normaliser.getShadowArraySizePrefix(depth: 0) + variableName),
        .mapRead(.identifier(normaliser.getShadowArraySizePrefix(depth: 1) + arrayIdentifer), index),
        TranslationInformation(sourceLocation: forStatement.sourceLocation)
    )
    assignValueToVariable.append(bStatement)
  default: break
}
mrRachar commented 5 years ago

This issue was originally matteobilardi/flint/#1 and has been moved here for further discussion