Python frontend: Class definition and instantiation #1552

brcfarias · 2023-12-20T19:02:22Z

This pull request adds support for class definition and instantiation.
Some relevant details:

The init() method is treated as class constructor.
In constructor calls like obj1 = MyClass(..), obj1 is passed as the first argument to the constructor.
In Python, "Variables defined in the class definition are class attributes; they are shared by instances. Instance attributes can be set in a method with self.name = value. Both class and instance attributes are accessible through the notation “self.name”, and an instance attribute hides a class attribute with the same name when accessed in this way."(https://docs.python.org/3/reference/compound_stmts.html#class).
This pull request specifically addresses instance attributes. When an attribute is referred by "self" it is added as a field to the corresponding self type. Class attributes will be addressed in a future (perhaps the next) PR.
The current implementation does not yet consider default inheritance from "object" class. This feature will also be addressed in a subsequent update.

lucasccordeiro · 2023-12-21T08:43:10Z

src/clang-c-frontend/clang_c_adjust_expr.cpp

@@ -234,6 +234,9 @@ void clang_c_adjust::adjust_side_effect(side_effect_exprt &expr)
    else if (statement == "gcc_conditional_expression")
    {
    }
+    else if (statement == "nondet")


Why do we have this statement?

A sideeffect with nondet as statement is generated at:
https://github.com/brcfarias/esbmc/blob/69112185c12d40be1eed5d87ea57c4eb6e9e23ac/src/python-frontend/python_converter.cpp#L352C5-L364C6

Due to the addition of the adjust step (see https://github.com/brcfarias/esbmc/blob/69112185c12d40be1eed5d87ea57c4eb6e9e23ac/src/python-frontend/python_language.cpp#L101) to manage pointer to struct usage, it was necessary to add it to avoid the abort at https://github.com/brcfarias/esbmc/blob/69112185c12d40be1eed5d87ea57c4eb6e9e23ac/src/clang-c-frontend/clang_c_adjust_expr.cpp#L243

Can you please add some comments here?

lucasccordeiro · 2023-12-21T08:43:47Z

src/python-frontend/python_annotation.h

@@ -125,8 +134,17 @@ class python_annotation

        // lhs
        auto target = element["targets"][0];
-        int col_offset = target["col_offset"].template get<int>() +
-                         target["id"].template get<std::string>().size() + 1;
+        std::string id;


can you add some comments here?

lucasccordeiro · 2023-12-21T08:44:10Z

src/python-frontend/python_annotation.h

@@ -156,6 +174,26 @@ class python_annotation
        element["value"]["end_col_offset"] =
          element["value"]["end_col_offset"].template get<int>() + type.size() +
          1;
+
+        if (element["value"].contains("args"))


Can you add some comments here?

lucasccordeiro · 2023-12-21T08:48:20Z

src/python-frontend/python_converter.cpp

+{
+  std::string symbol_id = "py:" + python_filename;
+  if (!current_class_name.empty())
+    symbol_id += "@C@" + current_class_name;


The + operator is usually okay for small string operations. However, it might be more efficiently done using std::stringstream or std::string::append to avoid unnecessary copying.

I changed to stringstream. Thanks.

lucasccordeiro · 2023-12-21T08:51:07Z

src/python-frontend/python_converter.cpp

+        if (it.first == "identifier")
+          obj_type_name = it.second.id_string();
+      }
+      assert(!obj_type_name.empty());


Shall we really use assert statements here? What happens with the release mode when we disable these assertions?

In release we would have a crash when dereferecing class_symbol at https://github.com/brcfarias/esbmc/blob/69112185c12d40be1eed5d87ea57c4eb6e9e23ac/src/python-frontend/python_converter.cpp#L502C1-L503C1.

I will remove the asserts, check if class_symbol is valid before dereferencing, and call abort() if so.

Excellent! Thanks, @brcfarias.

lucasccordeiro

Thanks for addressing my comments, @brcfarias.

fbrausse

In general looks like a good approach to me.

Since supporting the full dynamic nature of the language is probably out of scope, I'd suggest to start documenting the particular Python dialect supported by this frontend. Some things like the following reflect existing practice, but are not required by the language:

name self isn't fixed (could also be me or any other valid identifier)
restriction about int values we talked about before
computed instance attibutes not supported (e.g. non-literal access via get/setattr())
variable declarations need type annotations

lucasccordeiro · 2023-12-23T07:01:48Z

Thanks for submitting this PR, @brcfarias.

Can you please submit another PR that addresses @fbrausse's suggestion about the documentation?

brcfarias requested review from mikhailramalho, fbrausse, lucasccordeiro and rafaelsamenezes December 20, 2023 19:02

lucasccordeiro force-pushed the python-frontend branch from b9d5641 to 6911218 Compare December 20, 2023 23:18

lucasccordeiro requested changes Dec 21, 2023

View reviewed changes

brcfarias added 19 commits December 21, 2023 11:08

[python-frontend] Initial support for classes

3294be5

[python-frontend] Symbol id generation in a single function

a42e34c

[python-frontend] Get class attributes

1dc5411

[python-frontend] Add function to detect constructor calls

d7ea363

[python-frontend] Handling attributes access

163c90c

[python-frontend] Add regression tests

3b45add

[python-frontend] Add type annotation for constructor calls

4aa6b37

[python-frontend] Fix log

038e992

[python-frontend] Adjust type annotation for attributes

580b740

[python-frontend] Fix symbol id

e56db23

[python-frontend] Fix class type

bbe40db

[python-frontend] Get class attributes from self members

81c5a4a

[python-frontend] Passing instance as self parameter

fec9e07

[python-frontend] Adjust data members access

18f399f

[python-frontend] Add regression test

c4c79a6

[python-frontend] Fix constructor call and object member access

70c5a1d

[python-frontend] Fix attribute access

f807a7a

Accepting nondet as statement on side effect adjustment

c8a4d1b

Handling review comments

4192ac0

brcfarias force-pushed the python-frontend branch from 6911218 to 4192ac0 Compare December 21, 2023 11:10

clang-format

baa56e6

lucasccordeiro approved these changes Dec 21, 2023

View reviewed changes

fbrausse approved these changes Dec 23, 2023

View reviewed changes

Merge branch 'master' into python-frontend

a638703

lucasccordeiro merged commit 7c6d7d6 into esbmc:master Dec 23, 2023
7 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Python frontend: Class definition and instantiation #1552

Python frontend: Class definition and instantiation #1552

brcfarias commented Dec 20, 2023 •

edited

Loading

lucasccordeiro Dec 21, 2023

brcfarias Dec 21, 2023 •

edited

Loading

lucasccordeiro Dec 21, 2023

lucasccordeiro Dec 21, 2023

lucasccordeiro Dec 21, 2023

lucasccordeiro Dec 21, 2023

brcfarias Dec 21, 2023

lucasccordeiro Dec 21, 2023

brcfarias Dec 21, 2023

lucasccordeiro Dec 21, 2023

lucasccordeiro left a comment

fbrausse left a comment •

edited

Loading

lucasccordeiro commented Dec 23, 2023

Python frontend: Class definition and instantiation #1552

Python frontend: Class definition and instantiation #1552

Conversation

brcfarias commented Dec 20, 2023 • edited Loading

Choose a reason for hiding this comment

brcfarias Dec 21, 2023 • edited Loading

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

lucasccordeiro left a comment

Choose a reason for hiding this comment

fbrausse left a comment • edited Loading

Choose a reason for hiding this comment

lucasccordeiro commented Dec 23, 2023

brcfarias commented Dec 20, 2023 •

edited

Loading

brcfarias Dec 21, 2023 •

edited

Loading

fbrausse left a comment •

edited

Loading