Added support for assert and assume statement (#1548) #1799

enisah · 2019-03-18T13:32:08Z

Added removeAssertAssume pass in frontend which will remove
all assert and assume statements from program when BUILD_TYPE=RELEASE
Not supported in deparsers and verifyChecksum block with assumption
that it is not needed
Added support for code gen for built-in methods in ebpf backend
Changed generating error code value in bmv2 backend to be
generated like hex value into json file

Signed-off-by: Enisa Hadzic enisa.hadzic@rt-rk.com

* Added removeAssertAssume pass in frontend which will remove all assert and assume statements from program when BUILD_TYPE=RELEASE * Not supported in deparsers and verifyChecksum block with assumption that it is not needed * Added support for code gen for built-in methods in ebpf backend * Changed generating error code value in bmv2 backend to be generated like hex value into json file Signed-off-by: Enisa Hadzic <enisa.hadzic@rt-rk.com>

jafingerhut · 2019-03-18T13:58:12Z

@liujed @jnfoster Pinging you folks on this, as I know you are interested in this topic, and may be working on an implementation of these ideas that are hopefully in alignment with this? Or does this PR represent independent implementation work?

mihaibudiu

This is nice, but I think we should make assert/assume part of the architecture files, and not part of core.p4.
Or part of some library.

mihaibudiu · 2019-03-19T00:38:08Z

backends/bmv2/common/expression.cpp

@@ -251,7 +251,9 @@ void ExpressionConverter::postorder(const IR::Member* expression)  {
        result->emplace("type", "hexstr");
        auto decl = type->to<IR::Type_Error>()->getDeclByName(expression->member.name);
        auto errorValue = structure->errorCodesMap.at(decl);
-        result->emplace("value", Util::toString(errorValue));
+        // this generates error constant like hex value
+        auto reprValue = stringRepr(errorValue);


if this is a bug fix you should probably file a separate PR for it, including a test case.

Thank you for all comments.
I think that it is a bug fix, because when I extended core.p4 errors, I had noticed that two tests had failed: checksum3-bmv2.p4 and checksum2-bmv2.p4. These tests reported out_of_range exception when make check is done, because tests added new errors which will have values 9 and 10, but it didn't generate error values as hex values (0x9 and 0xa) in json file. For example, in case of error value 10 it was generated like:
"type" : "hexstr",
"value" : "10"
which will be read as hex value 16, not 10 as it should be.
Now it is generate like:
"type" : "hexstr",
"value" : "0xa"
I will include a test for this case and make it as a seperate PR.

mihaibudiu · 2019-03-19T00:38:35Z

backends/bmv2/common/parser.cpp

@@ -187,6 +187,22 @@ Util::IJson* ParserConverter::convertParserStatement(const IR::StatOrDecl* stat)
                    params->append(jexpr);
                }
                return result;
+            } else if (extfn->method->name.name == "assert") {


the code is almost the same, can you unify it?

mihaibudiu · 2019-03-19T00:39:36Z

backends/bmv2/psa_switch/psaSwitch.cpp

@@ -997,4 +999,42 @@ void ExternConverter_Digest::convertExternInstance(
    UNUSED const IR::ExternBlock* eb, UNUSED const bool& emitExterns)
 { /* TODO */ }

+Util::IJson* ExternConverter_assert::convertExternFunction(


lots of code duplicated here as well. Can you refactor?

mihaibudiu · 2019-03-19T00:40:19Z

backends/bmv2/simple_switch/simpleSwitch.cpp

+ExternConverter_assert ExternConverter_assert::singleton;
+ExternConverter_assume ExternConverter_assume::singleton;
+
+Util::IJson* ExternConverter_assert::convertExternFunction(


and again. Could this code go to common?

mihaibudiu · 2019-03-19T00:40:49Z

backends/ebpf/ebpfControl.cpp

+        builder->emitIndent();
+        builder->append("if (");
+        visit(function->expr->arguments->at(0)->expression);
+        builder->append(" == false) ");


This should be rather !expr

mihaibudiu · 2019-03-19T00:44:45Z

backends/ebpf/ebpfParser.cpp

+            return false;
+        }
+    } else if (mi->is<P4::BuiltInMethod>()) {
+    // Added this because compiler didn't recognize assert(hdr.ethernet.isValid()), for expample


if this is a bug maybe you can file a separate PR and a test case for it.
When does the compiler not recognize isValid, only within assert?
isValid should be handled by the expressionConverter.

Compiler didn't recognize isValid in assert, but also it didn't recognize setValid and setInvalid method calls for that ebpf backend when they are called from a parser state.
Also, I notice that compiler doesn't recognize verify call in parser state for ebpf backend, but I didn't add code generation for that case. In that case following error is reported:
error: Unexpected method call in parser verify
verify(false, error.NoError);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
If I understood it well, it should be enabled to call methods, that are mentioned above, in parser state.

It's possible that verify is not supported yet in the back-end.
But isValid should work; if you have a counter-example please file another issue.

mihaibudiu · 2019-03-19T00:45:15Z

backends/ebpf/ebpfTable.cpp

@@ -54,6 +54,67 @@ class ActionTranslationVisitor : public CodeGenInspector {
        return false;
    }

+    bool preorder(const IR::MethodCallExpression* expression) {
+        auto mi = P4::MethodInstance::resolve(expression, refMap, typeMap);
+        if (mi->is<P4::ExternFunction>()) {


this code should be refactored and should appear only once.

mihaibudiu · 2019-03-19T00:45:45Z

backends/ebpf/target.cpp

@@ -21,7 +21,8 @@ namespace EBPF {


 void KernelSamplesTarget::emitIncludes(Util::SourceCodeBuilder* builder) const {
-    builder->append("#include \"ebpf_kernel.h\"\n");
+    builder->append("#include \"ebpf_kernel.h\"\n"


Is there stdio.h in the kernel?

mihaibudiu · 2019-03-19T00:46:51Z

frontends/p4/coreLibrary.h

@@ -30,6 +30,8 @@ enum class StandardExceptions {
    OverwritingHeader,
    HeaderTooShort,
    ParserTimeout,
+    AssertError,


This is a big assumption: that we are changing code.p4.
I would rather expect that assert and assume are library functions - at least for a while.
Putting them in core.p4 may break programs that happen to use identifiers with these names.
This is a subject for the LDWG.

mihaibudiu · 2019-03-19T00:48:01Z

frontends/p4/frontend.cpp

@@ -148,6 +149,9 @@ const IR::P4Program *FrontEnd::run(const CompilerOptions &options, const IR::P4P
        new TypeInference(&refMap, &typeMap, false),  // insert casts
        new ValidateMatchAnnotations(&typeMap),
        new DefaultArguments(&refMap, &typeMap),  // add default argument values to parameters
+#ifdef NDEBUG


First of all, this NDEBUG is for the compiler source code. You should remove assert/assume only if the p4 compiler is invoked with NDEBUG, not gcc.
Second, this is too early to remove the calls. If the calls have side-effects they should still happen. So the removal should happen after the SideEffects pass.
Third, I am not sure we actually want this part of the front-end; perhaps the mid-end.

If I understood you well, p4 compiler should remove assert/assume if it is invoked with -DNDEBUG (and default) option and leave it if it is invoked with -UNDEBUG. I moved this pass to be the first in the mid-end, before any of the optimizations is done. Feel free to correct me if I misunderstood it.

What Mihai means is that when you write #ifdef NDEBUG, you are using a preprocessor flag that is meant for the C++ compiler with which you compile p4c. The assert / assume statements should be removed if the p4c compiler is invoked with -DNDEBUG. When I compile a C / C++ program, I choose whether asserts are removed by providing -DNEBUG or not. Whether the C / C++ compiler was itself compiled with -DNEBUG is completely irrelevant. The p4c invocation p4c -DNEBUG <path to P4 program> should remove the assert / assume statements. I would argue that using a preprocessor flag for this is probably not ideal. What about p4c -ndebug <path to P4 program> instead?

mihaibudiu · 2019-03-19T00:50:26Z

backends/ebpf/ebpfControl.cpp

+        auto linePosition = srcInfo.toPositionString();
+        builder->emitIndent();
+        builder->appendFormat(
+            "fprintf(stderr, \"Assertion error: ' % s ' failed, file ' % s ', line % s \\n\");",


Have you tested this with kernel code? Can you just call fprintf from an ebpf program running in the kernel?

I was trying to test it, but I couldn't manage to do it because I got some errors when I tried to compile .c file that is p4c output. So I did it according to the rest of code gen for ebpf backend.
Maybe I didn't understand well how to test it, so I would be thankful if you can give me more information how to do it.

If you get errors compiling a C file it's a bug in the ebpf back-end - please file an issue.
The ebpf testing tries to test the files in multiple ways, depending on your kernel version.
But the ebpf code is supposed to run in the kernel, so it may not use fprintf.
The more important question is how to handle an assertion failure in ebpf.

mihaibudiu · 2019-03-26T15:34:51Z

Usually assume gives preconditions (which are assumed to be true before you enter a piece of code), and assert enforces postconditions (which are true when you exit a piece of code). Usually a static analyzer (a prover) tries to prove the postconditions assuming that the preconditions hold. The prover cannot prove the precoditions - it will take them for granted. That's the difference between assume and assert. This behavior is true for static analyses.

The (dynamic) runtime behavior of both statements is the same, though: if the condition is false, then something is very wrong. For assume it means that the assumption was incorrect. For asserts it would mean that the proof made by the prover was wrong.

enisah · 2019-04-16T18:31:40Z

Hello everyone, I have done changes according to your suggestions. Unfortunately I didn't manage to test implementation for ebpf backend, so I made a new PR with support for bmv2 backend only. Please take a look, here is link to new PR #1859, meanwhile I will try to resolve problem with ebpf.

mihaibudiu requested changes Mar 19, 2019

View reviewed changes

enisah closed this Apr 16, 2019

enisah deleted the assert-assume-support branch April 16, 2019 17:45

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added support for assert and assume statement (#1548) #1799

Added support for assert and assume statement (#1548) #1799

enisah commented Mar 18, 2019

jafingerhut commented Mar 18, 2019

mihaibudiu left a comment

mihaibudiu Mar 19, 2019

enisah Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

enisah Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu Mar 19, 2019

enisah Mar 27, 2019

antoninbas Apr 1, 2019

mihaibudiu Mar 19, 2019

enisah Mar 19, 2019

mihaibudiu Mar 19, 2019

mihaibudiu commented Mar 26, 2019

enisah commented Apr 16, 2019

Added support for assert and assume statement (#1548) #1799

Added support for assert and assume statement (#1548) #1799

Conversation

enisah commented Mar 18, 2019

jafingerhut commented Mar 18, 2019

mihaibudiu left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mihaibudiu commented Mar 26, 2019

enisah commented Apr 16, 2019