Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix double free for lsc models during parsing #47

Merged
merged 4 commits into from
Aug 9, 2023
Merged

Fix double free for lsc models during parsing #47

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
1d84469
Remove constructor and destructor
thorulf4 Feb 23, 2023
059abe4
Merge remote-tracking branch 'upstream/main' into fix_invalid_free
thorulf4 Jul 13, 2023
5d58754
Added testing and default initialize to nullptr
thorulf4 Jul 13, 2023
90553e5
Strengthen non empty gurantees with unsigned integer types
thorulf4 Aug 9, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 16 additions & 27 deletions include/utap/document.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,11 +202,11 @@ struct instance_line_t; // to be defined later
/** Common members among LSC elements */
struct LSC_element_t
{
int nr{-1}; /**< Placement in input file */
uint32_t nr; /**< Placement in input file */
int location{-1};
bool is_in_prechart{false};
explicit LSC_element_t(uint32_t nr): nr{nr} {}
int get_nr() const { return nr; }
bool empty() const { return nr == -1; }
};

/** Information about a message. Messages have a source (src) and a
Expand All @@ -218,6 +218,7 @@ struct message_t : LSC_element_t
instance_line_t* src{nullptr}; /**< Pointer to source instance line */
instance_line_t* dst{nullptr}; /**< Pointer to destination instance line */
expression_t label; /**< The label */
explicit message_t(uint32_t nr): LSC_element_t{nr} {}
};
/** Information about a condition. Conditions have an anchor instance lines.
* The label is stored as an expression.
Expand All @@ -227,6 +228,7 @@ struct condition_t : LSC_element_t
std::vector<instance_line_t*> anchors{}; /**< Pointer to anchor instance lines */
expression_t label; /**< The label */
bool isHot{false};
explicit condition_t(uint32_t nr): LSC_element_t{nr} {}
};

/** Information about an update. Update have an anchor instance line.
Expand All @@ -236,39 +238,26 @@ struct update_t : LSC_element_t
{
instance_line_t* anchor{nullptr}; /**< Pointer to anchor instance line */
expression_t label; /**< The label */
explicit update_t(uint32_t nr): LSC_element_t{nr} {}
};

struct simregion_t : stringify_t<simregion_t>
{
int nr{};
message_t* message; /** May be empty */
condition_t* condition; /** May be empty */
update_t* update; /** May be empty */
uint32_t nr{};
message_t* message{nullptr}; /** May be empty */
condition_t* condition{nullptr}; /** May be empty */
update_t* update{nullptr}; /** May be empty */

int get_loc() const;
bool is_in_prechart() const;

simregion_t()
{
message = new message_t();
condition = new condition_t();
update = new update_t();
}

~simregion_t() noexcept
{
delete message;
delete condition;
delete update;
}

std::ostream& print(std::ostream&) const;
bool has_message() const { return message != nullptr && !message->empty(); }
bool has_condition() const { return condition != nullptr && !condition->empty(); }
bool has_update() const { return update != nullptr && !update->empty(); }
void set_message(std::deque<message_t>& messages, int nr);
void set_condition(std::deque<condition_t>& conditions, int nr);
void set_update(std::deque<update_t>& updates, int nr);
bool has_message() const { return message != nullptr; }
bool has_condition() const { return condition != nullptr; }
bool has_update() const { return update != nullptr; }
void set_message(std::deque<message_t>& messages, uint32_t nr);
void set_condition(std::deque<condition_t>& conditions, uint32_t nr);
void set_update(std::deque<update_t>& updates, uint32_t nr);
};

struct compare_simregion
Expand Down Expand Up @@ -353,7 +342,7 @@ struct instance_t
*/
struct instance_line_t : public instance_t
{
int32_t instance_nr; /**< InstanceLine number in template */
uint32_t instance_nr; /**< InstanceLine number in template */
std::vector<simregion_t> getSimregions(const std::vector<simregion_t>& simregions);
void add_parameters(instance_t& inst, frame_t params, const std::vector<expression_t>& arguments);
};
Expand Down
32 changes: 13 additions & 19 deletions src/document.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -340,37 +340,34 @@ instance_line_t& template_t::add_instance_line()
message_t& template_t::add_message(symbol_t src, symbol_t dst, int loc, bool pch)
{
int32_t nr = messages.empty() ? 0 : messages.back().nr + 1;
auto& message = messages.emplace_back();
auto& message = messages.emplace_back(nr);
message.src = static_cast<instance_line_t*>(src.get_data());
message.dst = static_cast<instance_line_t*>(dst.get_data());
message.location = loc;
message.is_in_prechart = pch;
message.nr = nr;
return message;
}

update_t& template_t::add_update(symbol_t anchor, int loc, bool pch)
{
int32_t nr = updates.empty() ? 0 : updates.back().nr + 1;
auto& update = updates.emplace_back();
auto& update = updates.emplace_back(nr);
update.anchor = static_cast<instance_line_t*>(anchor.get_data());
update.location = loc;
update.is_in_prechart = pch;
update.nr = nr;
return update;
}

condition_t& template_t::add_condition(vector<symbol_t> anchors, int loc, bool pch, bool isHot)
{
int32_t nr = conditions.empty() ? 0 : conditions.back().nr + 1;
auto& condition = conditions.emplace_back();
auto& condition = conditions.emplace_back(nr);

for (auto& anchor : anchors) {
condition.anchors.push_back(static_cast<instance_line_t*>(anchor.get_data())); // TODO
}
condition.location = loc;
condition.is_in_prechart = pch;
condition.nr = nr;
condition.isHot = isHot;
return condition;
}
Expand Down Expand Up @@ -532,7 +529,6 @@ bool template_t::get_update(instance_line_t& instance, int y, update_t*& simUpda
*/
bool template_t::get_update(vector<instance_line_t*>& instances, int y, update_t*& simUpdate)
{
update_t update;
for (auto& instance : instances) {
if (get_update(*instance, y, simUpdate))
return true;
Expand Down Expand Up @@ -563,24 +559,22 @@ vector<simregion_t> instance_line_t::getSimregions(const vector<simregion_t>& si
// get the simregions anchored to this instance
for (const auto& reg : simregions) {
const message_t* m = reg.message;
if (!m->empty() && (m->src->instance_nr == this->instance_nr || m->dst->instance_nr == this->instance_nr)) {
if ((m->src->instance_nr == this->instance_nr || m->dst->instance_nr == this->instance_nr)) {
i_simregions.push_back(reg);
continue;
}

const update_t* u = reg.update;
if (!u->empty() && u->anchor->instance_nr == this->instance_nr) {
if (u->anchor->instance_nr == this->instance_nr) {
i_simregions.push_back(reg);
continue;
}

const condition_t* c = reg.condition;
if (!c->empty()) {
for (auto* instance : c->anchors) {
if (instance->instance_nr == this->instance_nr) {
i_simregions.push_back(reg);
break;
}
for (auto* instance : c->anchors) {
if (instance->instance_nr == this->instance_nr) {
i_simregions.push_back(reg);
break;
}
}
}
Expand Down Expand Up @@ -619,7 +613,7 @@ bool simregion_t::is_in_prechart() const
return false; // should not happen
}

void simregion_t::set_message(std::deque<message_t>& messages, int nr)
void simregion_t::set_message(std::deque<message_t>& messages, uint32_t nr)
{
for (auto& message : messages) {
if (message.nr == nr) {
Expand All @@ -629,7 +623,7 @@ void simregion_t::set_message(std::deque<message_t>& messages, int nr)
}
}

void simregion_t::set_condition(std::deque<condition_t>& conditions, int nr)
void simregion_t::set_condition(std::deque<condition_t>& conditions, uint32_t nr)
{
for (auto& condition : conditions) {
if (condition.nr == nr) {
Expand All @@ -639,7 +633,7 @@ void simregion_t::set_condition(std::deque<condition_t>& conditions, int nr)
}
}

void simregion_t::set_update(std::deque<update_t>& updates, int nr)
void simregion_t::set_update(std::deque<update_t>& updates, uint32_t nr)
{
for (auto& update : updates) {
if (update.nr == nr) {
Expand Down Expand Up @@ -675,7 +669,7 @@ std::ostream& simregion_t::print(std::ostream& os) const
return os << ")";
}

inline auto find_simregion_by_nr(int nr)
inline auto find_simregion_by_nr(uint32_t nr)
{
return [nr](const simregion_t& reg) { return reg.nr == nr; };
}
Expand Down
183 changes: 183 additions & 0 deletions test/models/lsc_example.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,183 @@
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'>
<nta>
<declaration>// Place global declarations here.
chan m1, m3, m4, m2;
clock x;</declaration>
<template>
<name x="5" y="5">A</name>
<declaration>// Place local declarations here.
</declaration>
<location id="id0" x="16" y="-40">
</location>
<init ref="id0"/>
<transition>
<source ref="id0"/>
<target ref="id0"/>
<label kind="synchronisation" x="0" y="32">m2?</label>
<nail x="56" y="32"/>
<nail x="-24" y="32"/>
</transition>
<transition>
<source ref="id0"/>
<target ref="id0"/>
<label kind="synchronisation" x="0" y="-136">m4?</label>
<nail x="-24" y="-112"/>
<nail x="56" y="-112"/>
</transition>
</template>
<template>
<name>B</name>
<location id="id1" x="0" y="96">
<name x="-8" y="128">loc2</name>
<label kind="invariant" x="-10" y="111">x&lt;=5</label>
</location>
<location id="id2" x="0" y="-48">
<name x="-16" y="-96">loc1</name>
<label kind="invariant" x="-16" y="-80">x&lt;=5</label>
</location>
<init ref="id2"/>
<transition>
<source ref="id1"/>
<target ref="id2"/>
<label kind="synchronisation" x="32" y="0">m2!</label>
<nail x="24" y="24"/>
</transition>
<transition>
<source ref="id2"/>
<target ref="id1"/>
<label kind="guard" x="-64" y="0">x&gt;=3</label>
<label kind="synchronisation" x="-64" y="15">m1!</label>
<nail x="-24" y="24"/>
</transition>
</template>
<template>
<name>C</name>
<location id="id3" x="96" y="96">
<name x="80" y="112">loc5</name>
<committed/>
</location>
<location id="id4" x="0" y="96">
<name x="-16" y="112">loc4</name>
</location>
<location id="id5" x="0" y="0">
<name x="-10" y="-30">loc3</name>
</location>
<init ref="id5"/>
<transition>
<source ref="id3"/>
<target ref="id5"/>
<label kind="synchronisation" x="96" y="24">m4!</label>
<nail x="96" y="0"/>
</transition>
<transition>
<source ref="id5"/>
<target ref="id4"/>
<label kind="synchronisation" x="-32" y="40">m1?</label>
</transition>
<transition>
<source ref="id4"/>
<target ref="id3"/>
<label kind="synchronisation" x="32" y="96">m3!</label>
</transition>
</template>
<template>
<name>D</name>
<location id="id6" x="0" y="104">
</location>
<location id="id7" x="0" y="0">
</location>
<init ref="id7"/>
<transition>
<source ref="id6"/>
<target ref="id7"/>
<nail x="-32" y="104"/>
<nail x="-32" y="0"/>
</transition>
<transition>
<source ref="id6"/>
<target ref="id6"/>
<label kind="synchronisation" x="-8" y="152">m4?</label>
<nail x="-16" y="152"/>
<nail x="24" y="152"/>
</transition>
<transition>
<source ref="id7"/>
<target ref="id6"/>
<label kind="synchronisation" x="8" y="32">m3?</label>
</transition>
</template>
<lsc>
<name>LscTemplate</name>
<parameter>int a, int b</parameter>
<type>Universal</type>
<mode>Invariant</mode>
<declaration>// Place local declarations here.
</declaration>
<yloccoord number="0" y="0"/>
<yloccoord number="1" y="56"/>
<yloccoord number="2" y="104"/>
<yloccoord number="3" y="144"/>
<yloccoord number="4" y="168"/>
<yloccoord number="5" y="220"/>
<instance id="id8" x="432" y="0">
<name x="0" y="0">D</name>
</instance>
<instance id="id9" x="288" y="0">
<name x="0" y="0">C</name>
</instance>
<instance id="id10" x="144" y="0">
<name x="0" y="0">B</name>
</instance>
<instance id="id11" x="0" y="0">
<name x="0" y="0">A</name>
</instance>
<prechart x="0" y="104">
<lsclocation>2</lsclocation>
</prechart>
<message x="0" y="144">
<source ref="id10"/>
<target ref="id11"/>
<lsclocation>3</lsclocation>
<label kind="message" x="61" y="-18">m2</label>
</message>
<message x="0" y="168">
<source ref="id9"/>
<target ref="id8"/>
<lsclocation>4</lsclocation>
<label kind="message" x="357" y="-18">m3</label>
</message>
<message x="0" y="56">
<source ref="id10"/>
<target ref="id9"/>
<lsclocation>1</lsclocation>
<label kind="message" x="205" y="-18">m1</label>
</message>
<condition x="0" y="56">
<anchor instanceid="id9"/>
<lsclocation>1</lsclocation>
<temperature>cold</temperature>
<label kind="condition">x &gt;=b</label>
</condition>
<condition x="0" y="144">
<anchor instanceid="id11"/>
<lsclocation>3</lsclocation>
<temperature>hot</temperature>
<label kind="condition">x &gt;= a</label>
</condition>
</lsc>
<system>// Place template instantiations here.
Scenario = LscTemplate(2,3);

// List one or more processes to be composed into a system.
system A, B, C, D;
</system>
<queries>
<query>
<formula>sat: Scenario
</formula>
<comment>
</comment>
</query>
</queries>
</nta>
Loading