| 44 | { |
| 45 | |
| 46 | std::string formatDatatypeAccessor(smtutil::Expression const& _expr, std::vector<std::string> const& _args) |
| 47 | { |
| 48 | auto const& op = _expr.name; |
| 49 | |
| 50 | // This is the most complicated part of the translation. |
| 51 | // Datatype accessor means access to a field of a datatype. |
| 52 | // In our encoding, datatypes are used to encode: |
| 53 | // - arrays/mappings as the tuple (array, length) |
| 54 | // - structs as the tuple (<member1>, ..., <memberK>) |
| 55 | // - hash and signature functions as the tuple (keccak256, sha256, ripemd160, ecrecover), |
| 56 | // where each element is an array emulating an UF |
| 57 | // - abi.* functions as the tuple (<abiCall1>, ..., <abiCallK>). |
| 58 | if (op == "dt_accessor_keccak256") |
| 59 | return "keccak256"; |
| 60 | if (op == "dt_accessor_sha256") |
| 61 | return "sha256"; |
| 62 | if (op == "dt_accessor_ripemd160") |
| 63 | return "ripemd160"; |
| 64 | if (op == "dt_accessor_ecrecover") |
| 65 | return "ecrecover"; |
| 66 | |
| 67 | std::string accessorStr = "accessor_"; |
| 68 | // Struct members have suffix "accessor_<memberName>". |
| 69 | std::string type = op.substr(op.rfind(accessorStr) + accessorStr.size()); |
| 70 | solAssert(_expr.arguments.size() == 1, ""); |
| 71 | |
| 72 | if (type == "length") |
| 73 | return _args.at(0) + ".length"; |
| 74 | if (type == "array") |
| 75 | return _args.at(0); |
| 76 | |
| 77 | if ( |
| 78 | starts_with(type, "block") || |
| 79 | starts_with(type, "msg") || |
| 80 | starts_with(type, "tx") || |
| 81 | starts_with(type, "abi") |
| 82 | ) |
| 83 | return type; |
| 84 | |
| 85 | if (starts_with(type, "t_function_abi")) |
| 86 | return type; |
| 87 | |
| 88 | return _args.at(0) + "." + type; |
| 89 | } |
| 90 | |
| 91 | std::string formatGenericOp(smtutil::Expression const& _expr, std::vector<std::string> const& _args) |
| 92 | { |
no test coverage detected