Skip to content

Typecheck fn calls #79

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

Draft
mikucionisaau wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Typecheck fn calls #79

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
af2d4f1
Added tests for typechecking function calls (crashes when arg count i…
mikucionisaau Oct 1, 2024
d5bf0ef
Unfinished work
mikucionisaau Feb 14, 2025
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
14 changes: 8 additions & 6 deletions src/ExpressionBuilder.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -341,17 +341,19 @@ void ExpressionBuilder::expr_call_end(uint32_t n)
switch (id.get_type().get_kind()) {
case FUNCTION_EXTERNAL:
case FUNCTION:
if (expr.size() != id.get_type().size()) {
handle_error(TypeException{"$Wrong_number_of_arguments"});
}
if (expr.size() < id.get_type().size())
handle_error(TypeException{"$Too_few_arguments_for_function_call"});
if (expr.size() > id.get_type().size())
handle_error(TypeException{"$Too_many_arguments_for_function_call"});
e = expression_t::create_nary(id.get_type().get_kind() == FUNCTION ? FUN_CALL : FUN_CALL_EXT, expr, position,
id.get_type()[0]);
break;

case PROCESS_SET:
if (expr.size() - 1 != id.get_type().size()) {
handle_error(TypeException{"$Wrong_number_of_arguments"});
}
if (expr.size() - 1 < id.get_type().size())
handle_error(TypeException{"$Too_few_arguments_for_template_instantiation"});
if (expr.size() - 1 > id.get_type().size())
handle_error(TypeException{"$Too_many_arguments_for_template_instantiation"});
instance = static_cast<instance_t*>(id.get_symbol().get_data());

/* Process set lookups are represented as expressions indexing
Expand Down
16 changes: 10 additions & 6 deletions src/typechecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2129,12 +2129,16 @@ bool TypeChecker::checkExpression(expression_t expr)
checkExpression(expr[0]);

bool result = true;
type_t type = expr[0].get_type();
size_t parameters = type.size() - 1;
for (uint32_t i = 0; i < parameters; i++) {
type_t parameter = type[i + 1];
expression_t argument = expr[i + 1];
result &= checkParameterCompatible(parameter, argument);
type_t fn_type = expr[0].get_type(); // [ret_type, arg1_type, ..., argn_type]
size_t param_count = fn_type.size() - 1;
for (uint32_t i = 1; i < param_count; ++i) {
if (i >= expr.get_size()) {
handleError(expr, "$Too_few_function_arguments");
break;
}
type_t param_type = fn_type[i];
expression_t argument = expr[i];
result &= checkParameterCompatible(param_type, argument);
}
return result;
}
Expand Down
49 changes: 49 additions & 0 deletions test/models/function_calls.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.6//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_6.dtd'>
<nta>
<declaration>int v;

bool enabled(int i) {
return (i&gt;0);
}
</declaration>
<template>
<name x="5" y="5">P</name>
<location id="id0" x="136" y="0">
<name x="126" y="-34">Done</name>
</location>
<location id="id1" x="0" y="0">
<urgent/>
</location>
<init ref="id1"/>
<transition id="id2">
<source ref="id1"/>
<target ref="id0"/>
<label kind="guard" x="25" y="-25">enabled(1)</label>
<label kind="assignment" x="25" y="0">v=1</label>
</transition>
</template>
<system>system P;</system>
<queries>
<query>
<formula>simulate[&lt;=5;3] { v, enabled(1) } : 2 : enabled(1)</formula>
<comment>Good call, should pass</comment>
</query>
<query>
<formula>simulate[&lt;=5;3] { v, enabled(1) } : 2 : enabled()</formula>
<comment>Call is missing argument, should give meaningful error and not crash.</comment>
</query>
<query>
<formula>simulate[&lt;=5;3] { v, enabled() } : 2 : enabled(1)</formula>
<comment>Call is missing argument, should give meaningful error and not crash.</comment>
</query>
<query>
<formula>simulate[&lt;=5;3] { v, enabled() } : 2 : enabled()</formula>
<comment>Both calls are missing arguments, should give error message and not crash</comment>
</query>
<query>
<formula>simulate[&lt;=5;3] { v, non_existent() } : 2 : non_existent()</formula>
<comment>Chould give meaningfull error message and not crash</comment>
</query>
</queries>
</nta>
102 changes: 101 additions & 1 deletion test/test_typechecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -473,4 +473,104 @@ TEST_CASE("Nested structs")
CHECK(warns.size() == 0);
auto errs = doc->get_errors();
CHECK(errs.size() == 1);
}
}

TEST_CASE("Function calls in queries")
{
auto doc = read_document("function_calls.xml");
const auto& errs = doc->get_errors();
REQUIRE_MESSAGE(errs.empty(), errs.front().msg);
auto builder = std::make_unique<UTAP::TigaPropertyBuilder>(*doc);
const auto& queries = doc->get_queries();
REQUIRE(queries.size() == 5);
SUBCASE("Correct")
{
const auto& query = *queries.begin();
builder->parse(query.formula.c_str(), query.location, query.options);
REQUIRE_MESSAGE(errs.empty(), errs.front().msg);
/*
REQUIRE_MESSAGE(props.size() == prop_count + 1, "Should contain one more property");
const auto& expr = std::next(props.begin(), prop_count)->intermediate;
REQUIRE(expr.get_size() == 7);
CHECK(expr.get(0).get_value() == 3); ///< max runs
CHECK(expr.get(1).get_value() == 1); ///< bound kind of time
CHECK(expr.get(2).get_value() == 5); ///< time bound
// CHECK(expr.get(3));
// CHECK(expr.get(4));
// CHECK(expr.get(5));
CHECK(expr.get(6).get_value() == 2); ///< number of satisfying runs
*/
}
SUBCASE("Predicate misses argument")
{
const auto& query = *std::next(queries.begin(), 1);
builder->parse(query.formula.c_str(), query.location, query.options);
CHECK_MESSAGE(errs.empty(), errs.front().msg);
/*
REQUIRE_MESSAGE(props.size() == prop_count + 1, "Should contain one more property");
const auto& expr = std::next(props.begin(), prop_count)->intermediate;
REQUIRE(expr.get_size() == 7);
CHECK(expr.get(0).get_value() == 3); ///< max runs
CHECK(expr.get(1).get_value() == 1); ///< bound kind of time
CHECK(expr.get(2).get_value() == 5); ///< time bound
// CHECK(expr.get(3));
// CHECK(expr.get(4));
// CHECK(expr.get(5));
CHECK(expr.get(6).get_value() == 2); ///< number of satisfying runs
*/
}
SUBCASE("Monitored expression misses argument")
{
const auto& query = *std::next(queries.begin(), 2);
builder->parse(query.formula.c_str(), query.location, query.options);
CHECK_MESSAGE(errs.empty(), errs.front().msg);
/*
REQUIRE_MESSAGE(props.size() == prop_count + 1, "Should contain one more property");
const auto& expr = std::next(props.begin(), prop_count)->intermediate;
REQUIRE(expr.get_size() == 7);
CHECK(expr.get(0).get_value() == 3); ///< max runs
CHECK(expr.get(1).get_value() == 1); ///< bound kind of time
CHECK(expr.get(2).get_value() == 5); ///< time bound
// CHECK(expr.get(3));
// CHECK(expr.get(4));
// CHECK(expr.get(5));
CHECK(expr.get(6).get_value() == 2); ///< number of satisfying runs
*/
}
SUBCASE("Missing arguments in both calls")
{
const auto& query = *std::next(queries.begin(), 3);
builder->parse(query.formula.c_str(), query.location, query.options);
CHECK_MESSAGE(errs.empty(), errs.front().msg);
/*
REQUIRE_MESSAGE(props.size() == prop_count + 1, "Should contain one more property");
const auto& expr = std::next(props.begin(), prop_count)->intermediate;
REQUIRE(expr.get_size() == 7);
CHECK(expr.get(0).get_value() == 3); ///< max runs
CHECK(expr.get(1).get_value() == 1); ///< bound kind of time
CHECK(expr.get(2).get_value() == 5); ///< time bound
// CHECK(expr.get(3));
// CHECK(expr.get(4));
// CHECK(expr.get(5));
CHECK(expr.get(6).get_value() == 2); ///< number of satisfying runs
*/
}
SUBCASE("Non-existent fn")
{
const auto& query = *std::next(queries.begin(), 4);
builder->parse(query.formula.c_str(), query.location, query.options);
CHECK_MESSAGE(errs.empty(), errs.front().msg);
/*
REQUIRE_MESSAGE(props.size() == prop_count + 1, "Should contain one more property");
const auto& expr = std::next(props.begin(), prop_count)->intermediate;
REQUIRE(expr.get_size() == 7);
CHECK(expr.get(0).get_value() == 3); ///< max runs
CHECK(expr.get(1).get_value() == 1); ///< bound kind of time
CHECK(expr.get(2).get_value() == 5); ///< time bound
// CHECK(expr.get(3));
// CHECK(expr.get(4));
// CHECK(expr.get(5));
CHECK(expr.get(6).get_value() == 2); ///< number of satisfying runs
*/
}
}
Loading