[vala/staging] codegen: Emit postconditions before free'ing local variables

[Rico Tzschichholz <ricotz src gnome org>]

commit 4555ed66dcf5839e79e3b9a62ef5cf83bde35d4e
Author: Rico Tzschichholz <ricotz ubuntu com>
Date:   Fri Mar 13 00:01:09 2020 +0100

    codegen: Emit postconditions before free'ing local variables
    
    It was possible to cause segmentation-faults or use-after-free errors.

 codegen/valaccodebasemodule.vala  | 18 ++++++++------
 tests/Makefile.am                 |  1 +
 tests/methods/postconditions.vala | 51 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 63 insertions(+), 7 deletions(-)
---
diff --git a/codegen/valaccodebasemodule.vala b/codegen/valaccodebasemodule.vala
index 20f250704..0bf62de07 100644
--- a/codegen/valaccodebasemodule.vala
+++ b/codegen/valaccodebasemodule.vala
@@ -2339,6 +2339,14 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
                        pop_line ();
                }
 
+               if (b.parent_symbol is Method) {
+                       unowned Method m = (Method) b.parent_symbol;
+                       // check postconditions
+                       foreach (var postcondition in m.get_postconditions ()) {
+                               create_postcondition_statement (postcondition);
+                       }
+               }
+
                // free in reverse order
                for (int i = local_vars.size - 1; i >= 0; i--) {
                        var local = local_vars[i];
@@ -2363,10 +2371,6 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
                                        return_out_parameter (param);
                                }
                        }
-                       // check postconditions
-                       foreach (var postcondition in m.get_postconditions ()) {
-                               create_postcondition_statement (postcondition);
-                       }
                } else if (!unreachable_exit_block && b.parent_symbol is PropertyAccessor) {
                        var acc = (PropertyAccessor) b.parent_symbol;
                        if (acc.value_parameter != null && !acc.value_parameter.captured && requires_destroy 
(acc.value_parameter.variable_type)) {
@@ -3993,9 +3997,6 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
                        ccode.add_assignment (result_lhs, get_cvalue (stmt.return_expression));
                }
 
-               // free local variables
-               append_local_free (current_symbol);
-
                if (current_method != null) {
                        // check postconditions
                        foreach (Expression postcondition in current_method.get_postconditions ()) {
@@ -4003,6 +4004,9 @@ public abstract class Vala.CCodeBaseModule : CodeGenerator {
                        }
                }
 
+               // free local variables
+               append_local_free (current_symbol);
+
                if (current_method != null && !current_method.coroutine) {
                        // assign values to output parameters if they are not NULL
                        // otherwise, free the value if necessary
diff --git a/tests/Makefile.am b/tests/Makefile.am
index dcda2cbe0..9139b02d5 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -120,6 +120,7 @@ TESTS = \
        methods/iterator.vala \
        methods/parameter-ref-array-resize.vala \
        methods/prepostconditions.vala \
+       methods/postconditions.vala \
        methods/same-name.vala \
        methods/symbolresolution.vala \
        methods/bug540483.vala \
diff --git a/tests/methods/postconditions.vala b/tests/methods/postconditions.vala
new file mode 100644
index 000000000..5cd9c5929
--- /dev/null
+++ b/tests/methods/postconditions.vala
@@ -0,0 +1,51 @@
+void foo (owned string[] a) ensures (a[1] == "bar") {
+}
+
+void foz (ref string[] a) ensures (a[1] == "bar") {
+       a = { "foo", "bar" };
+}
+
+void fom (out string[] a) ensures (a[1] == "bar") {
+       a = { "foo", "bar" };
+}
+
+string[] bar (owned string[] a) ensures (result[0] == "manam" && a[1] == "foo") {
+       return { "manam" };
+}
+
+string[] baz (ref string[] a) ensures (result[0] == "manam" && a[1] == "foo") {
+       a = { "bar", "foo" };
+       return { "manam" };
+}
+
+string[] bam (out string[] a) ensures (result[0] == "manam" && a[1] == "foo") {
+       a = { "bar", "foo" };
+       return { "manam" };
+}
+
+void main () {
+       {
+               foo ({ "foo", "bar" });
+       }
+       {
+               string[] a = {};
+               foz (ref a);
+               assert (a[0] == "foo");
+       }
+       {
+               string[] a;
+               fom (out a);
+               assert (a[0] == "foo");
+       }
+       {
+               assert (bar ({ "bar", "foo" })[0] == "manam");
+       }
+       {
+               string[] a = {};
+               assert (baz (ref a)[0] == "manam");
+       }
+       {
+               string[] a;
+               assert (bam (out a)[0] == "manam");
+       }
+}