microsoft / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
223 stars 80 forks source link

Deserializing strings stuck forever #17

Open marcelotaube opened 6 years ago

marcelotaube commented 6 years ago

Currently ivy deserialize for string literals produces a loop which does not advance the loop index, effectively creating an infinite loop

Look at the code extracted:

        while (pos < inp.size() && inp[pos]) {
            if (inp[pos] == '"')
                throw deser_err();
         }
        res.push_back(inp[pos++]);
     }

Additionally i think it might be better to serialize the string size at the beggining of the package rather than checking for the first '\0' tab, that is because some users might want to treat the string as a generic buffer to store any binary piece of data.

kenmcmil commented 6 years ago

Hi Marcelo,

The string deserialization bug is fixed in a branch pldi18 (which doesn’t have the multiple ‘after init’ feature). I didn’t switch to using a length field because I’m not sure how std::string handles nulls in the string. If you really need to send binary data, let me know…

--Ken

From: marcelotaube [mailto:notifications@github.com] Sent: Sunday, February 18, 2018 10:16 AM To: Microsoft/ivy ivy@noreply.github.com Cc: Subscribed subscribed@noreply.github.com Subject: [Microsoft/ivy] Deserializing strings stuck forever (#17)

Currently ivy deserialize for string literals produces a loop which does not advance the loop index, effectively creating an infinite loop

Look at the code extracted:

    while (pos < inp.size() && inp[pos]) {

        if (inp[pos] == '"')

            throw deser_err();

     }

    res.push_back(inp[pos++]);

 }

Additionally i think it might be better to serialize the string size at the beggining of the package rather than checking for the first '\0' tab, that is because some users might want to treat the string as a generic buffer to store any binary piece of data.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FMicrosoft%2Fivy%2Fissues%2F17&data=04%7C01%7Ckenmcmil%40exchange.microsoft.com%7C08ec991115bb4c02318a08d576fbaa17%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636545745622071893%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwifQ%3D%3D%7C-1&sdata=XdDh2cabIY7yMYyYWYgejn7%2Fq0ibiAnX1dmrnmQ64I4%3D&reserved=0, or mute the threadhttps://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FAHo5VcSuBgnI0MZYaNQdTZpA67H1o4i8ks5tWGjfgaJpZM4SJyPP&data=04%7C01%7Ckenmcmil%40exchange.microsoft.com%7C08ec991115bb4c02318a08d576fbaa17%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636545745622071893%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwifQ%3D%3D%7C-1&sdata=xWbYyiDXNdTZ766oGnKIFmuL9XH3GsD3%2BA2BCMaMe88%3D&reserved=0.