Skip to content

Instantly share code, notes, and snippets.

@master-q

master-q/memo.md

Last active November 17, 2019 07:11
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save master-q/729d9f5b7405760ee5fafea9e9a30658 to your computer and use it in GitHub Desktop.
Save master-q/729d9f5b7405760ee5fafea9e9a30658 to your computer and use it in GitHub Desktop.
Download ZIP
Metasepiプロジェクト進捗報告 2019年11月 (日本Androidの会秋葉原支部ロボット部 第86回勉強会)
Raw
memo.md

Metasepiプロジェクト進捗報告 2019年11月 (日本Androidの会秋葉原支部ロボット部 第86回勉強会)

idiomaticca(i9a): C言語コードからATS実装を自動生成

YouTubeでクオリティショッキング配信

kernel-tla: Linux kernelの一部をTLA+で検証する

リポジトリ

概要

主にarm64アーキティクチャについてkernel部品毎に別々のTLA+コードで検証する

$ date
Fri 19 Apr 2019 06:00:00 PM JST
$ wc -l *.tla|sort -n
   212 ticketlock.tla
   468 qrwlock.tla
   614 qspinlock.tla
   623 ctxsw.tla
  1029 asidalloc.tla
  1506 arm64kpti.tla
  4452 total

ということで当面はticketlock.tlaを理解することが先決？ と思ったけれどctxsw.tlaはコンテキストスイッチだから面白そう

使用方法

からtla.zipをダウンロード。

$ cd ~/
$ unar tla.zip
$ ls ~/tla
com/       javax/       META-INF/  pcal/   tla2sany/  tlc2/
examples/  License.txt  model/     README  tla2tex/   util/
$ cd ~/src
$ git clone git://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git
$ cd kernel-tla
$ ls
arm64kpti.cfg  asidalloc.tla  ctxsw.cfg    qrwlock.tla    README
arm64kpti.tla  check.sh*      ctxsw.tla    qspinlock.cfg  ticketlock.cfg
asidalloc.cfg  COPYING        qrwlock.cfg  qspinlock.tla  ticketlock.tla
$ which tla2dvi
tla2dvi () {
        if [ "$#" != "1" ]
        then
                echo "Usage: tla2dvi FILENAME.tla"
                return 1
        fi
        java -classpath $HOME/tla tla2tex.TLA $1
        xdvi `basename -s tla $1`dvi
}
$ tla2dvi ticketlock.tla
$ ./check.sh ticketlock

ValaはどうやってDWARFを吐くのか

参考

やってみる

$ cat main.vala
class Foo : Object {
    public int field;
}

void main() {
    Foo? foo = null;
    stdout.printf("%d\n", foo.field);
}
$ valac -g --save-temps main.vala
$ gdb main
(gdb) run
Starting program: /home/kiwamu/tmp/vala/main 
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Program received signal SIGSEGV, Segmentation fault.
0x0000555555555333 in _vala_main () at main.vala:7
7           stdout.printf("%d\n", foo.field);
(gdb) bt
#0  0x0000555555555333 in _vala_main () at main.vala:7
#1  0x0000555555555386 in main (argc=1, argv=0x7fffffffd688) at main.vala:5

valac -gすると何が起きる？

以下を眺めてみる:

$ strace -f -s 100000 valac -g --save-temps main.vala |&lv

なんとどうやら以下でシンボルが埋め込まれるらしい。

$ valac -g --save-temps main.vala
$ rm -f a.out main
$ vi main.vala
  1 class Foo : Object {
  2     public int field;
  3 }
  4 
  5 void main() {
  6     Foo? foo = null;
  7     stdout.printf("%d\n", foo.field);
  8 }
$ cat main.c
/* main.c generated by valac 0.42.5, the Vala compiler
 * generated from main.vala, do not modify */



#include <glib.h>
#include <glib-object.h>
#include <stdio.h>


#define TYPE_FOO (foo_get_type ())
#define FOO(obj) (G_TYPE_CHECK_INSTANCE_CAST ((obj), TYPE_FOO, Foo))
#define FOO_CLASS(klass) (G_TYPE_CHECK_CLASS_CAST ((klass), TYPE_FOO, FooClass))
#define IS_FOO(obj) (G_TYPE_CHECK_INSTANCE_TYPE ((obj), TYPE_FOO))
#define IS_FOO_CLASS(klass) (G_TYPE_CHECK_CLASS_TYPE ((klass), TYPE_FOO))
#define FOO_GET_CLASS(obj) (G_TYPE_INSTANCE_GET_CLASS ((obj), TYPE_FOO, FooClass))

typedef struct _Foo Foo;
typedef struct _FooClass FooClass;
typedef struct _FooPrivate FooPrivate;
enum  {
	FOO_0_PROPERTY,
	FOO_NUM_PROPERTIES
};
static GParamSpec* foo_properties[FOO_NUM_PROPERTIES];
#define _g_object_unref0(var) ((var == NULL) ? NULL : (var = (g_object_unref (var), NULL)))

struct _Foo {
	GObject parent_instance;
	FooPrivate * priv;
	gint field;
};

struct _FooClass {
	GObjectClass parent_class;
};


static gpointer foo_parent_class = NULL;

GType foo_get_type (void) G_GNUC_CONST;
Foo* foo_new (void);
Foo* foo_construct (GType object_type);
static void foo_finalize (GObject * obj);
void _vala_main (void);


Foo*
foo_construct (GType object_type)
{
	Foo * self = NULL;
#line 1 "main.vala"
	self = (Foo*) g_object_new (object_type, NULL);
#line 1 "main.vala"
	return self;
#line 57 "main.c"
}


Foo*
foo_new (void)
{
#line 1 "main.vala"
	return foo_construct (TYPE_FOO);
#line 66 "main.c"
}


static void
foo_class_init (FooClass * klass)
{
#line 1 "main.vala"
	foo_parent_class = g_type_class_peek_parent (klass);
#line 1 "main.vala"
	G_OBJECT_CLASS (klass)->finalize = foo_finalize;
#line 77 "main.c"
}


static void
foo_instance_init (Foo * self)
{
}


static void
foo_finalize (GObject * obj)
{
	Foo * self;
#line 1 "main.vala"
	self = G_TYPE_CHECK_INSTANCE_CAST (obj, TYPE_FOO, Foo);
#line 1 "main.vala"
	G_OBJECT_CLASS (foo_parent_class)->finalize (obj);
#line 95 "main.c"
}


GType
foo_get_type (void)
{
	static volatile gsize foo_type_id__volatile = 0;
	if (g_once_init_enter (&foo_type_id__volatile)) {
		static const GTypeInfo g_define_type_info = { sizeof (FooClass), (GBaseInitFunc) NULL, (GBaseFinalizeFunc) NULL, (GClassInitFunc) foo_class_init, (GClassFinalizeFunc) NULL, NULL, sizeof (Foo), 0, (GInstanceInitFunc) foo_instance_init, NULL };
		GType foo_type_id;
		foo_type_id = g_type_register_static (G_TYPE_OBJECT, "Foo", &g_define_type_info, 0);
		g_once_init_leave (&foo_type_id__volatile, foo_type_id);
	}
	return foo_type_id__volatile;
}


void
_vala_main (void)
{
	Foo* foo = NULL;
	FILE* _tmp0_;
	gint _tmp1_;
#line 6 "main.vala"
	foo = NULL;
#line 7 "main.vala"
	_tmp0_ = stdout;
#line 7 "main.vala"
	_tmp1_ = foo->field;
#line 7 "main.vala"
	fprintf (_tmp0_, "%d\n", _tmp1_);
#line 5 "main.vala"
	_g_object_unref0 (foo);
#line 129 "main.c"
}


int
main (int argc,
      char ** argv)
{
#line 5 "main.vala"
	_vala_main ();
#line 5 "main.vala"
	return 0;
#line 141 "main.c"
}
$ gcc -g `pkg-config --cflags --libs glib-2.0 gobject-2.0` main.c
$ gdb a.out
(gdb) run
Starting program: /home/kiwamu/tmp/vala/a.out
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Program received signal SIGSEGV, Segmentation fault.
0x0000555555555333 in _vala_main () at main.vala:7
7           stdout.printf("%d\n", foo.field);
(gdb) bt
#0  0x0000555555555333 in _vala_main () at main.vala:7
#1  0x0000555555555386 in main (argc=1, argv=0x7fffffffd678) at main.vala:5

ということで単に#lineを打ち込めばDWARFが適切に吐き出されるらしい。 ちなみにclangも同様の動作。

ところで

今はGenieという言語の方が最新？ / "Projects/Genie - GNOME Wiki!" https://wiki.gnome.org/Projects/Genie

ATS2(ATS-Postiats)はDWARFに対応済みだった

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment